Category: эзотерика

Category was added automatically. Read all entries about "эзотерика".

glider

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

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

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

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