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

(НИУ ВШЭ, факультет компьютерных наук, январь – март 2018 г.)

Таблица с результатами проверки домашних заданий и самостоятельной работы.
Если в крайней правой колонке написано "ДЗ проверяется", дождитесь результатов проверки. Если вы заметили какое-либо иное несоответствие, напишите по электронной почте.
Алгоритм вычисления оценок приведён ниже.

22 марта в 9:00 в ауд. 300 те, кто не написал самостоятельную работу, смогут это сделать.

Теория

Термы

λ-термы строятся из переменных и констант с помощью двух конструкций:

Неформально, \((uv)\) означает применение функции \(u\) к аргументу \(v\); в математике и императивных языках программирования чаще обозначается \(u(v)\). Абстракция \(\lambda x.u\) задаёт функцию, возвращающую значение \(u\) при данном значении \(x\).

Символ «λ» связывает переменную \(x\), как кванторы в логике первого порядка. Несвязанные переменные называются свободными. Связанные переменные можно переименовывать. Это преобразование называется α-конверсией: например, \(\lambda x.\lambda y. x =_\alpha \lambda z.\lambda t.z\).

Более содержательное преобразование термов — β-редукция: \( (\lambda x. u) v \to_\beta u[x := v]\). Это преобразование можно применить к любому подтерму вида \((\lambda x . u) v\) — такой подтерм называется редексом. Поэтому иногда бывает, что данный терм можно редуцировать многими способами. Через \(\twoheadrightarrow_\beta\) обозначим рефлексивно-транзитивное замыкание \(\to_\beta\), т.е. применение нескольких (возможно, ни одной) β-редукций.

Конфлюэнтность (свойство Чёрча – Россера). Если \( u \twoheadrightarrow_\beta v_1 \) и \( u \twoheadrightarrow_\beta v_2 \), то существует такой терм \(w\), что \( v_1 \twoheadrightarrow_\beta w \) и \( v_2 \twoheadrightarrow_\beta w \).

Терм \(u\) называется нормальной формой, если к нему нельзя применить ни одну редукцию (в нём нет редексов). Если \(u \twoheadrightarrow_\beta u' \) и \(u'\) является нормальной формой, то \(u'\) называется нормальной формой терма \(u\). В силу свойства Чёрча – Россера, нормальная форма данного терма (если она существует) единственна. Бывают, однако, термы без нормальной формы: например \( (\lambda x . (x x) ) (\lambda x. (x x )) \) редуцируется «петлёй» к себе.

Терм называется слабо нормализуемым (WN), если у него есть нормальная форма. Терм называется сильно нормализуемым (SN), если любая последовательность редукций, начинающаяся с этого терма, приводит к нормальной форме (эквивалентно: граф его редукций конечен и ацикличен).

Типы

Система простых типов. Типы строятся из примитивных (таких как Int, Bool, Char, ...) с помощью одной операции \(\to\); \(A \to B\) означает тип функций из типа \(A\) в тип \(B\).

Разметка термов типами может осуществляться двумя способами. При типизации по Чёрчу (жёсткой) каждой константе и каждой свободной переменной приписан определённый тип, и также опеределённый тип приписывается каждой переменной при λ-абстракции: вместо \(\lambda x . u\) пишем \(\lambda x:A .u \). По индукции теперь можно определить тип любого терма: если \(u\) имеет тип \(B\), то \(\lambda x:A. u \) имеет тип \(A \to B\); если \(u\) имеет тип \(A \to B \) и \(v\) имеет тип \(A\), то \((uv)\) имеет тип \(B\). Если же типы \(u\) и \(v\) несогласованы, то \((uv)\) не считается правильно построенным термом. При типизации по Чёрчу отсутствует всякий полиморфизм: например, тождественная функция \(\mathrm{id} = \lambda x. x\) должна быть своя для каждого типа: \(\lambda x : \mathrm{Int}. x\) типа \(\mathrm{Int} \to \mathrm{Int}\), \(\lambda x : \mathrm{Bool} \to \mathrm{Bool}. x\) типа \( (\mathrm{Bool} \to \mathrm{Bool}) \to (\mathrm{Bool} \to \mathrm{Bool})\) и т.д.

При типизации по Карри сами λ-термы не несут никакой информации о типах. Вместо этого, утверждения вида „терм \(u\) может иметь тип \(A\)“ (записывается \(u:A\)) выводятся (доказываются) в специальном логическом исчислении. Этот процесс называется type inference. Для свободных переменных и констант типы должны быть объявлены в контексте \(\Gamma\) — множестве утверждений вида \(x : B\), где \(x\) — переменная или константа, причём любая \(x\) встречается в \(\Gamma\) не более одного раза. Утверждение „в контексте \(\Gamma\) терм \(u\) может иметь тип \(A\)“ записывается как \(\Gamma \vdash u : A\). Исчисление для type inference в случае простых типов по Карри следующее: \[ \dfrac{(x : B) \in \Gamma}{\Gamma \vdash x : B}\,[\mbox{Var}] \qquad \dfrac{\Gamma \vdash u : (A \to B) \quad \Gamma \vdash v : A}{\Gamma \vdash (uv) : B}\,[\mbox{App}] \qquad \dfrac{\Gamma, x : A \vdash u : B}{\Gamma \vdash (\lambda x . u) : (A \to B)}\,[\mbox{Abs}] \]

Типизация по Карри допускает некоторый уровень полиморфизма: один терм может иметь несколько типов. Например, для \(\mathrm{id} = \lambda x . x\) утверждение \(\vdash (\lambda x . x) : (A \to A) \) (с пустым контекстом) выводится для любого типа \(A\). Таким образом, \(\mathrm{id}\) является полиморфной тождественной функцией, применимой к объекту любого типа.

Безопасность типов: если \(\Gamma \vdash u_1 : A \) и \( u_1 \twoheadrightarrow_\beta u_2 \), то \( \Gamma \vdash u_2 : A \). Иначе говоря, β-редукция не может испортить типы.

Теорема. Если \(\Gamma \vdash u : A \) для некоторого контекста \(\Gamma\) и некоторого типа \(A\), то терм \(u\) обладает свойством SN. Иначе говоря, всякий типизуемый терм сильно нормализуем.

Система типов 2-го порядка (λ2, система F). В этой системе добавляется ещё один конструктор типов: квантор всеобщности \(\forall\). Теперь типы строятся из примитивных типов и переменных по типам (обозначаются α, β, ...) следующим образом: если \(A\) и \(B\) — типы, а \(\alpha\) — переменная по типам, то \(A \to B\) и \(\forall \alpha. A \) — типы. Квантор \(\forall\) задаёт полиморфный тип: например, \((\lambda x . x) : \forall \alpha. (\alpha \to \alpha)\).

Громадная (даже чрезмерная) выразительная сила системы λ2 проистекает из того, что конструкции с \(\forall\) можно дальше использовать в построении типов. Например, в этой системе оказывается типизуемым терм \(\lambda x. (x x) : \forall \alpha . (\alpha \to \alpha) \to \forall \alpha . (\alpha \to \alpha) \). Действительно, если \(x\) имеет тип \(\forall \alpha . (\alpha \to \alpha) \), т.е. обозначает функцию, действующую на объект любого типа \(\alpha\) и возвращающую значение также типа \(\alpha\), то его можно применить к самому себе, получив значение того же типа, что и \(x\), т.е. \( \forall \alpha. (\alpha \to \alpha) \). Правила вывода типов в λ2 таковы: \[ \dfrac{(x : B) \in \Gamma}{\Gamma \vdash x : B}\,[\mbox{Var}] \qquad \dfrac{\Gamma \vdash u : (A \to B) \quad \Gamma \vdash v : A}{\Gamma \vdash (uv) : B}\,[\mbox{App}] \qquad \dfrac{\Gamma, x : A \vdash u : B}{\Gamma \vdash (\lambda x . u) : (A \to B)}\,[\mbox{Abs}] \] \[ \dfrac{\Gamma \vdash u : A}{\Gamma \vdash u : (\forall \alpha. A)}\, [\mbox{Gen}] \qquad \dfrac{\Gamma \vdash u : (\forall. \alpha A)}{\Gamma \vdash u : A[\alpha := B]} \, [\mbox{Inst}] \]

Как ни странно, система λ2 сохраняет свойство SN для всех типизуемых в ней термов (J.-Y. Girard). В частности, терм \((\lambda x. (xx))(\lambda x. (xx))\) в ней не типизуем. Однако, с другой стороны, проблема типизуемости (вывода типа) для данного терма в этой системе алгоритмически неразрешима (J. B. Wells). Это означает, что при использовании λ2 интерпретатор функционального языка не сможет сам восстановить типы, и их придётся явно указывать.

В Haskell систему типов 2-го порядка можно использовать с помощью ключа RankNTypes: 

{-# LANGUAGE RankNTypes #-}

lxx :: (forall a . a -> a) -> (forall a . a -> a)
lxx = \x -> (x x) 

lxx2 :: (forall b . (b->b) -> (b->b)) -> (forall b. (b->b) -> (b->b))
lxx2 = \x -> (x x)

dup = \f -> \x -> f (f x)
Заметим, что здесь мы определили две разных версии \(\lambda x . (x x)\) с разными типами. Эти типы несравнимы: один нельзя получить из другого подстановкой типов (хотя кажется, что второй тип — это «частный случай» первого). К функции dup, выведенный тип которой: (t -> t) -> t -> t, применим только lxx2, но не lxx.

Выражение lxx2 dup (+2) 3 даёт 11. Действительно, dup означает «примени данную функцию дважды»; lxx2 dup применяет dup к самой себе, и означает «примени функцию четырежды». Значит, мы 4 раза применяем операцию «+2» к числу 3.

Система типов Хиндли – Милнера. TBA

Теоретические задачи

  1. Постройте λ-терм с бесконечным графом β-редукций.
  2. Постройте слабо, но не сильно нормализуемый λ-терм.
  3. Постройте λ-термы \(u_1\) и \(u_2\), такие что \(u_1 \to_\beta u_2\), при этом \(u_2\) типизируем в простом типовом λ-исчислении (по Карри), а \(u_1\) — нет.
  4. Постройте замкнутый λ-терм, типизуемый типом \((A \to (B \to C)) \to (A \to B) \to (A \to C)\).
  5. С помощью алгоритма W выведите наиболее общий тип для терма \( \mathbf{let}\ z = \lambda f. \lambda x. f (f\, x)\ \mathbf{in}\ z\, z \) в системе типов Хиндли — Милнера.
  6. Выведите наиболее общий тип для терма \( \mathbf{let}\ y = \lambda f. f (y\, f)\ \mathbf{in}\ y\) в системе типов Хиндли – Милнера с рекурсивным \(\mathbf{let}\).

Практика

Элементы функционального программирования в нефункциональных языках

C/C++

Функция сортировки из стандартной библиотеки C принимает в качестве аргумента другую функцию — сравнения двух элементов: 
void qsort(void *base, size_t nmemb, size_t size,
                  int (*compar)(const void *, const void *));
Для использования qsort нужно создать функцию compar, сравнивающую два объекта.

Python

bigrams = {"AB": [10, 11, 12], "BC": [5, -5, 8], "CD": [105, 1, 0], 
           "DE": [6, 6], "EF": [15, 20, 15], "FG": [22, 11, 32], 
           "GH": [20, 20, 20]}
sorter = sorted(bigrams, key=lambda key: sum(bigrams[key]), reverse=True)

for key in sorter:
    print(key, bigrams[key])
Здесь функция, осуществляющая сравнение двух значений для сортировки (точнее, для вычисления ключа сортировки: вместо сравнения элементов \(u_i\) и \(u_j\), мы сначала вычисляем целочисленные ключи \(k(u_i)\) и \(k(u_j)\), а потом сравниваем уже их — этот способ, хотя и менее общий, более эффективен), определена непосредственно при вызове алгоритма сортировки (sorted) с помощью ключевого слова lambda. В математической нотации, \(\lambda x. v\), где \(v\) — выражение, содержащее переменную \(x\), означает функцию, по данному значению \(x\) вычисляющую \(v\).

Посмотрим на следующий код: 

x=5
f=lambda y : y+x
print f(2)
x=7
print f(2)
Значение f(2) изменилось: действительно, lambda создаёт новую безымянную функцию, которая, помимо своего аргумента y имеет также неявный доступ к переменной x. Меняется значение x — меняется поведение f.

Таким образом, переменные-функции ведут себя не совсем так, как обычные переменные: в следующем примере значение f, конечно, не поменяется: 

x=5
f=x+2
print f
x=7
print f

В Haskell эта трудность решена радикально: изменять значение x запрещено.

Списки и бесконечные списки в Haskell

Для любого типа a Haskell умеет определять тип [a], населённый списками из элементов типа a. Например, "abc" имеет тип String, а ["abc", "de", "efgh"] — тип [String]. Операция (:) :: a -> [a] -> [a] приписывает элемент к списку слева: 1 : [2,3] даёт [1,2,3]. Таким образом, список «растёт» влево. Заметим, что элементы списка должны быть одного типа. Например, [1,"abc"] некорректен. Тип [a] рекурсивен: всякий список есть либо [] (пустой список), либо x : xs, где x — объект типа x («голова» списка), а xs — типа [x] («хвост»). Значит, функцию на списках можно определить разбором этих двух случаев, причём во втором случае её можно применить рекурсивно к xs. Для примера рассмотрим два алгоритма сортировки (простой рекурсивный алгоритм и сортировку слияниями): 
sort [] = []
sort [z] = [z]
sort (x : xs) = if (head(sort xs) >= x) then x : sort xs else head(sort xs) : sort (x : tail xs)


halve x = splitAt (length x `div` 2) x

merge xs [] = xs
merge [] ys = ys
merge (x : xs) (y : ys) = if (x < y) then (x : (merge xs (y:ys))) else (y : (merge (x:xs) ys))

mergesort [] = []
mergesort [z] = [z]
mergesort xs = merge (mergesort (fst (halve xs))) (mergesort (snd (halve xs)))
Пример с решетом Эратосфена: 
sieve [] = []
sieve (p : xs) = p : sieve [ x | x <- xs, x `mod` p /= 0 ]
primes = sieve [2..]
(на самом деле с точки зрения эффективности это совсем не решето Эратосфена)

List comprehension — довольно мощное средство. Иногда можно программировать так, как будто пишешь математический текст: 

primes = [ p | p <- [2..100], all (\y -> (p `mod` y /= 0)) [2..p-1] ]
perfect = [ p | p <- [2..], p == sum [ y | y <- [1..p-1], p `mod` y == 0 ] ]

Ограничение допустимых типов: 

rmnb :: (Num t, Show t) => t -> String
rmnb n = "Room number " ++ (show n)
rmnb нельзя теперь применить к нечисловому типу (напр., [...])

Домашнее задание № 1

Срок сдачи: 3 февраля (23:59 МСК)
  1. Фибоначчи. Постройте бесконечный список, состоящих из всех чисел Фибоначчи в порядке их следования. (Последовательность Фибоначчи \((F_n)_{n=1}^{\infty}\) задаётся рекурсивно: \(F_1 = F_2 = 1\), \(F_{n} = F_{n-1} + F_{n-2}\) для \(n \geqslant 3\).)
  2. Фибоняччи. Постройте бесконечный список слов “nya”, “nya”, “nyanya”, “nyanyanya”, “nyanyanyanyanya”, “nyanyanyanyanyanyanyanya”, ...: число слогов “nya” в \(n\)-м слове равно \(n\)-му числу Фибоначчи, \(F_n\).
  3. FizzBuzz. Постройте бесконечный список строк: n-я строка есть "Fizz", если n делится на 3, но не на 5; "Buzz", если n делится на 5, но не на 3; "FizzBuzz", если n делится на 15; представляет собой десятичную запись числа n в остальных случаях.
  4. Постройте функцию decsplit :: Integral t => t -> [t], превращающую число в список его десятичных знаков (например, decsplit 256 даёт [6, 5, 2]).
  5. Алгоритм Луна для проверки корректности номеров банковских карт работает следующим образом: Постройте функцию luhn :: Integral t => t -> Bool, проверяющее данное число на корректность по алгоритму Луна.
  6. Перестановки. а) Постройте функцию interleave :: a -> [a] -> [[a]], такую что interleave x ys даёт список всех вставок x в список ys (например, interleave 5 [2,34,10] даст [[5,2,34,10],[2,5,34,10],[2,34,5,10],[2,34,10,5]]).
    б) Постройте функцию permutations :: [a] -> [[a]], порождающую список всех перестановок данного списка (например, permutations [1,2,3] даст [[1,2,3],[2,1,3],[2,3,1],[1,3,2],[3,1,2],[3,2,1]]).
  7. Последовательность Туэ — Морса определяются следующим образом. Задан алфавит из двух букв \(\{a,b\}\). Первая итерация последовательности есть слово \(a\). Каждая следующая итерация \(u_{n+1}\) получается из предыдущей \(u_n\) как \(u_n \, \bar{u}_n\), где \(\bar{v}\) означает слово \(v\), в котором все \(a\) заменены на \(b\) и наоборот. Например, \( u_3 = abba \), \( u_4 = abbabaab \) и т.д.
    а) Постройте функцию thue :: Integral t => t -> String, такую что thue n даёт \(u_n\)
    б) Легко видеть, что каждое следующее слово \(u_{n+1}\) в последовательности Туэ — Морса содержит все предыдущие как начальные отрезки. Следовательно, можно рассмотреть бесконечное слово, получающееся как объединение всех \(u_k\). Постройте его как объект thue_infinite :: String.

Домашнее задание № 2

Срок сдачи: 17 февраля (23:59 МСК)
  1. Определите функцию saynumber :: Integer -> String, для чисел от 0 до 999 999 возвращающую их запись на русском языке (например, “сто двадцать пять тысяч четыреста пятнадцать” для 125 415). (Для корректного вывода кириллицы можно использовать Text.Show.Unicode или, как более простое решение, putStrLn.)
  2. Постройте функцию hamming, вычисляющую расстояние Хэмминга между двумя списками, т.е. число позиций, в которых они различаются. Предполагается, что списки имеют равную длину.
  3. Постройте функцию gray :: Num a => a -> [[Bool]], выдающую для данного \(n\) код Грея: такое упорядочение всех \(2^n\) последовательностей из \(n\) битов, что соседние последовательности отличаются только одним битом.
  4. Ориентированный граф можно задать список его дуг как пар вершин (например, [(1,2),(2,3),(1,3),(3,4),(4,2),(5,6)])). Определите функцию paths :: a -> a -> [(a,a)] -> [[a]], выдающую все пути из одной данной вершины в другую (например, paths 1 4 [(1,2),(2,3),(1,3),(3,4),(4,2),(5,6)] даёт [[1,2,3,4],[1,3,4]]).
  5. Определите функцию, выдающую список компонент связности данного неориентированного графа.
  6. Постройте список queens всех расстановок ферзей на шахматной доске 8×8 так, чтобы он не били друг друга. (Например, в этом списке будет элемент [1,5,8,6,3,7,2,4].)
  7. В присутствии {-# LANGUAGE RankNTypes #-} определите функцию applyToTuple так, чтобы applyToTuple length ("hello",[1,2,3]) давало результат (5,3).

Домашнее задание № 3

Срок сдачи: 26 марта (23:59 МСК)
  1. Игра «Ним». В эту игру играют двое. Изначально имеется 3 кучки камней. Ходят по очереди. За один ход можно взять любое количество камней, но только из одной кучки. Выигрывает тот, кто заберёт последний камень. Нужно написать программу, которая интерактивно играет против человека: сначала вводятся три натуральных числа (количества камней в кучках изначально); первым ходит программа, затем человек (он должен ввести номер кучки и количество камней, которое он забирает) и т.д. В конце программа сообщает, кто выиграл.

    Подсказка о выигрывающей стратегии: для определения выигрывающей позиции вычисляют так называемую ним-сумму, записывая количества камней в кучках в двоичной системе и применяя поразрядно операцию «исключающее ИЛИ» (XOR). Если ним-сумма оказалась равной 0, то позиция проигрышная: либо камней нет вообще, либо любой ход приведёт к позиции с ненулевой ним-суммой. А вот позиция с ненулевой ним-суммой выигрышная: из неё всегда есть ход, переводящий её в позицию с ним-суммой, равной 0. (Как найти этот ход, остаётся в качестве упражнения.)

  2. Регулярные выражения и конечные автоматы. Регулярным выражением называется формула, составленная из символов некоторого алфавита (у нас — объектов типа Char) и пустого слова \(\varepsilon\) с помощью операций \(\cdot\) (конкатенация), \(+\) («или»), \({}^*\) (итерация). Каждое регулярное выражение задаёт некоторое множество слов. Например, \(a \cdot (a+b)^* \cdot b\) задаёт все слова из букв \(a\) и \(b\), начинающиеся на \(a\) и заканчивающиеся на \(b\).

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

    data RegExp = Char
        | Con RegExp RegExp
        | Uni RegExp RegExp
        | Eps
        | Ite RegExp
    Задача заключается в том, чтобы написать программу, проверяющую данное слово на соответствие регулярному выражению: checkregexp :: RegExp -> String -> Bool.

    Для этого предлагается сначала построить по регулярному выражению недетерминированный конечный автомат (NFA), а потом запустить его на данном входном слове.

    NFA — это набор \(\langle Q, \Sigma, \delta, q_0, F \rangle\), где \(Q\) — множество состояний, среди которых выделено начальное \(q_0\) и множество допускающих состояний \(F\), \(\Sigma\) — алфавит, в котором задано слово, а \(\delta \colon \Sigma \to (Q \to \mathcal{P}(Q))\) — функция перехода, по данному входному символу переводящая текущее состояние во множество состояний, в которые можно их него перейти (это и есть недетерминизм). Автомат принимает данное слово \(a_1\dots a_n\), если есть хотя бы один путь \( q_0 \to q_1 \to q_2 \to \ldots \to q_n \), такой что \( q_i \in \delta (a_i) (q_{i-1})\) и \(q_n \in F \).

    Как мы видим, здесь появляется монада \(\mathcal{P}(Q)\) множества всех подмножеств данного множества \(Q\). Грубым приближением её является монада списка [Q]. Таким образом реализован, например, недетерминизм ходов коня в примере с ходом коня из LearnYouAHaskell: 

    -- from "Learn you a Haskell"

-- Motto: [a] is a monad for non-determinism

-- import Control.Monad


-- add monoid structure
class Monad m => MonadPlus m where  
    mzero :: m a  
    mplus :: m a -> m a -> m a  

instance MonadPlus [] where  
    mzero = []  
    mplus = (++)  

guard :: (MonadPlus m) => Bool -> m ()  
guard True = return ()  
guard False = mzero

-- example:
--    [1..10] >>= \x -> guard (x `mod` 3 == 0) >> return x

type KnightPos = (Int,Int)  

moveKnight :: KnightPos -> [KnightPos]  
moveKnight (c,r) = do  
    (c',r') <- [(c+2,r-1),(c+2,r+1),(c-2,r-1),(c-2,r+1)  
               ,(c+1,r-2),(c+1,r+2),(c-1,r-2),(c-1,r+2)  
               ]  
    guard (c' `elem` [1..8] && r' `elem` [1..8])  
    return (c',r')  

in3 :: KnightPos -> [KnightPos]  
in3 start = do   
    first <- moveKnight start  
    second <- moveKnight first  
    moveKnight second  

canReachIn3 :: KnightPos -> KnightPos -> Bool  
canReachIn3 start end = end `elem` in3 start  


-- inMany :: Int -> KnightPos -> [KnightPos]  
-- inMany x start = return start >>= foldr (<=<) return (replicate x moveKnight)

inMany2 1 start = moveKnight start
inMany2 n start = inMany2 (n-1) start >>= moveKnight
      
inMany3 1 start = moveKnight start
inMany3 n start = do
     first <- inMany3 (n-1) start
     moveKnight first
  

canReachIn :: Int -> KnightPos -> KnightPos -> Bool  
canReachIn x start end = end `elem` inMany2 x start
    Такая реализация NFA, однако, будет неэффективной: после нескольких шагов автомата в списке может оказаться несколько копий одного состояния (по одной для каждого пути), и потребуется экспоненциально много времени. Поэтому правильнее использовать монаду Set.

Вычисление оценки за курс

Ссылки

Учебники

(To be continued...)

Теоретическая литература