платное говно не интересует

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

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

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

про макросы я ваще не уверен
можно како то пример макроса который ломает вывод типов

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

я не настолько крутой чтоб такое делать

а насчет никому не надо это конечно бредятина

всем все надо

а как привести пример макроса ломающего систему типов, если лисповые макросы не находятся в среде с выводом типов тотальным?

не сделал = не хочешь это самое тупое равенство на свете

ну вообрази что там это происходит

в чем проблема то

> оверхед чего времени компиляции?

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

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

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

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

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

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

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