Системы типизации лямбда-исчисления
Курс Хит![](https://www.lektorium.tv/sites/lektorium.tv/files/courses/1300660671_22797_csclub_moskvin_1_metadata.flv_snapshot_00.18.03_%5B2011.03.21_01.36.37%5D.jpg)
Современные функциональные языки программирования, такие как Haskell, наследники ML (SML, Ocaml, F#), Agda2 и т.п., обладают весьма богатыми и сложными системами типов. Несмотря на такое разнообразие, эти системы имеют в своей основе хорошо проработанную формальную теорию типизированных лямбда-исчислений.
В рамках курса рассматриваются различные системы типизации лямбда-исчисления. Понятие типа вводится на примере просто типизированного чистого лямбда-исчисления. Исследуются два основных подхода к типизации лямбда-исчисления: в стиле Карри и в стиле Чёрча. Обсуждаются следующие системы: полиморфные типы (System F), операторы над типами, полиморфизм высших порядков, зависимые типы, рекурсивные типы. Для изучаемых систем исследуются проблемы проверки, присваивания (синтеза) и населенности типов. Обсуждается связь между различными логическими системами и системами типов.