gds (gds) wrote,
gds
gds

dependent types

(как бы разворачивая каменты из предыдущего поста)

А расскажите, где вообще полезны dependent types?
Про примеры с массивами и их границами я в курсе, но это мало полезно лично мне на практике -- дело в том, что я как-то не нарывался на проблемы с этим уже несколько лет, причём dependent types не использовал для этого никак, ни разу. (а вот модульность и нормальные интерфейсы модулей -- как раз использовал.)
Далее, понятно, с помощью dependent types можно протаскивать какие-то утверждения в compile time. Очень хорошо, но с какими практическими целями?
Что я уже читал: первые несколько страниц выдачи гугла по "dependent types", в том числе известное "why dependent types matter". И, всё равно, либо dependent types это малонужная хуйня, либо я тупой. (не стесняйтесь, я прекрасно знаю свои интеллектуальные способности, поэтому последний вариант не оскорбителен.)
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 37 comments