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

Программа курса

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

    Лекция

    Введение. Функциональное и императивное программирование.
    Лямбда-исчисление. Применение и абстракция. Свободные и связанные переменные.

    Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки.

    Бета-преобразование. Эта-преобразование. Расширение чистого
    лямбда-исчисления: дельта-преобразование.

    Практика

    Лямбда-исчисление как язык программирования. Булевы значения,
    пары. Каррирование. Числа Чёрча, простейшие операции над ними.

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

    Лекция

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

    Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме,
    единственность нормальной формы.

    Cтратегии редукции. Теорема о нормализации. Механизмы вызова в функциональных языках.

    Практика

    Числа Чёрча: предшествование, вычитание. Примитивная рекурсия. Списки.
    Комбинаторы неподвижной точки Карри и Тьюринга.

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

    Лекция

    Роль типов в языках программирования. Предтермы. Утверждения о
    типизации. Контексты.

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

    Проблемы разрешимости. Сильная и слабая нормализация. Соответствие
    Карри-Говарда.

    Практика

    Вывод типов в системах Карри и Чёрча просто типизированного
    лямбда-исчисления. Незамкнутость просто типизированной системы относительно экспансии.

Введение в Haskell.

    Лекция

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

    Основные синтаксические конструкции. Система модулей.

    Частичное применение, каррирование. Инфиксные операторы, сечения. Бесточечный стиль.

    Практика

    Кодирование рекурсивных функций.

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

    Лекция

    Ошибки. Основание. Строгие и нестрогие функции. Ленивое и энергичное
    исполнение. Функция seq.

    Алгебраические типы данных. Сопоставление с образцом, его семантика.

    Объявления type и newtype. Метки полей.

    Практика

    Списки, стандартные функции для работы с ними. Функции высших порядков.
    "Бесконечные" структуры данных. Генерация (выделение) списков.

Система типов Haskell.

    Лекция

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

    Операторы над типами как параметры в определении класса. Класс типов Functor.

    Реализация классов типов.

    Практика

    Стандартные классы типов: Enum и Bound, Num и его наследники, Show и Read.

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

    Лекция

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

    Моноиды. Представители класса типов Monoid.

    Свёртки списков. Правая и левая свёртки. Ленивые и энергичные версии свёрток.

    Класс типов Foldable.

    Практика

    использование аппликативных функторов и свёрток.

Монады.

    Лекция

    Монады. Класс типов Monad. Пример: монада Identity.

    Законы класса типов Monad. do-нотация.

    Монада Maybe: вычисления, которые могут завершиться неудачей.

    Монада списка: вычисления со множественными результатами.

    Практика

    Программирование с помощью стандартных монад.

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

    Лекция

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

    Практика

    Ввод-вывод. Работа с псевдослучайными величинами.

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

    Лекция

    Класс Alternative. Парсеры регулярных выражений. Класс MonadPlus.

    Монада Error: вычисление, которое может вызвать исключение.

    Монада Cont: управление порядком вычислений.

    Проблема комбинирования монадических эффектов. Трансформеры монад.

    Практика

    Монадические вычисления с множественными эффектами.

Вывод типов.

    Лекция

    Вывод типов. Главный (наиболее общий) тип. Свойства подстановки типов.

    Композиция подстановок.

    Унификатор, теорема унификации. Главная пара. Алгоритм Хиндли-Милнера.

    Практика

    Реализация алгоритма вывода типов на Haskell.

Полиморфные системы типов.

    Лекция

    Сильный и слабый полиморфизм. Let-полиморфизм. Полиморфизм высших рангов.
    Универсальные абстракция и применение. Импредикативность. Сильная нормализация.
    Программирование в полиморфных системах.

    Система с зависимыми типами. Семейства типов. Виды для семейств типов. Тип зависимого произведения.

    Практика

    Обобщенные алгебраические типы данных (GADTs). Экзистенциальные типы.
    Семейства типов в Haskell. Программирование на типах.

Параметричность.

    Лекция

    Параметричность как свойство полиморфных систем. Теорема Рейнольдса.
    Свободные теоремы для полиморфных типов.

    Практика

    Оптимизации с помощью правил переписывания в GHC. Правило fold/build.

Чисто функциональные структуры данных.

    Лекция

    Неизменяемые структуры данных и эффективные алгоритмы для них. Роль
    ленивости.
    Аммортизированная сложность. Зипперы. Список с произвольным доступом
    (flexible array).