# Функциональное программирование в языке Haskell

## Ссылка на курс для CSC:

Описание и программа: https://compscicenter.ru/courses/func-prog/2022-spring/

Записи лекций: https://www.youtube.com/playlist?list=PLlb7e2G7aSpTDub2LFDVBvvjWj-53Gfuh

## Описание

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

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

Практическая часть курса ориентирована на изучении языка программирования Haskell. Студенты знакомятся с ленивой и энергичной версиями операционной семантики, алгебраическими типами данных и их использованием для реализации механизма сопоставления с образцом. При изучении системы типов языка Haskell будут обсуждаться параметрический и специальный полиморфизм и, в частности, механизм классов типов, в том числе многопараметрических.

Подробно рассматриваются основные классы типов из стандартной библиотеки Haskell, в том числе полугруппы и моноиды с одной стороны, и функторы, аппликативные функторы и монады с другой. Также обсуждаются различные стратегии свертки и обхода списков, деревьев и обобщение этих стратегий в классах типов Foldable и Traversable.

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

## Программа

**1. $\lambda$-исчисление.** Функциональная модель вычислений. Чистое $\lambda$-исчисление. Подстановка и редукция.

**2. Рекурсия и редукция.** Теорема о неподвижной точке. Нормальная форма. Теорема Чёрча-Россера. Cтратегии редукции.

**3. Просто типизированное $\lambda$-исчисление.** Понятие типа. Просто типизированное $\lambda$-исчисление. Свойства просто типизированных систем.

**4. Введение в Haskell.** Язык Haskell. Основы программирования. Базовые типы. Операторы и их сечения.

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

**6. Классы типов.** Образцы и типы данных: дополнительные сведения. Классы типов. Стандартные классы типов.

**7. Свертки и развертки.** Свертки списков. Развертки и оптимизации. Полугруппы и моноиды. Класс типов Foldable.

**8. Аппликативные функторы.** Функторы. Класс типов Pointed. Аппликативные функторы.

**9. Использование аппликативных функторов.** Аппликативные парсеры. Класс типов Alternative. Класс типов Traversable.

**10. Монады.** Класс типов Monad. Монада Identity. Монада Maybe. Класс типов MonadFail. Список как монада.

**11. Использование монад.** Монада Reader: чтение из окружения. Монада Writer: запись в лог. Монада State: изменяемое состояние. Монада IO: ввод-вывод.

**12. Трансформеры монад.** Классы Alternative и MonadPlus. Монады с обработкой ошибок. Мультипараметрические классы типов. Трансформеры монад. Трансформер MaybeT.

**13. Вывод типов.** Главный тип. Подстановка типа и унификация. Теорема Хиндли-Милнера. let-полиморфизм и типы высших рангов.

## Лекции и семинары

**Лекция 1.** Лямбда-исчисление

**Семинар 1.** Чистое лямбда-исчисление как язык программирования

**Лекция 2.** Рекурсия и редукция

**Семинар 2.** Рекурсия и редукция

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

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

**Лекция 4.** Введение в Haskell

**Семинар 4.** Введение в Haskell

**Лекция 5.** Типы данных

**Семинар 5.** Стандартные списки

**Лекция 6.** Классы типов

**Семинар 6.** Реализация представителей стандартных классов типов

**Лекция 7.** Свертки

**Семинар 7.** Моноиды и свертки

**Лекция 8.** Аппликативные функторы

**Семинар 8.** Аппликативные функторы

**Лекция 9.** Использование аппликативных функторов

**Семинар 9.** Траверсы, парсеры, моноидальные функторы

**Лекция 10.** Монады

**Семинар 10.** Монады

**Лекция 11.** Использование монад

**Семинар 11.** Использование монад

**Лекция 12.** Трансформеры монад

**Семинар 12.** Трансформеры монад

**Лекция 13.** Вывод типов

## Критерии и методы выставления оценок за курс

Оценка отлично выставляется тем, кто наберет 90% баллов и более за выполнение домашних заданий, курсовой работы и тестирования. Оценка хорошо - тем, кто наберет 75% баллов. Оценка удовлетворительно (зачет) - тем, кто наберет 50% баллов. Большая часть баллов набирается слушателями в процессе прохождения приватного курса на платформе Stepik, разработанного специально для этого курса.

## Литература

### Основная:

- Miran Lipovača, Learn You a Haskell for Great Good! A Beginner’s Guide 2011 (русский перевод: Миран Липовача, Изучай Haskell во имя добра! Издательство: ДМК Пресс, 2012)
- Уилл Курт, Программируй на Haskell, М.:ДМК Пресс, 2019
- Vitaly Bragilevsky, Haskell in Depth, Manning Publications, 2020

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

- Барендрегт Х., Ламбда-исчисление, его синтаксис и семантика, М.:Мир, 1985
- Филд А., Харрисон П., Функциональное программирование, М.:Мир, 1993
- John Harrison, Introduction to Functional Programming
- Simon Peyton Jones, The Implementation of Functional Programming Languages,Prentice Hall, 1987
- Simon Marlow and Simon Peyton-Jones. The Glasgow Haskell Compiler.
- Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002 (русский перевод: Бенджамин Пирс, Типы в языках программирования, Издательство: Лямбда пресс, Добросвет, 2012)
- Sorensen M. H., Urzyczyn P. Lectures on the Curry-Howard Isomorphism. — Elsevier, 2006.
- 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