Category: эзотерика

glider

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

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

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

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