постдока он кстати сейчас взял крутого, который раньше над агдой работал

Ну например скорее всего внутри скомпилированного Идриса лежит такая же вычислительная модель, как в хаскеле

неа

идрис2 вообще в схему компилится

ну и любой релиз довольно условная штука, вот хаскельный первый репорт как я понимаю не сильно отличался от драфта лета 88-го года (мономорфизм рестрикшоном, наличием вьюпаттернов и кое-каким синтаксисом по мелочи)
а то что более менее на нынешний хаскель похоже появилось только году в 96-м

первый компилился в стек промежуточных строгих языков, начиная от систем ф-образного до стекового автомата

нет

второй ещё сильнее от хаскеля отличается потому что там в ядро линейные типы ещё вшиты

если вкратце, то строгостью, завтипами+тотальностью и имплицитами+некогерентностью

Про тотальность я помню, про завтипы имею некоторое представление. Строгость уже является расплывчатым термином для моего понимания, имплициты - это явность чего-то?

Некогерентность же я просто не могу нагуглить. Нашел только некую отсылку к тому, что хаскель и ещё некоторое языки могут удовлетворять заданные ограничения на типы множеством разных способов, но тем не менее приходят к одному и тому же стабильному результату, и это дескать когерентно.

строгость/энергичность это неленивость, все вычисляется сразу

имплициты это аргументы, которые компилятор находит сам (унификацией или поиском)

когерентность да, это гарантия того что результат поиска по иерархии не зависит от траектории, классический пример в программировании - diamond problem

с завтипами можно делать адхок-когерентность вручную, протаскивая нужные равенства на уровне типов

Спасибо. На русском языке мало про Идрис пишут, а читать нечто сложное на английском я могу, но мне это неприятно.

Я раньше тоже так думал, пока не купил

Пожалуйста скажи где читать

Как когерентность протащить равенством

The principal use of lisp to me ( at least as of now) is to make me feel good about myself. I use python, php, ruby, js at my job but at home doing some lisp is better than sex

Всё так.