EG
И это закроет потребность в наиболее болезненных фичах типа HKT, не разверзая при этом бездну математического ада
Size: a a a
2021 February 01
DS
Проблема в том, что просто никто не брался за именно что практический язык с зав типами
EG
Проблема в том, что просто никто не брался за именно что практический язык с зав типами
Idris?
p
Idris?
Рисерч от одного человека
DS
Idris?
Язык который unironically компилится в схему - не может быть практичным по умолчанию
EG
Язык который unironically компилится в схему - не может быть практичным по умолчанию
Idris 1 имел собственный рантайм, и сильно его это спасло?
DS
Idris 1 имел собственный рантайм, и сильно его это спасло?
Там был такой рантайм, что лучше его бы не было.
DS
А практический язык - это прежде всего хороший рантайм и/или компилятор
EG
За 14 лет в идрисе тайп-левел функции не довели до совершенно элементарных уровней работоспособности типа "они работают на примитивных типах"
DS
За 14 лет в идрисе тайп-левел функции не довели до совершенно элементарных уровней работоспособности типа "они работают на примитивных типах"
Потому что автора не это интересует
DS
Принципиальной проблемы тут нет
p
За 14 лет в идрисе тайп-левел функции не довели до совершенно элементарных уровней работоспособности типа "они работают на примитивных типах"
Да это на изи делается лол
EG
14 человеколет.
В Zig за четыре года есть относительно-полноценные тайплевел функции.
Вот до чего доводит отсутствие тонны математики.
В Zig за четыре года есть относительно-полноценные тайплевел функции.
Вот до чего доводит отсутствие тонны математики.
p
Написать интерпретатор для семантического дерева - что может быть проще?
p
Просто не нужно
DS
14 человеколет.
В Zig за четыре года есть относительно-полноценные тайплевел функции.
Вот до чего доводит отсутствие тонны математики.
В Zig за четыре года есть относительно-полноценные тайплевел функции.
Вот до чего доводит отсутствие тонны математики.
Потому что другие приоритеты в языке, тот же идрис вообще не похож на практический язык.
DS
И не надо его таковой судить, чтобы фанаты не говорили
EG
Чортов тайпскрипт умеет работать с примитивными типами на тайплевеле. Найтли раст умеет. Плюсы умеют десять тысяч лет.
EG
Потому что другие приоритеты в языке, тот же идрис вообще не похож на практический язык.
Идрис позиционирует себя как практический в книжке
DS
Идрис позиционирует себя как практический в книжке
Потому что автор книжки хочет её продать.