Простое введение в завтипы

Почти все слышали про современные функциональные языки программирования со строгими системами типов. Например, про Haskell. Этим языком и темами про монады и монадные трансформеры уже никого не удивить. Зато про языки с зависимыми типами слышали далеко не все, хотя это очень интересная и многообещающая история.

Зависимые типы настолько выразительны, что позволяют перенести решение некоторых safety-проблем на уровень компиляции. По сути вы пишете спецификацию своей программы в типах, и написав программу, проходящую проверку типов, автоматически получаете доказательство ее корректности.

Статьи и книги, объясняющие базовые принципы таких языков, к сожалению, часто достаточно объемны, а хотелось бы поверхностно ознакомиться с темой, чтобы понимать, инвестировать ли в нее время.

К счастью, есть неплохая статья 2009 года с введением в зависимые типы на примере языка Agda. В ней авторы демонстрируют несколько примеров того, как языки с завтипами могут статически решать проблемы, которые раньше разрешались только на стадии исполнения.

#literature