История изменений

На сколько я понимаю, идрис - первый язык с депендент тайпс который претендует на звание «язык общего назначения» (не уверен претендует ли Агда).

Идиоматические абстракции - не новые. Новые они с данной системой типов.

Теория действительно разрабатывается довольно давно. Но как долго не появлялось важных статей по теории? (ну понятно исследовательские по агде/идрису появляются интересные, но я имею ввиду так сказать «вехи»).

В целом наверное тебе виднее, я ещё не разобрался с теорией так чтобы спорить по существу по теории, но по практике - это всё таки новый шаг в языках (общего назначения).

АПД. Да, вот вспомнил, у пирса в 2002 (кажется) году было «такие языки испытывают пока серьёзные трудности» (о языках с зависимыми типами). Т.е. идрис - это достижение последних 10-15 лет, на практике. По теории, повторюсь, не возьмусь судить.

На сколько я понимаю, идрис - первый язык с депендент тайпс который претендует на звание «язык общего назначения» (не уверен претендует ли Агда).

Идиоматические абстракции - не новые. Новые они с данной системой типов.

Теория действительно разрабатывается довольно давно. Но как долго не появлялось важных статей по теории? (ну понятно исследовательские по агде/идрису появляются интересные, но я имею ввиду так сказать «вехи»).

В целом наверное тебе виднее, я ещё не разобрался с теорией так чтобы спорить по существу по теории, но по практике - это всё таки новый шаг в языках (общего назначения).

На сколько я понимаю, идрис - первый язык с депендент тайпс который претендует на звание «язык общего назначения» (не уверен претендует ли Агда).

Идиоматические абстракции - не новые. Новые они с данной системой типов.

Теория действительно разрабатывается довольно давно. Но как долго не появлялось важных статей по теории? (ну понятно исследовательские по агде/идрису появляются интересные, но я имею ввиду так сказать «вехи»).

В целом наверное тебе виднее, я ещё не разобрался с теорией так чтобы спорить по существу.