DP
sbcl выводит кое где
Size: a a a
2020 December 21
SA
я это и сказал
DP
Мне тоже интересно, что за реализации, типов-то в лиспах, почитай, кроме typed racket и CL нету. Есть только какие-то слабые попытки в Gambit Scheme
я имел ввиду хаскель - что там сплошной борьбизм с типами, вместо написания программ
DP
я это и сказал
ты лучше скажи, что бы ты хотел видеть. чем тебе не нравится typed racket? ты хочешь реализацию agda на лиспе или что
SA
рекет на борщ
SA
а так то да
SA
агда ок
SA
особенно если можно так а можно эдак
DP
есть какие-то реализации именно зависимых типов на лиспе? ракетка, цл? так чтоб оно гламурненько смотрелось и понятно было что с ним делать и зачем
DP
про ракетку и борщ не совсем понял посыл
DP
что мешает это сделать в виде библиотеки (макросов)? если кому-то нужны зависимые типы в CL или racket
DP
кстати, я не смотрел детально на Shen (Qi) - там как обстоят дела с зависимыми типами?
DP
локальный вывод типов, там где ты сам сказал, что да, давайте тут выводить - это вполне себе гуд. я против вывода типов везде и по дефолту. потому что это оверхед и "ненужно"
DP
что с макросами делать в системе с тотальным выводом типов? у нас есть примеры статически типизированных макросов - nemerle, scala. смотрятся ... э, ну так себе
DP
Shen по-идее из той же оперы (только лисп), но я его видел совсем издалека, то есть почти не видел даже
DP
на мой взгляд зависимые типы и прочий рокет сайнс взлетит, если показать - вот у нас крутая программа, в которой есть зависимые типы. смотрите как круто они помогают решать наши проблемы в этом домейне. ну и, естественно, это должно быть в проекте с открытым исходным кодом, чтобы каждый мог убедиться, а не на словах и обс
SA
что мешает это сделать в виде библиотеки (макросов)? если кому-то нужны зависимые типы в CL или racket
не особо чего мешает
DP
то есть лучший способ убедить кого-либо в крутости зависимых типов (в частности на лиспах) - это написать релевантный полезный код
SA
никто не сделал еще вот и все
SA
про ракетку и борщ не совсем понял посыл
они не одно и то же