Типы в языках программирования

2023/2024

Учебный год

RUS

Обучение ведется на русском языке

5

Кредиты

Кто читает:

Департамент больших данных и информационного поиска

Статус:

Курс по выбору

Когда читается:

4-й курс, 1, 2 модуль

Преподаватель

Соколов Павел Павлович

Программа дисциплины

Аннотация

Можно с уверенностью сказать, что сфера разработки языков программирования переживает новый бум — из тех имён, что на слуху, можно назвать Rust, Julia, Kotlin, Crystal, Zig,.. Причём основным selling point большинства новых языков является какая-то инновационная система типов. Данный курс как раз и посвящен введению в теорию типов — учение о дизайне систем типов и разработке соответствующих алгоритмов. Будем решать как теоретические, так и практические задачи; если вам до этого нравились курсы по дискретной математике, логике, вычислимости и алгоритмам, вам понравится и здесь.

Цель освоения дисциплины

• Изучение основных алгоритмов проверки и вывода типов.
• Знакомство с взаимосвязями между теорией типов и логикой, написанием кода и доказательством теорем.

Планируемые результаты обучения

• Знакомство с теорией типов.
• Умение формализовать системы типов различных языков программирования.

Содержание учебной дисциплины

• Введение в теорию типов. Система типов и денотационная семантика языка арифметики.
• Корректность, preservation и progress. Лямбда-исчисление и его Тьюринг-полнота.
• Теоретико-множественная семантика STLC. Алгебраические типы данных. Соответствие Карри-Говарда.
• Оператор явной типизации. Типизация параметров в STLC. Полиморфизм и System F. Лямбда-куб.
• Синтаксическая система типизации по Хиндли-Милнеру. Алгоритм W.
• Система типов Хиндли-Милнера и отношение подтипизации.
• Полиморфизм и подтипизация. Ко- и контравариантность.
• Рекурсивные типы.
• Рекурсивные типы и полиморфизм. Индуктивные типы.
• Операторы на типах. Система кайндов.
• Тайпклассы, трейты и функторы.
• Простые зависимые типы. Сигма-тип и Пи-тип.
• W-типы. Индукция. Язык Twelf.
• Равенство в DTT. Система типов Мартина-Лёфа.

Элементы контроля

• Практическое домашнее задание 1
  Реализация программы, обманывающей систему типов одного из мейнстримных языков программирования. 5 баллов за реализацию, 5 баллов за объяснение.
• Теоретическое домашнее задание 1
  Решение теоретических задач по темам первой части курса. До 15 баллов.
• Практическое домашнее задание 2
  Реализация алгоритма W с различными расширениями. Базовая реализация 10б, расширения – до 5 бб.
• Теоретическое домашнее задание 2
  Решение теоретических задач по темам второй части курса. До 15 баллов.
• Практическое домашнее задание 3
  Реализация двусторонней проверки типов с различными расширениями. Три вариации до 5 баллов за каждую.

Промежуточная аттестация

• 2023/2024 2nd module
  Итог = Округление(0.1 * ПДЗ1 + 0.2 * ПДЗ2 + 0.2 * ПДЗ3 + 0.25 * ТДЗ1 + 0.25 * ТДЗ2).

Список литературы

Рекомендуемая основная литература

• Pierce, B. C. (2002). Types and Programming Languages. Cambridge, Mass: The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=70966

Рекомендуемая дополнительная литература

• Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism (Vol. 1st ed). Amsterdam: Elsevier Science. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=196231