Функциональное программирование
Новосибирск, весна 2018
Описание
Курс знакомит слушателей с функциональными языками программирования и методами программирования на этих языках.
Мы рассмотрим отличия функционального подхода к программированию от традиционного императивного, познакомимся с лямбда-исчислением, как теоретической основой функционального программирования, изучим системы типов функциональных языков и алгоритм вывода типов Хиндли-Дамаса-Милнера.
Мы познакомимся с языком программирования Haskell, изучим ленивую и энергичную семантики, алгебраические типы данных и их использование для сопоставления с образцом. Изучая систему типов языка Haskell, мы обсудим параметрический и специальный полиморфизм и, в частности, механизм классов типов.
Мы изучим основные классы типов из стандартной библиотеки Haskell, в том числе функторы, аппликативные функторы и монады. Мы обсудим различные стратегии свертки и обхода списков, деревьев и познакомимся с обобщением этих операций в классах типов Foldable и Traversable.
Мы научимся программировать, используя стандартные монады, в частности обсудим проблему ввода-вывода в чистых языках и его реализацию в Haskell с помощью монады IO, а также работу с изменяемым состоянием с помощью монады State и родственных ей монад.
Формат курса
Курс проводится в интенсивном формате и разделён на две неравные части. Первая часть (9 занятий по 4 академических часа в вечернее время) пройдёт с 30 января по 8 февраля, воскресенье выходной. Вторая часть курса (еще 4 занятия) запланирована на апрель.
Критерии выставления оценок за курс
Всего за выполнение домашних заданий, курсовой работы и тестирования можно заработать 151 балл.
Оценка “отлично” выставляется тем, кто наберет 90% баллов и более (136 баллов). Оценка “хорошо” - тем, кто наберет 75% баллов (113 баллов). Оценка “удовлетворительно” (“зачет”) - тем, кто наберет 50% баллов (75 баллов).
Точное количество баллов может слегка измениться, поэтому скрупулезным студентам рекомендуется следить за процентами.
Литература
Основная:
Miran Lipovača, Learn You a Haskell for Great Good! A Beginner’s Guide, 2011 (русский перевод: Миран Липовача, Изучай Haskell во имя добра! Издательство: ДМК Пресс, 2012)
Vitaly Bragilevsky, Haskell in Depth, Manning Publications, 2019
Дополнительная:
общетеоретические книги по ФП:
Х. Барендрегт, Ламбда-исчисление, его синтаксис и семантика, М.:Мир, 1985
Филд А., Харрисон П., Функциональное программирование, М.:Мир, 1993
John Harrison, Introduction to Functional Programming (русский перевод)
Simon Peyton Jones, The Implementation of Functional Programming Languages, Prentice Hall, 1987
книги о языке Haskell:
Will Kurt, Get Programming with Haskell, Manning Publications, 2018, 616 pages
Richard Bird, Thinking Functionally with Haskell, Cambridge University Press, 2014, 344 pages
Bryan O’Sullivan, Don Stewart, and John Goerzen, Real World Haskell O’Reilly Media, 2008
книги про типы:
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002 (русский перевод: Бенджамин Пирс, Типы в языках программирования, Издательство: Лямбда пресс, Добросвет, 2012)
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.
Алехандро Серано Мена, Изучаем Haskell Издательство: Питер, 2015
Хороший обзор самых новых англоязычных книг про Haskell сделал Виталий Николаевич Брагилевский. Общие итоги доступны здесь и далее по ссылкам на обзоры конкретных книг.
Видео
Видео всех лекций курса версии 2015 года можно смотреть на канале CS центра на YouTube.
Преподаватели
Список лекций
Введение. Функциональное и императивное программирование. Лямбда-исчисление. Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Эта-преобразование. Расширение чистого лямбда-исчисления: дельта-преобразование.
Теорема о неподвижной точке, Y-комбинатор. Редексы. Одношаговая и многошаговая редукция. Нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Cтратегии редукции. Теорема о нормализации. Механизмы вызова в функциональных языках.
Роль типов в языках программирования. Предтермы. Утверждения о типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Свойства типизированного лямбда-исчисления. Связь между системами Карри и Чёрча. Проблемы разрешимости. Сильная и слабая нормализация. Соответствие Карри-Говарда.
Стандарт языка. Компилятор GHC. Интерпретатор GHCi. Hoogle. Связывание. Кодирование функций. Рекурсия. Основные синтаксические конструкции. Система модулей. Частичное применение, каррирование. Инфиксные операторы: приоритет, ассоциативность, сечения. Бесточечный стиль.
Ошибки. Основание. Строгие и нестрогие функции. Ленивое и энергичное исполнение. Функция seq
.
Алгебраические типы данных. Сопоставление с образцом, его семантика. Объявления type
и newtype
. Метки полей.
Основные функции стандартной библиотеки для работы со списками. Бесконечные списки. Арифметические последовательности. Выделение списков.
Параметрический и специальный полиморфизм. Классы типов. Объявления представителей (instance declaration). Пример: классы Eq
и Ord
.
Операторы над типами как параметры в определении класса. Класс типов Functor
.
Стандартные классы типов: Enum
и Bound
, Num
и его наследники.
Реализация классов типов.
Свёртки списков. Правая и левая свёртки. Ленивые и энергичные версии свёрток. Моноиды. Представители класса типов Monoid
. Класс типов Foldable
. Свойство слияния (fusion law) для свертки.
Законы для функторов. Класс типов Pointed
и законы для него. Класс типов Applicative
и его представители. Два способа объявления списка аппликативным функтором.
Аппликативные парсеры. Класс типов Alternative
. Класс типов Traversable
.
Монады. Класс типов Monad
. Пример: монада Identity
. Законы класса типов Monad
. do
-нотация. Монада Maybe
: вычисления, которые могут завершиться неудачей. Монада списка: вычисления со множественными результатами.
Монады для записи в лог, чтения из внешнего окружения и работы с изменяемым состоянием: Reader
, Writer
, State
. Ввод-вывод в чистых языках. Монада IO
.
Класс типов MonadPlus
. Монада Except
. Мультипараметрические классы типов и их использование в mtl. Трансформеры монад в библиотеках transformers и mtl.
Вывод типов. Главный (наиболее общий) тип. Свойства подстановки типов. Композиция подстановок. Унификатор, теорема унификации. Главная пара. Алгоритм Хиндли-Милнера.