Функциональное программирование
Санкт-Петербург, весна 2016
Описание
Курс знакомит слушателей с функциональными языками программирования и методами программирования на этих языках.
Мы рассмотрим отличия функционального подхода к программированию от традиционного императивного, познакомимся с лямбда-исчислением, как теоретической основой функционального программирования, изучим системы типов функциональных языков и алгоритм вывода типов Хиндли-Дамаса-Милнера.
Мы познакомимся с языком программирования Haskell, изучим ленивую и энергичную семантики, алгебраические типы данных и их использование для сопоставления с образцом. Изучая систему типов языка 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)
Дополнительная:
Х. Барендрегт, Ламбда-исчисление, его синтаксис и семантика, М.:Мир, 1985
Филд А., Харрисон П., Функциональное программирование, М.:Мир, 1993
John Harrison, Introduction to Functional Programming http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh-1996/ (русский перевод: http://code.google.com/p/funprog-ru/)
Bryan O’Sullivan, Don Stewart, and John Goerzen, Real World Haskell O’Reilly Media, 2008 http://book.realworldhaskell.org/read/
Simon Peyton Jones, The Implementation of Functional Programming Languages, Prentice Hall, 1987 http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/index.htm
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002 http://www.cis.upenn.edu/bcpierce/tapl (русский перевод: Бенджамин Пирс, Типы в языках программирования, Издательство: Лямбда пресс, Добросвет, 2012 http://starling.rinet.ru/~goga/tapl/tapl.pdf)
Henk Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2), Oxford University Press, 1993
Henk Barendregt, Wil Dekkers, Richard Statman, Lambda Calculus with Types, Cambridge University Press, 2013
Саймон Марлоу. Параллельное и конкурентное программирование на языке Haskell. Издательство: ДМК Пресс, 2014
Simon Marlow and Simon Peyton-Jones. The Glasgow Haskell Compiler. http://www.aosabook.org/en/ghc.html
Алехандро Серано Мена, Изучаем Haskell Издательство: Питер, 2015
Видео
Видео всех лекций прошлогодней версии курса можно смотреть на канале CS центра на YouTube.
Преподаватели
Список лекций
Введение. Функциональное и императивное программирование. Лямбда-исчисление. Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Эта-преобразование. Расширение чистого лямбда-исчисления: дельта-преобразование.
Теорема о неподвижной точке, Y-комбинатор. Редексы. Одношаговая и многошаговая редукция. Нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Cтратегии редукции. Теорема о нормализации. Механизмы вызова в функциональных языках.
Роль типов в языках программирования. Предтермы. Утверждения о типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Свойства типизированного лямбда-исчисления. Связь между системами Карри и Чёрча. Проблемы разрешимости. Сильная и слабая нормализация. Соответствие Карри-Говарда.
Работа с GHCi и GHC. Использование основных синтаксических конструкций языка. Кодирование рекурсивных функций.
Ошибки. Основание. Строгие и нестрогие функции. Ленивое и энергичное исполнение. Функция seq. Алгебраические типы данных. Сопоставление с образцом, его семантика. Объявления type и newtype. Метки полей.
Основные функции стандартной библиотеки для работы со списками. Бесконечные списки. Арифметические последовательности. Выделение списков.
Параметрический и специальный полиморфизм. Классы типов. Объявления представителей (instance declaration). Пример: классы Eq и Ord. Операторы над типами как параметры в определении класса. Класс типов Functor. Стандартные классы типов: Enum и Bound, Num и его наследники. Реализация классов типов.
Свёртки списков. Правая и левая свёртки. Ленивые и энергичные версии свёрток. Моноиды. Представители класса типов Monoid. Класс типов Foldable. Свойство слияния (fusion law) для свертки.
Законы для функторов. Класс типов Pointed и законы для него. Класс типов Applicative и его представители. Два способа объявления списка аппликативным функтором. Класс типов Traversable.
Монады. Класс типов Monad. Пример: монада Identity. Законы класса типов Monad. do-нотация. Монада Maybe: вычисления, которые могут завершиться неудачей. Монада списка: вычисления со множественными результатами.
Монады для записи в лог, чтения из внешнего окружения и работы с изменяемым состоянием: Reader, Writer, State. Ввод-вывод в чистых языках. Монада IO.
Вывод типов. Главный (наиболее общий) тип. Свойства подстановки типов. Композиция подстановок. Унификатор, теорема унификации. Главная пара. Алгоритм Хиндли-Милнера.