Степпер для SBCL - 2

Хочу задать вопрос участнику дискуссии 2017 года (товарищу «зачем нужен Lisp, если есть Agda/Idris»). AndreyKl, написал что-нибудь на Idris’е за это время? Есть такие, кто написал? Ищу пример реального использования, чтобы понять как это всё выглядит IRL, пока нахожу только обсасывание примера с вектором / матрицей (Matrix m n -> Matrix n k -> Matrix m k). Для чего-то ещё годится эта dependent typed system?

Ищу пример реального использования, чтобы понять как это всё выглядит IRL

Например, так:

https://gitlab.com/bobbbay/idris-server

Thanks. Как раз то что искал.

Prism, Adapter, Profunctor, Cartesian, CoCartesian, Optics, MkLens

Типичный API сервер :)

paper pdf

Естественно.

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

ха, классный вопрос :)

Так сложилось, что я ушёл в формальные доказательства. Поэтому на идрисе кроме крестиков ноликов я так ничего и не написал.

Но в целом, кроме того что привёл как пример monk, есть Scala - промышленно применяемый язык с зависимыми типами. Там можно поглядеть как это должно выглядеть ориентировочно. + Идрис может быть облегчит написание за счёт того Бреди называет type driven development. (Вообще на сколько я помню, мне показалось что очень удобно было видеть цели в ide, по сравнению со скала).

Для чего-то ещё годится эта dependent typed system?

Для формальных доказательств ещё.

В SBCL есть степпер. Делается (step) и дальше он включается при условии что декларации настроены на дебаг а не оптимизацию.

Проблема в чем? В тыканье мышкой как в дельфи? Столько лет, а писать на лиспе как на лиспе, а не как на дельфи, ты так и не научился.

Ты им на практике когда-нибудь пользовался?

Idris – это такой proof of concept. Его с тех пор заново переписали в Idris 2. А Agda реально используется для доказательств и верификации. Программы на ней, ясен хер, никто не пишет.

есть Scala - промышленно применяемый язык с зависимыми типами.

Нет там зависимых типов.

Что ты понимаешь под «писать на лиспе, как на лиспе а не как на дельфи»? В дельфи, питоне, го, js, я, находясь в точке кода во время выполнения, могу поставить, неважно чем, мышью или клавиатурой, брекпойнт ниже по стеку, потом нажать «продолжить» и бежать до этой точки. В лиспе я так сделать не могу, причём не только в SBCL, но и в LW, хотя в LW, в отличие от SBCL, есть хоть что-то более-менее похожее на человеческий степпер. В чём тут какая-то особая исключительность лиспа? Это простое неудобство, у которого нет никакого объяснения или оправдания. Просто плохо развитые инструментальные средства. Ни макросы, ни гомоиконность, ни горячая замена кода никак это не компенсируют - они про другое. trace лишь отчасти компенсирует и да, в обычных современных IDE оно тоже присутствует, хотя и в менее удобной форме. Сделать возможность ставить брекпойнты - нет никакой технической проблемы. Т.е. просто какие-то дурные предрассудки или чванство, какой-то мифический „особый путь“, там, где просто на самом деле дырявые носки.

https://markehammons.wordpress.com/2013/07/02/dependent-types-in-scala/

Ага. Но это не полноценные зависимые типы.

https://cstheory.stackexchange.com/questions/53728/isnt-it-misleading-for-scala-3-to-claim-it-has-dependent-function-types

Scala 3 doesn’t have full dependent types, but only path dependent types, which is a weaker form of dependency. They allow values (e.g. objects) to carry types along with them, and these types can be used in type-checking.

То есть, ты, конечно, можешь сказать, что и скала и хачкель (см. синглтоны) имеют зависимые типы, но что-то реально применимое в повседневности из этого сделать сложно.

Ты по ссылке https://markehammons.wordpress.com/2013/07/02/dependent-types-in-scala/ ходил? Там вполне подробно показывается, как можно построить.

Вот подробнее: https://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types

Ага. Я и код на хачкелле с синглтонами видел. Мне не понравилось.

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

Я с тех пор по собеседованиям успел помотаться, в том числе с разными ребятами, пишущими на скалке, говорил. Почему-то все как один говорят, что в итоге проще было на тот же хачкель перейти либо просто перестать насиловать скалу и писать на ней нормально.

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

Вроде были. Они правда называютсяу них вроде бы path dependent или как то так, но на сколько я помню по итогу они изоморфны обычным зависимым типам, т. Е. Одинако мощные и все что выражается в одной, можно выразить во второй. Но подробностей за давностью лет не дам. А откуда таки дровишки что нет?

Обн. Прочитал ответы, пока вопросы отпали. Можно считать что «чуть-чуть есть, если очень надо». спасибо за поправку.

Ага. Я и код на хачкелле с синглтонами видел. Мне не понравилось.

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

А если что-то чуть более нетривиальное доказывать, то синглтонов достаточно (пусть и слегка многословно).

Зачем ты врешь про отсутствие степпера в SBCL?

зачем ты врёшь про мои высказывания? Где я написал, что его нет?

Т.е. просто какие-то дурные предрассудки или чванство, какой-то мифический „особый путь“, там, где просто на самом деле дырявые носки.

А ты точно автор «славянского ПО»?

Есть определённый прогресс:

• можно ткнуть мышью и поставится точка прерывания. Которая, впрочем, не визуализируется, не прилипла к тексту и всё прочее плохое.
• работает step out, причём, чтобы он работал, необязательно сначала делать step in. Правда, алгоритм, который определяет, что мы вышли, приближённый и, наверное, может давать сбои
• также работает step over, но это и раньше работало
• шагание происходит подробно (остановка на каждый чих)
• треды пока никак не учитываются
• всё работает не просто неэффективно, а вопиюще неэффективно

Видосик я записал, но нет сил выложить, да и всё равно всем пофигу. Но код в принципе здесь:

https://tvoygit.ru/budden/jar/src/branch/jary-2024-07

Видимо, ещё несколько дней прозанимаюсь этим проектом, а потом математик сочтёт, что решение существует и уйдёт в свою комнату. Т.к. на самом деле моя задача совершенно не про то.

https://dzen.ru/video/watch/66b6870069a32a2421151420 - реализовал минимальное мышетыкальство. Но ещё пахать и пахать. А уже пора завязывать, или не пора.