![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
dependent types
(как бы разворачивая каменты из предыдущего поста)
А расскажите, где вообще полезны dependent types?
Про примеры с массивами и их границами я в курсе, но это мало полезно лично мне на практике -- дело в том, что я как-то не нарывался на проблемы с этим уже несколько лет, причём dependent types не использовал для этого никак, ни разу. (а вот модульность и нормальные интерфейсы модулей -- как раз использовал.)
Далее, понятно, с помощью dependent types можно протаскивать какие-то утверждения в compile time. Очень хорошо, но с какими практическими целями?
Что я уже читал: первые несколько страниц выдачи гугла по "dependent types", в том числе известное "why dependent types matter". И, всё равно, либо dependent types это малонужная хуйня, либо я тупой. (не стесняйтесь, я прекрасно знаю свои интеллектуальные способности, поэтому последний вариант не оскорбителен.)
А расскажите, где вообще полезны dependent types?
Про примеры с массивами и их границами я в курсе, но это мало полезно лично мне на практике -- дело в том, что я как-то не нарывался на проблемы с этим уже несколько лет, причём dependent types не использовал для этого никак, ни разу. (а вот модульность и нормальные интерфейсы модулей -- как раз использовал.)
Далее, понятно, с помощью dependent types можно протаскивать какие-то утверждения в compile time. Очень хорошо, но с какими практическими целями?
Что я уже читал: первые несколько страниц выдачи гугла по "dependent types", в том числе известное "why dependent types matter". И, всё равно, либо dependent types это малонужная хуйня, либо я тупой. (не стесняйтесь, я прекрасно знаю свои интеллектуальные способности, поэтому последний вариант не оскорбителен.)