Основная

1. Миран Липовача. Изучай Haskell во имя добра! - М.:ДМК Пресс, 2017.
2. Уилл Курт. Программируй на Haskell - М.:ДМК Пресс, 2019.
3. Бенжамин Пирс. Типы в языках программирования. M.: “Лямбда-пресс”: “Добросвет”, 2014.

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

1. Алехандро Серано Мена. Изучаем Haskell - СПб:Питер, 2015.
2. Ричард Бёрд. Жемчужины проектирования алгоритмов - М.:ДМК Пресс, 2013.
3. Душкин Р. В. Функциональное программирование на языке Haskell. — М.: ДМК Пресс, 2006
4. Душкин Р. В. Справочник по языку Haskell. — М.: ДМК Пресс, 2008

• Противопоставляется императивному программированию
• вычисление – последовательное изменение состояний

• Формальная основа ФП – λ-исчисление
• описывает абстрактное вычисление на основе функций
• близок к формализму частично-рекурсивных функций
• Формальная основа ИП – напр. машины Тьюринга, Поста

• Ключевое отличие математической функции от понятия “функции” в императивных языках – отсутствие “побочных эффектов”.
• Следствие: результат вычисления функции зависит только от значений аргументов
• абсолютно “чистый” функциональный подход – “бесполезен” по причине невозможности ввода-вывода
• Разные языки решают эту проблему по-разному

• функциональный подход в общем случае может быть менее эффективен из-за накладных расходов
• следует отметить, что иногда функциональные алгоритмы – более эффективны
• ФП часто приводит к более простому, ёмкому, читаемому и поддерживаемому коду
• гораздо лучше подходит для высокопараллельных вычислений (как следствие отсутствия неявного состояния)

Хаскелл Брукс Карри (1900-1982)

Некоторые возможности:

• взаимодействие с кодом на других языках программирования
• многозадачное и параллельное программирование
• средства автоматического тестирования
• средства отладки и профилирования
• более 10 тысяч библиотек с открытым исходным кодом

• Исторический предшественник – Miranda (1985 Дэвид Тёнрер)
• К 1987 году – около 15 различных чистых функциональных языков с ленивыми вычислениями, большинство из которых были проприетарными
• В 1987 году образован комитет для разработки открытого стандарта

• Первая версия Haskell 1.0, 1990 год
• Стабильная версия стандарта, Haskell 98 – 1998 год
• Исправления и дополнения Haskell 98 – 2003 год
• Новая версия Haskell 2010
• Де факто версия – Haskell 2010 + расширения

• Основной (фактически единственный) компилятор – GHC (Glasgow Haskell Compiler)
• “новая” лицензия BSD
• много расширений языка

Экосистема

• Компилятор GHC
• Интерпретатор и отладчик GHCi
• Системы сборки проектов и разрешения зависимостей
  • cabal-install
  • stack
• Библиотека пакетов Hackage

• Вопрос с IDE – несколько болезненный. Основной вариант: haskell-language-server + редактор
  • VSCode
  • Sublime Text
  • Vim
  • Emacs
  • Kakoune
  • Atom (*)

• λ-исчисление является наиболее простым исчислением, реализующим эти концепции
• все значения – либо функциональные абстракции, либо переменные.

Cинтаксис

1. Переменная – маленькие латинские буквы, напр. x.
2. Лямбда-абстракция. Анонимная функциональная абстракция. Обозначается символом λ, переменной-параметром, точкой, затем произвольным термом – “телом”, напр. λx. x
3. Применение – два терма, разделённых пробелом. Применение левого терма к правому терму. Напр. (λx. x) y. Правый терм будем называть аргументом.

• В случае неоднозначности, будем использовать скобки для разделения термов.
• Переменные в теле λ-абстракции, являющиеся параметрами, называются связанными переменными. Прочие – свободными.
• Терм без свободных переменных называется замкнутым; замкнутые термы называют также комбинаторами.

\(α\)-эквивалентность

• Название связанных переменных может быть произвольным
• Два лямбда-терма, одинаковые с точностью до переименования связанных переменных, называются α-эквивалентными
• Например:
  • λx. x
  • λy. y
  • λz. z
  • являются α-эквивалентными
  • λx. y
  • λy. x
  • не являются α-эквивалентными

\(β\)-редукция

• Применение по правилу: вместо применения подставляется результат замены всех вхождений связанной переменной в теле на значение аргумента

• Формально:

  (λx. t₁) t₂ → [x → t₂] t₁

  • t₁, t₂ – произвольные лямбда-термы, а выражение в квадратных скобках означает замену в следующем терме.

• Терм, к которому применима β-редукция – редекс (redex, reducible expression).

(λx. x) (λy. y)

  [x → (λy. y)]x
= (λy. y)

Стратегии вычисления

• Вычисление λ-терма – применение β-редукции, пока это возможно
• Стратегии определяют последовательность
• Будем называть термы, к которым (в соответствии с выбранной стратегией) нельзя применить β-редукцию термами в нормальной форме

Рассмотрим типовые стратегии на примере терма

(λx. x) ((λy. y) (λz. (λw. w) z))

или для простоты

id (id (λz. id z))

где id обозначает комбинатор идентичности, id = λx. x.

Полная β-редукция

• Любой редекс может сработать на любом шаге.

(λx. x) ((λy. y) (λz. (λw. w) z))

→ (λx. x) ((λy. y) (λz. [w → z]w))

= (λx. x) ((λy. y) (λz. z))

→ [x → ((λy. y) (λz. z))]x

= (λy. y) (λz. z)

→ [y → (λz. z)]y

= λz. z

Нормальный порядок вычислений

• Сначала обрабатывается самый левый, самый внешний редекс.

  (λx. x) ((λy. y) (λz. (λw. w) z))

→ [x → ((λy. y) (λz. (λw. w) z))]x

= (λy. y) (λz. (λw. w) z)

→ [y → (λz. (λw. w) z)] y

= λz. (λw. w) z

→ λz. [w → z]w

= λz. z

Вызов по имени

• нормальный порядок вычислений
• запрещает проводить редукцию внутри абстракций
• Соответствует модели “ленивых” (нестрогих) вычислений

  (λx. x) ((λy. y) (λz. (λw. w) z))

→ [x → ((λy. y) (λz. (λw. w) z))]x

= (λy. y) (λz. (λw. w) z)

→ [y → (λz. (λw. w) z)]y

= λz. (λw. w) z

• Используется в
  • ALGOL
  • Haskell (строго говоря “вызов по необходимости”)

Вызов по значению

• в большинстве языков программирования
• Модель “нетерпеливых” (строгих) вычислений
• нормальный порядок
• сокращаются только внешние редексы (не находящиеся внутри абстракций)
• правая часть которых в нормальной форме

  (λx. x) ((λy. y) (λz. (λw. w) z))

→ (λx. x) ([y → (λz. (λw. w) z)]y)

= (λx. x) (λz. (λw. w) z)

→ [x → (λz. (λw. w) z)]x

= λz. (λw. w) z

Функции нескольких аргументов

• Рассмотрим вложенную абстракцию вида

  λx. λy. λz. (x y) (x z)

• При последовательном применении

  (((λx. λy. λz. (x y) (x z)) u) v) w

  получим

  (u v) (u w)

• семантически эквивалентно применению функции 3 аргументов к 3 аргументам.

• Для удобства, введём сокращённое обозначение:

  λx y …. t ≡ λx. λy. … t

• условимся, что оператор применения лево-ассоциативен, т.е.

  t₁ t₂ … tₙ ≡ ((t₁ t₂) …) tₙ

Булевские константы Чёрча

• Определим:

  tru ≡ λx y. x
  fls ≡ λx y. y

• Пусть tru – “истина”, а fls – “ложь”

• Тогда определим комбинатор

• ifThenElse = λc t f. c t f

• функция 3 аргументов

• если с ≡ tru, ifThenElse c t f → t

• если с ≡ fls, ifThenElse c t f → f

• ifThenElse почти ничего не делает – его поведение закодировано в tru и fls.

• Не составляет труда определить логические функции, например, конъюнкция

  and = λx y. x y fls

• Упражнение вывести выражения для or, not, xor.

Пары

• можно закодировать пары значений в виде термов. Введём определения

  pair = λf s. λb. b f s
  fst = λp. p tru
  snd = λp. p fls

• Определение pair записано в таком виде, чтобы подчеркнуть, что применение pair к двум аргументам возвращает функцию.

fst (pair u v)

= (λp. p tru) ((λf s. λb. b f s) u v)

→ (λp. p tru) (λb. b u v)

→ (λb. b u v) tru

→ tru u v

= (λx y. x) u v

→ u

Числа Чёрча

Стандартная конструкция натуральных чисел – числа Чёрча – выглядит следующим образом:

c₀ ≡ λs z. z
c₁ ≡ λs z. s z
c₂ ≡ λs z. s (s z)
c₃ ≡ λs z. s (s (s z))
...

• Число n кодируется комбинатором двух аргументов cₙ,

• принимает “функцию следования” s и “ноль” z

• n раз применяет s к z.

• В кодировании Чёрча, число n – функция, которая что-то делает n раз.

succ = λn. λs z. s (n s z)

• Упражнение предложить другое (не α-эквивалентное) определение для succ.

plus = λm n. λs z. m s (n s z)

times = λm n. λs z. m (n s) z

• Упражнение определите plus и times через succ и plus соответственно
• Упражнение выведите терм для возведения в степень.

iszero = λn. n (λx. fls) tru

• вычитание чисел Чёрча – достаточно нетривиально
• “хитрая” функция предшествования с парами чисел, такими, что на каждом шаге применения функции следования, предыдущее число сохраняется как элемент пары:

zz = pair c₀ c₀
ss = λnn. pair (snd nn) (succ (snd nn))
pred = λn. fst (n ss zz)

• при таком определении, pred c₀ → c₀
• несложно изменить поведение для поддержки, например, целых чисел (т.е. включая отрицательные).

• Упражнение определите функцию вычитания чисел Чёрча используя функцию pred
• Упражнение определите функцию проверки чисел Чёрча на равенство.

Рекурсия

• для некоторых термов нормальной формы может не существовать
• Самый простой пример – расходящийся комбинатор

Ω = (λx. x x) (λx. x x)

• содержит только один редекс
• один шаг β-редукции снова приводит нас к Ω:

  (λx. x x) (λx. x x)
→ [x → (λx. x x)](x x)
= (λx. x x) (λx. x x)

• термы не имеющие нормальной формы – расходятся
• Ω можно обобщить до более полезного комбинатора – комбинатора неподвижной точки, который позволяет использовать рекурсию:

fix = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

• достаточно сложная структура с повторами

• Смысл достаточно прост:

• мы хотим ввести рекурсию, то есть возможность пользоваться конструкциями вида

  f = <тело, содержащее f>

• Для этого собственно и используется комбинатор fix:

  f = fix (λf. <тело, содержащее f>)

• Функция факториала
• Одна итерация может быть записана как

fact1 = λf. λn. ifThenElse (iszero n) c₁ (times n (f (pred n)))

• здесь f – рекурсивный вызов.
• Используя fix, можем записать функцию факториала как

fact = fix fact1

fact1 = λf. λn. ifThenElse (iszero n) c₁ (times n (f (pred n)))

fact = fix fact1

  fact c₂

= fix fact1 c₂

= (λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))) fact1 c₂

→ (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) c₂

→ fact1 (λy. (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) y) c₂

= fact1 (λz. (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) z) c₂

→ ... →
times c₂ ((λz. (λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) z) c₁)

→ times c₂ ((λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) c₁)

→ ... →
times c₂ (times c₁ ((λx. fact1 (λy. x x y)) (λx. fact1 (λy. x x y)) c₀))

→ ...
→ times c₂ (times c₁ c₁)

→ ...
→ c₂