Функциональное программирование
Санкт-Петербург, весна 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
Дополнительная:
Х. Барендрегт, Ламбда-исчисление, его синтаксис и семантика, М.:Мир, 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
Саймон Марлоу. Параллельное и конкурентное программирование на языке Haskell. Издательство: ДМК Пресс, 2014
Simon Marlow and Simon Peyton-Jones. The Glasgow Haskell Compiler. http://www.aosabook.org/en/ghc.html
Видео
Видео всех лекций курса можно смотреть на страницах лекций или на канале CS центра на YouTube.
Преподаватели
Список лекций
Введение. Функциональное и императивное программирование. Лямбда-исчисление. Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Эта-преобразование. Расширение чистого лямбда-исчисления: дельта-преобразование.
Теорема о неподвижной точке, Y-комбинатор. Редексы. Одношаговая и многошаговая редукция. Нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Cтратегии редукции. Теорема о нормализации. Механизмы вызова в функциональных языках.
Роль типов в языках программирования. Предтермы. Утверждения о типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Свойства типизированного лямбда-исчисления. Связь между системами Карри и Чёрча. Проблемы разрешимости. Сильная и слабая нормализация. Соответствие Карри-Говарда.
Стандарт языка. Компилятор GHC. Интерпретатор GHCi. Hoogle. Связывание. Кодирование функций. Рекурсия. Основные синтаксические конструкции. Система модулей. Частичное применение, каррирование. Инфиксные операторы, сечения. Бесточечный стиль.
Ошибки. Основание. Строгие и нестрогие функции. Ленивое и энергичное исполнение. Функция 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. Мультипараметрические классы типов. Монады для обработки исключений. Трансформеры монад.
Вывод типов. Главный (наиболее общий) тип. Свойства подстановки типов. Композиция подстановок. Унификатор, теорема унификации. Главная пара. Алгоритм Хиндли-Милнера.