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

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

Описание

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

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

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

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

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

Литература

Основная:

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

  • Алехандро Серано Мена, Изучаем Haskell Издательство: Питер, 2015

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

Видео

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

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

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

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

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

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

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

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

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

Введение в Haskell

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

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

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

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

Классы типов

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

Свертки

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

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

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

Монады

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

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

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

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

Родственники моноидов: Alternative и MonadPlus. Мультипараметрические классы типов. Монады для обработки исключений. Трансформеры монад.

Вывод типов

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