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

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

Описание

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

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

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

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

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

Литература

Основная:

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

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

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

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

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

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

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

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

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

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

Введение в Haskell

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

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

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

Классы типов

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

Свёртки

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

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

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