Функциональное программирование

Санкт-Петербург, весна 2019

Описание

Курс знакомит слушателей с функциональными языками программирования и методами программирования на этих языках.

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

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

Мы изучим основные классы типов из стандартной библиотеки Haskell, в том числе функторы, аппликативные функторы и монады. Мы обсудим различные стратегии свертки и обхода списков, деревьев и познакомимся с обобщением этих операций в классах типов Foldable и Traversable.

Мы научимся программировать, используя стандартные монады, в частности обсудим проблему ввода-вывода в чистых языках и его реализацию в Haskell с помощью монады IO, а также работу с изменяемым состоянием с помощью монады State и родственных ей монад.

Критерии выставления оценок за курс

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

Оценка отлично выставляется тем, кто наберет 90% баллов и более (140 баллов). Оценка хорошо - тем, кто наберет 75% баллов (117 баллов). Оценка удовлетворительно (зачет) - тем, кто наберет 50% баллов (78 баллов).

Литература

Основная:

  • Miran Lipovača, Learn You a Haskell for Great Good! A Beginner’s Guide 2011 http://learnyouahaskell.com/chapters (русский перевод: Миран Липовача, Изучай Haskell во имя добра! Издательство: ДМК Пресс, 2012)

  • Уилл Курт, Программируй на Haskell, М.:ДМК Пресс, 2019

Дополнительная:

Видео

Видео всех лекций прошлогодней версии курса можно смотреть на канале CS центра на YouTube.

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

Список лекций

Лямбда-исчисление

Введение. Функциональное и императивное программирование. Лямбда-исчисление. Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Эта-преобразование.

Рекурсия и редукция

Теорема о неподвижной точке, Y-комбинатор. Редексы. Одношаговая и многошаговая редукция. Нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Cтратегии редукции. Теорема о нормализации. Механизмы вызова в функциональных языках.

Просто типизированное лямбда-исчисление

Роль типов в языках программирования. Предтермы. Утверждения о типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Свойства типизированного лямбда-исчисления. Связь между системами Карри и Чёрча. Проблемы разрешимости. Сильная и слабая нормализация.

Введение в Haskell

Стандарт языка. Компилятор GHC. Интерпретатор GHCi. Hoogle. Связывание. Кодирование функций. Рекурсия. Основные синтаксические конструкции. Система модулей. Частичное применение, каррирование. Инфиксные операторы: приоритет, ассоциативность, сечения. Бесточечный стиль.

Программирование на языке Haskell

Ошибки. Основание. Строгие и нестрогие функции. Ленивое и энергичное исполнение. Функция seq.

Алгебраические типы данных. Сопоставление с образцом, его семантика. Объявления type и newtype. Метки полей.

Основные функции стандартной библиотеки для работы со списками. Бесконечные списки. Арифметические последовательности. Выделение списков.

Классы типов

Параметрический и специальный полиморфизм. Классы типов. Объявления представителей (instance declaration). Пример: классы Eq и Ord.

Операторы над типами как параметры в определении класса. Класс типов Functor.

Стандартные классы типов: Enum и Bound, Num и его наследники.

Реализация классов типов.

Свертки

Свёртки списков. Правая и левая свёртки. Ленивые и энергичные версии свёрток. Моноиды. Представители класса типов Monoid. Класс типов Foldable. Свойство слияния (fusion law) для свертки.

Аппликативные функторы

Законы для функторов. Класс типов Pointed и законы для него. Класс типов Applicative и его представители. Два способа объявления списка аппликативным функтором.

Использование аппликативных функторов

Аппликативные парсеры. Класс типов Alternative. Класс типов Traversable.

Монады

Монады. Класс типов Monad. Пример: монада Identity. Законы класса типов Monad. do-нотация. Монада Maybe: вычисления, которые могут завершиться неудачей. Монада списка: вычисления со множественными результатами. Класс типов MonadFail.

Вывод типов

Вывод типов. Главный (наиболее общий) тип. Свойства подстановки типов. Композиция подстановок. Унификатор, теорема унификации. Главная пара. Алгоритм Хиндли-Милнера.

Использование монад

Монады для записи в лог, чтения из внешнего окружения и работы с изменяемым состоянием: Reader, Writer, State. Ввод-вывод в чистых языках. Монада IO.

Трансформеры монад

Класс типов MonadPlus. Монада Except. Мультипараметрические классы типов и их использование в mtl. Трансформеры монад в библиотеках transformers и mtl.