xeno_by (xeno_by) wrote,
xeno_by
xeno_by

Categories:

Зависимые типы

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

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

upd. Материалы по теме:
* А про зависимые типы - это примерно так
* Зависимые типы и метапрограммирование
* Решительно непонятно, как можно программировать без dependent types
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 5 comments