Хорошее объяснение на пальцах

что такое и к чему зависимые типы (точнее - частный случай, но зато понятный интуитивно) - мне в свое время когда разбирался чего-то такого именно для начала не хватало

(ну и вообще минипроектик и в целом полезный именно тем, что реализованы "в простом виде" довольно многие алгоритмы вывода типов)