or ‘Game.Left’,
imported from ‘Game’ at Loop. hs:5:1-11
(and originally defined at Game. hs:10:25-28)
Loop. hs:47:28:
Ambiguous occurrence ‘Left’
...
...
Failed, modules loaded: Game.
*Game>
По ошибкам видно, что произошёл конфликт имён. Конструкторы Left и Right уже определены в Prelude.
Это конструкторы типа Either. Давайте скроем их, добавим в модуль такую строчку:
import Prelude hiding (Either(.. ))
Пятнашки | 209
Теперь проверим:
*Game> :r
[2 of 2] Compiling Loop
( Loop. hs, interpreted )
Ok, modules loaded: Game, Loop.
*Loop>
Всё работает, можно двигаться дальше.
Последние штрихи
В модуле Loop нам осталось определить несколько маленьких функций. Поиск по слову un говорит нам
о том, что осталось определить функции “
greetings
:: IO ()
readInt
:: String -> Maybe Int
showAsk
:: IO ()
Самая простая это функция showAsk, она приглашает игрока сделать ход:
showAsk :: IO ()
showAsk = putStrLn ”Ваш ход: ”
Теперь функция распознавания целого числа:
import Data.Char (isDigit)
...
readInt :: String -> Maybe Int
readInt n
| all isDigit n = Just $ read n
| otherwise
= Nothing
В первой альтернативе мы с помощью стандартной функции isDigit :: Char -> Bool проверяем, что
строка состоит из одних только чисел. Если все символы числа, то мы пользуемся функцией из модуля Read
и читаем целое число, иначе возвращаем Nothing.
Последняя функция, это функция приветствия. Когда игрок входит в игру он сталкивается с её результа-
тами. Определим её так:
-- в модуль Loop
greetings :: IO ()
greetings = putStrLn ”Привет! Это игра пятнашки” >>
showGame initGame >>
remindMoves
-- в модуль Game
initGame :: Game
initGame = un
Сначала мы приветствуем игрока, затем показываем состояние (initGame), к которому ему нужно стре-
миться, и напоминаем как делаются ходы. На этом определении мы раскрыли все выражения в модуле Loop,
нам остался лишь модуль Game.
Правила игры
Определим модуль Game, но мы будем определять его не с чистого листа. Те функции, которые нам нуж-
ны уже определились в ходе описания диалога с пользователем. Нам нужно уметь составлять начальное
состояние initGame, уметь составлять перемешанное состояние игры shuffle, нам нужно уметь реагиро-
вать на ходы move, определять какая позиция является выигрышной isGameOver и уметь показывать фишки
в красивом виде. Приступим!
initGame
:: Game
shuffle
:: Int -> IO Game
isGameOver
:: Game -> Bool
move
:: Move -> Game -> Game
instance Show Game where
show = un
Таков наш план.
210 | Глава 13: Поиграем
Начальное состояние
Начнём с самой простой функции, составим начальное состояние:
initGame :: Game
initGame = Game (3, 3) $ listArray ((0, 0), (3, 3)) $ [0 .. 15]
Мы будем кодировать фишки цифрами от нуля до 14, а пустая клетка будет равна 15. Это просто согла-
шения о внутреннем представлении фишек, показывать мы их будем совсем по-другому.
С этим значением мы можем легко определить функцию определения конца игры. Нам нужно только
добавить deriving (Eq) к типу Game. Тогда функция isGameOver примет вид:
isGameOver :: Game -> Bool
isGameOver = ( == initGame)
Делаем ход
Напишем функцию:
move :: Move -> Game -> Game
Она обновляет позицию после хода. В пятнашках не во всех позициях доступны все ходы. Если пустышка
находится на краю, мы не можем вывести её за пределы доски. Это необходимо как-то учесть. Каждый ход
задаёт направление обмена фишками. Если у нас есть текущее положение пустышки и ход, то по ходу мы
можем узнать направление, а по направлению ту фишку, которая займёт место пустышки после хода. При
этом нам необходимо проверять находится ли та фишка, которую мы хотим поместить на пустое место в пре-
делах доски. Например если пустышка расположена в самом верху и мы хотим сделать ход Up (передвинуть
её ещё выше), то положение игры не должно измениться.
import Prelude hiding (Either(.. ))
newtype Vec = Vec (Int, Int)
move :: Move -> Game -> Game
move m (Game id board)
| within id’ = Game id’ $ board // updates
| otherwise
= Game id board
where id’ = shift (orient m) id
updates = [(id, board ! id’), (id’, emptyLabel)]
-- определение того, что индексы внутри доски
within :: Pos -> Bool
within (a, b) = p a && p b
where p x = x >= 0 && x <= 3
-- смещение положение по направдению
shift :: Vec -> Pos -> Pos
shift (Vec (va, vb)) (pa, pb) = (va + pa, vb + pb)
-- направление хода
orient :: Move -> Vec
orient m = Vec $ case m of
Up
-> (-1, 0)
Down
-> (1 , 0)
Left
-> (0 , -1)
Right
-> (0 , 1)
-- метка для пустой фишки
emptyLabel :: Label
emptyLabel = 15
Маленькие функции within, shift, orient, emptyLabel делают как раз то, что подписано в комментариях.
Думаю, что их определение не сложно понять. Но есть одна тонкость, поскольку в функции orient мы поль-
зуемся конструкторами Left и Right необходимо спрятать тип Either из Prelude. Мы ввели дополнительный
тип Vec для обозначения смещения, чтобы случайно не подставить вместо него индексы.
Разберёмся с функцией move. Сначала мы вычисляем положение фишки, которая пойдёт на пустое место
id’. Мы делаем это, сместив (shift) положение пустышки (id) по направлению хода (orient a).
Мы обновляем массив, который описывает доску с помощью специальной функции //. Посмотрим на её
тип:
Пятнашки | 211
(//) :: Ix i => Array i a -> [(i, a)] -> Array i a
Она принимает массив и список обновлений в этом массиве. Обновления представлены в виде пары
индекс-значение. В охранном выражении мы проверяем, если индекс перемещаемой фишки в пределах дос-
ки, то мы возвращаем новое положение, в котором пустышка уже находится в положении id’ и массив об-
новлён. Мы составляем список обновлений updates bз двух элементов, это перемещения фишки и пустышки.
Если же фишка за пределами доски, то мы возвращаем исходное положение.
Перемешиваем фишки
Игра начинается с такого положения, в котором все фишки перемешаны. Но перемешивать фишки про-
извольным образом было бы не честно, поскольку известно, что в пятнашках половина расстановок не при-
водит к выигрышу. Поэтому мы будем перемешивать так: мы стартуем из начального положения и делаем
несколько ходов произвольным образом. Количество ходов определяет сложность игры:
shuffle :: Int -> IO Game
shuffle n = (iterate (shuffle1 =<< ) $ pure initGame) !! n
shuffle1 :: Game -> IO Game
shuffle1 = un
Функция shuffle1 перемешивает фишки один раз. С помощью функции iterate мы строим список рас-
становок, которые мы получаем на каждом шаге перемешивания. В самом конце мы выбираем из списка
n-тую позицию. Обратите внимание на то, что мы не можем просто написать:
iterate shuffle1 initGame
Так у нас не совпадут типы. Для функции iterate нужно чтобы вход и выход функции имели одинаковые
типы. Поэтому мы пользуемся в функции iterate методами классов Monad и Applicative (глава 6).
Теперь определим функцию shuffle1. Мы делаем ход в текущей позиции, который мы выбрали случай-
ным образом из списка доступных ходов. Выбором случайного элемента из списка, будет заниматься функция
randomElem, а функция nextMoves будет возвращать список доступных ходов для данного положения:
shuffle1 :: Game -> IO Game
shuffle1 g = flip move g <$> (randomElem $ nextMoves g)
randomElem :: [a] -> IO a
randomElem = un
nextMoves :: Game -> [Move]
nextMoves = un
Нам осталось определить всего две функции, и всё готово для игры. Определим выбор случайного эле-
мента из списка:
import System.Random
...
randomElem :: [a] -> IO a
randomElem xs = (xs !! ) <$> randomRIO (0, length xs - 1)
Мы генерируем случайное число в диапазоне индексов списка и затем извлекаем элемент. Теперь функ-
ция определения ходов в текущем положении:
nextMoves g = filter (within . moveEmptyTo . orient) allMoves
where moveEmptyTo v = shift v (emtyField g)
allMoves = [Up, Down, Left, Right]
Мы выполняем схожие операции с теми, что были в функции move. Мы фильтруем из списка всех ходов
те, что выводят пустую фишку за пределы доски.
212 | Глава 13: Поиграем
Отображение положения
Я немного поторопился, нам осталась ещё одна функция. Это отображение позиции. Я не буду подробно
останавливаться на теле функции, скажу лишь то, что она составляет строку так как это показано в коммен-
тарии к функции.
--
+----+----+----+----+
--
|
1 |
2 |
3 |
4 |
--
+----+----+----+----+
--
|
5 |
6 |
7 |
8 |
--
+----+----+----+----+
--
|
9 | 10 | 11 | 12 |
--
+----+----+----+----+
--
| 13 | 14 | 15 |
|
--
+----+----+----+----+
--
instance Show Game where
show (Game _ board) = ”\n” ++ space ++ line ++
(foldr (\a b -> a ++ space ++ line ++ b) ”\n” $ map column [0 .. 3])
where post id = showLabel $ board ! id
showLabel n
= cell $ show $ case n of
15 -> 0
n
-> n+1
cell ”0”
= ”
”
cell [x]
= ’ ’:’ ’: x :’ ’:[]
cell [a,b] = ’ ’: a : b :’ ’:[]
line = ”+----+----+----+----+\n”
nums = ((space ++ ”|”) ++ ) . foldr (\a b -> a ++ ”|” ++ b) ”\n” .
map post
column i = nums $ map (\x -> (i, x)) [0 .. 3]
space = ”\t”
Теперь мы можем загрузить модуль Loop в интерпретатор и набрать play. Немного отвлечёмся и поигра-
ем.
Prelude> :l Loop
[1 of 2] Compiling Game
( Game. hs, interpreted )
[2 of 2] Compiling Loop
( Loop. hs, interpreted )
Ok, modules loaded: Loop, Game.
*Loop> play
Привет! Это игра пятнашки
+----+----+----+----+
|
1 |
2 |
3 |
4 |
+----+----+----+----+
|
5 |
6 |
7 |
8 |
+----+----+----+----+
|
9 | 10 | 11 | 12 |
+----+----+----+----+
| 13 | 14 | 15 |
|
+----+----+----+----+
Возможные ходы пустой клетки:
left
или l
-- налево
right
или r
-- направо
up
или u
-- вверх
down
или d
-- вниз
Другие действия:
new int
или n int -- начать новую игру, int - целое число,
указывающее на сложность
quit
или q
-- выход из игры
Начнём новую игру?
Укажите сложность (положительное целое число):
5
+----+----+----+----+
|
1 |
2 |
3 |
4 |
+----+----+----+----+
|
5 |
6 |
7 |
8 |
+----+----+----+----+
Пятнашки | 213
|
9 |
| 10 | 11 |
+----+----+----+----+
| 13 | 14 | 15 | 12 |
+----+----+----+----+
Ваш ход:
r
+----+----+----+----+
|
1 |
2 |
3 |
4 |
+----+----+----+----+
|
5 |
6 |
7 |
8 |
+----+----+----+----+
|
9 | 10 |
| 11 |
+----+----+----+----+
| 13 | 14 | 15 | 12 |
+----+----+----+----+
Ваш ход:
r
+----+----+----+----+
|
1 |
2 |
3 |
4 |
+----+----+----+----+
|
5 |
6 |
7 |
8 |
+----+----+----+----+
|
9 | 10 | 11 |
|
+----+----+----+----+
| 13 | 14 | 15 | 12 |
+----+----+----+----+
Ваш ход:
d
+----+----+----+----+
|
1 |
2 |
3 |
4 |
+----+----+----+----+
|
5 |
6 |
7 |
8 |
+----+----+----+----+
|
9 | 10 | 11 | 12 |
+----+----+----+----+
| 13 | 14 | 15 |
|
+----+----+----+----+
Игра окончена.
Ураа, получилось. Мы так долго писали программу, проверяя лишь типы, и в самом конце, когда мы
закончили определение, всё работает. Конечно не всё работает так гладко, я уже написал эту программу и
объясняю готовое решение, но когда общая схема программы утряслась, возможные ошибки определяются
на раз. Мы могли вызвать отображение позиции не в том порядке или забыть проверку конца игры, всё это
несколько строчек изменений.
Самые неприятные ошибки происходят, когда в середине выясняется, что мы ошиблись с типами. Типы,
которые мы выбрали не могут описать явление, возможно мы не можем делать какие-то операции, которые
нам, как неожиданно выяснилось, очень нужны. Это значит, что нужно менять каркас. Менять каркас, это
значит сносить весь дом и строить новый. Возможно разрушения окажутся локальными, мы строим не дом,
а город. И сносить придётся не всё, а несколько кварталов. Но это тоже большие перемены. Поэтому шаг
определения типов очень важен. Впрочем сносить кварталы в Haskell одно удовольствие, посольку стоит
нам изменить какой-нибудь тип, например убрать какой-нибудь тип или изменить имя, компилятор тут же
подскажет нам какие функции стали бессмысленными. Более коварные изменения связаны с добавлением
конструктора-альтернативы. Например нам вдруг не понравился тип Bool и мы решили сделать его более
человечным. Мы решили добавить ещё одно значение:
data Bool = True | False | IDonTKnow
Это может привести к неполному рассмотрению альтернатив в case-выражениях и сопоставлениях с об-
разцом в аргументах функции. Такие ошибки крайн неприятны, поскольку они происходят на этапе выпол-
нения программы, когда новое значение IDonTKnow дойдёт до case. В этом случае нам на выручку может
прийти функция свёртки, если мы вместе с типом изменим и функцию свёртки, это скажется на всех функ-
циях, которые были определены через неё. Чем больше таких функций, тем больше ошибок мы поймаем.
214 | Глава 13: Поиграем
13.3 Упражнения
• Измените диалог с пользователем. Сделайте так чтобы у игры было главное меню, в котором игрок
выбирает разные побочные функции, вроде выхода, начать новую игру, подсказка и игровое меню, в
котором игрок только передвигает фишки. Когда игрок собирает игру он попадает в главное меню.
• Добавьте в игру подсчёт статистики. Если игрок дошёл до победной позиции он узнаёт за сколько ходов
ему удалось решить задачу. Также ведётся история предыдущих попыток, по которой пользователь
может следить как изменяются его результаты.
• Подумайте можно ли выделить интерфейс игры в отдельный класс так, чтобы модуль Loop не зависел
от конкретной реализации игры. Чтобы можно было, опираясь на абстрактные методы, вроде show для
Game, или реакции на ход, вести диалог с пользователем. Попробуйте переписать игру пятнашки с
помощью такого класса.
• Попробуйте написать другую игру, например игру раскладывания пасьянса, крестики-нолики или
шашки, не меняя модуля Loop. Так чтобы вы сделали необходимые экземпляры для классов из преды-
дущего упражнения, а всё остальное поведение следовало из них.
Упражнения | 215
Глава 14
Лямбда-исчисление
В этой главе мы узнаем о лямбда-исчислении. Лямбда-исчисление описывает понятие алгоритма. Ещё
до появления компьютеров в 30-е годы двадцатого века математиков интересовал вопрос о возможности со-
здания алгоритма, который мог бы на основе заданных аксиом дать ответ о том верно или нет некоторое
логическое высказывание. Например у нас есть базовые утверждения и логические связки такие как “и”,
“или”, “для любого из”, “существует один из”, с помощью которых мы можем строить из базовых высказы-
ваний составные. Некоторые из них окажутся ложными, а другие истинными. Нам интересно узнать какие.
Но для решения этой задачи прежде всего необходимо было понять а что же такое алгоритм?
Ответ на этот вопрос дали Алонсо Чёрч (Alonso Church) и Алан Тьюринг (Alan Turing). Чёрч разработал
лямбда-исчисление, а Тьюринг теорию машин Тьюринга. Оказалось, что задача автоматического определе-
ния истинности формул в общем случае не имеет решения.
В основе лямбда-исчисление лежит понятие функции. Мы можем составлять сложные функции из про-
стейших, а также подставлять в функции аргументы, которые могут быть как константами так и другими
функциями. Как только мы составили выражение мы можем передать его вычислителю. Он подставляет ар-
гументы в функции и возвращает такое выражение, в котором невозможно далее проводить подстановки
аргументов. Этот процесс проведения подстановок считается вычислением алгоритма.
В рамках теории машин Тьюринга алгоритм описывается по-другому. Машина Тьюринга имеет внут-
реннее состояние, Состояние содержит некоторое значение, которое изменяется по ходу работы машины.
Машина живёт не сама по себе, она читает ленту символов. Лента символов – это большая цепочка букв.
На каждую букву машина реагирует серией действий. Она может изменить значение состояния, обновить
букву в ленте или перейти к следующему или предыдущему символу. Есть состояния, которые обозначают
конец работы, они называются терминальными. Как только машина дойдёт до терминального состояния мы
считаем, что вычисление алгоритма закончилось. После этого мы можем считать результат из состояний
машины.
Функциональные языки программирования основаны на лямбда-исчислении. Поэтому мы будем гово-
рить именно об этом описании алгоритма.
14.1 Лямбда исчисление без типов
Составление термов
Можно считать, что лямбда исчисление это такой маленький язык программирования. В нём есть множе-
ство символов, которые считаются переменными, они что-то обозначают и неделимы. В лямбда-исчислении
программный код называется термом. Для написания программного кода у нас есть всего три правила:
• Переменные x, y, z … являются термами.
• Если M и N – термы, то ( MN) – терм.
• Если x – переменная, а M – терм, то ( λx. M) – терм
В формальном описании добавляют ещё одно правило, оно говорит о том, что других термов нет. Первое
правило, говорит о том, что у нас есть алфавит символов, который что-то обозначает, эти символы явля-
ются базовыми строительными блоками программы. Второе и третье правила говорят о том как из базовых
элементов получаются составные. Второе правило – это правило применения функции к аргументу. В нём
M обозначает функцию, а N обозначает аргумент. Все функции являются функциями одного аргумента, но
они могут принимать и возвращать функции. Поэтому применение трёх аргументов к функции F un будет
выглядеть так:
216 | Глава 14: Лямбда-исчисление
((( F un Arg 1) Arg 2) Arg 3)
Третье правило говорит о том как создавать функции. Специальный символ лямбда ( λ) в выражении
( λx. M ) говорит о том, что мы собираемся определить функцию с аргументом x и телом функции M . С та-
кими функциями мы уже сталкивались. Это безымянные функции. Приведём несколько примеров функций.
Начнём с самого простого, определим тождественную функцию:
( λx. x)
Функция принимает аргумент x и тут же возвращает его в теле. Теперь посмотрим на константную функ-
цию:
( λx. ( λy. x))
Константная функция является функцией двух аргументов, поэтому наш терм принимает переменную
x и возвращает другой терм функцию ( λy. x). Эта функция принимает y, а возвращает x. В Haskell мы бы
написали это так:
\x -> (\y -> x)
Точка сменилась на стрелку, а лямбда потеряла одну ножку. Теперь определим композицию. Композиция
принимает две функции одного аргумента и направляет выход второй функции на вход первой:
( λf. ( λg. ( λx. ( f ( gx)))))
Переменные f и g – это функции, которые участвуют в композиции, а x это вход результирующей функ-
ции. Уже в таком простом выражении у нас пять скобок на конце. Давайте введём несколько соглашений,
которые облегчат написание термов:
Пишем
Подразумеваем
Опустим внешние скобки:
λx. x
( λx. x)
В применении группируем скобки
f ghx
(( f g) h) x
влево:
Ф функциях группируем скобки
λx. λy. x
( λx. ( λy. x))
вправо:
Пишем функции нескольких
λxy. x
( λx. ( λy. x))
аргументов с одной лямбдой:
С этими соглашениями мы можем переписать терм для композиции так:
λf gx. f ( gx)
Сравните с выражением на языке Haskell:
\f g x -> f (g x)
Выражения очень похожи. Haskell иногда называют засахаренной версией лямбда исчисления. В лямбда-
исчислении мы не будем ставить пробелы для применения аргументов к функции. Мы будем считать, что
все имена однобуквенные. При этом переменные мы будем писать с маленькой буквы, а составные термы с
большой.
Определим ещё несколько функций. Например так выглядит функция flip:
λf xy. f yx
Или можно записать в более явном виде, выделим функцию двух аргументов:
λf. λxy. f yx
Определим функцию on, она принимает функцию двух аргументов ∗ и функцию одного аргумента f, а
возвращает функцию двух аргументов, в которой к аргументам сначала применяется функция f, а затем они
передаются в функцию ∗:
λ ∗ f. λx. ∗ ( f x)( f x)
В лямбда-исчислении есть только префиксное применение поэтому мы написали ∗( fx)( fx) вместо при-
вычного ( fx) ∗ ( fx). Здесь операция ∗ это не только умножение, а любая бинарная функция.
Лямбда исчисление без типов | 217
Абстракция
Функции в лямбда-исчислении называют абстракциями. Мы берём терм M и параметризуем его по пе-
ременной x в выражении λx.M. При этом если в терме M встречается переменная x, то она становится свя-
занной. Например в терме λx.λy.x$ Переменная x является связанной, но в терме λy.x, она уже не связана.
Такие переменные называют свободными. Множество связанных переменных терма M мы будем обозначать
BV ( M )$ от англ. bound variables, а множество свободных переменных мы будем обозначать F V ( M ) от англ.
free variables.
На интуитивном уровне процесс абстракции заключается в том, что мы смотрим на несколько частных
случаев и видим в них что-то общее. Это общее мы выделяем в функцию, которая параметризована частно-
стями. Например мы видим выражения:
λx. + xx,
λx. ∗ xx
И в том и в другом у нас есть функция двух аргументов + или ∗ и мы делаем из неё функцию одного
аргумента. Мы можем абстрагировать (параметризовать) это поведение в такую функцию:
λb. λx. bxx
На Haskell мы бы записали это так:
\b -> \x -> b x x
Редукция. Вычисление термов
Процесс вычисления термов заключается в подстановке аргументов во все функции. Выражения вида:
( λx. M ) N
Заменяются на
M [ x = N ]
Эта запись означает, что в терме M все вхождения x заменяются на терм N. Этот процесс называется
редукцией терма. А выражения вида ( λx. M) N называются редексами. Проведём к примеру редукцию терма:
( λb. λx. bxx) ∗
Для этого нам нужно в терме ( λx. bxx) заменить все вхождения переменной b на переменную ∗. После
этого мы получим терм:
λx. ∗ xx
В этом терме нет редексов. Это означает, что он вычислен или находится в нормальной форме.
α-преобразование
При подстановке необходимо следить за тем, чтобы у нас не появлялись лишние связывания переменных.
Например рассмотрим такой редекс:
( λxy. x) y
После подстановки за счёт совпадения имён переменных мы получим тождественную функцию:
λy. y
Переменная y была свободной, но после подстановки стала связанной. Необходимо исключить такие
случаи. Поскольку с ними получается, что имена связанных переменных в определении функции влияют на
её смысл. Например смысл такого выражения
( λxz. x) y
После подстановки будет совсем другим. Но мы всего лишь изменили обозначение локальной перемен-
ной y на z. И смысл изменился, для того чтобы исключить такие случаи пользуются переименованием пе-
ременных или α-преобразованием. Для корректной работы функций необходимо следить за тем, чтобы все
переменные, которые были свободными в аргументе, остались свободными и после подстановки.
218 | Глава 14: Лямбда-исчисление
β-редукция
Процесс подстановки аргументов в функции называется β-редукцией. В редексе ( λx. M) N вместо свобод-
ных вхождений x в M мы подставляем N. Посмотрим на правила подстановки:
x[ x = N ]
⇒ N
y[ x = N ]
⇒ y
( P Q)[ x = N ]
⇒ ( P [ x = N] Q[ x = N])
( λy. P )[ x = N ] ⇒ ( λy. P [ x = N ]) ,
y /
∈ F V ( N)
( λx. P )[ x = N ] ⇒ ( λx. P )
Первые два правила определяют подстановку вместо переменных. Если переменная совпадает с той, на
место которой мы подставляем терм N, то мы возвращаем терм N, иначе мы возвращаем переменную:
x[ x = N ] ⇒ N
y[ x = N ] ⇒ y
Подстановка применения термов равна применению термов, в которых произведена подстановка:
( P Q)[ x = N ] ⇒ ( P [ x = N ] Q[ x = N ])
При подстановке в лямбда-функции необходимо учитывать связность переменных. Если переменная ар-
гумента отличается от той переменной на место которой происходит подстановка, то мы заменяем в теле
функции все вхождения этой переменной на N:
( λy. P )[ x = N ] ⇒ ( λy. P [ x = N ]) ,
y /
∈ F V ( N)
Условие y / ∈ F V ( N) означает, что необходимо следить за тем, чтобы в N не оказалось свободной пере-
менной с именем y, иначе после подстановки она окажется связанной. Если такая переменная в N всё-таки
окажется мы проведём α-преобразование в терме $ λy. M и заменим y на какую-нибудь другую переменную.
В последнем правиле мы ничего не меняем, поскольку переменная x оказывается связанной. А мы про-
водим подстановку только вместо свободных переменных:
( λx. P )[ x = N ] ⇒ ( λx. P )
Отметим, что не любой терм можно вычислить, например у такого терма нет нормальной формы:
( λx. xx)( λx. xx)
На каждом шаге редукции мы будем вновь и вновь возвращаться к исходному терму.
Стратегии редукции
В главе о ленивых вычислениях нам встретились две стратегии вычисления выражений. Это вычисление
по имени и вычисление по значению. Также там мы узнали о том, что ленивые вычисления это улучшенная
версия вычисления по имени, в которой аргументы функций вычисляются не более одного раза.
Эти стратегии вычисления пришли из лямбда-исчисления. Если нам нужно избавиться от всех редексов
в выражении, то с какого редекса лучше начать? В вычислении по значению ( аппликативная стратегия) мы
начинаем с самого левого редекса, который не содержит других редексов, то есть с самого маленького подвы-
ражения. А в вычислении по имени ( нормальная стратегия) мы начинаем с самого левого внешнего редекса.
Левый редекс означает, что в записи выражения он находится ближе всех к началу выражения.
Теорема (Карри) Если у терма есть нормальная форма, то последовательное сокращение самого левого
внешнего редекса приводит к ней.
Эта теорема говорит о том, что стратегия вычисления по имени может вычислить все термы, которые
имеют нормальную форму. В том, что вычисление по значению может не справиться с некоторыми такими
термами мы можем на следующем примере:
( λxy. x) z (( λx. xx)( λx. xx))
Этот терм имеет нормальную форму z несмотря на то, что мы передаём вторым аргументом в констант-
ную функцию терм, у которого нет нормальной формы. Алгоритм вычисления по значению зависнет при
вычислении второго аргумента. В то время как алгоритм вычисления по имени начнёт с самого внешнего
терма и там определит, что второй аргумент не нужен.
Ещё один важный результат в лямбда-исчислении был сформулирован в следующей теореме:
Лямбда исчисление без типов | 219
Теорема (Чёрча-Россера) Если терм X редуцируется к термам Y 1 и Y 2, то существует терм L, к которому
редуцируются и терм Y 1 и терм Y 2.
Эта теорема говорит о том, что у терма может быть только одна нормальная форма. Поскольку если бы
их было две, то существовал третий терм, к которому можно было бы редуцировать эти нормальные формы.
Но по определению нормальной формы, мы не можем её редуцировать. Из этого следует, что нормальные
формы должны совпадать.
Теорема Чёрча-Россера указывает на способ сравнения термов. Для того чтобы понять равны термы или
нет, необходимо привести их к нормальной форме и сравнить. Если термы совпадают в нормальной форме,
значит они равны.
Рекурсия. Комбинатор неподвижной точки
В лямбда-исчислении все функции являются безымянными. Это означает, что мы не можем в теле функ-
ции вызвать саму функции, ведь мы не можем на неё сослаться, кажется, что у нас нет возможности строить
рекурсивные функции. Однако это не так. Нам на помощь придёт комбинатор неподвижной точки. По опре-
делению комбинатор неподвижной точки решает задачу: для терма F найти терм X такой, что
F X = X
Существует много комбинаторов неподвижной точки. Рассмотрим Y -комбинатор:
Y = λf. ( λx. f ( xx))( λx. f ( xx))
Убедимся в том, что для любого терма F , выполнено тождество: F ( Y F ) = Y F :
Y F = ( λx. F ( xx))( λx. F ( xx)) = F ( λx. F ( xx))( λx. F ( xx)) = F ( Y F ) Так с помощью Y -комбинатора можно составлять рекурсивные функции.
Кодирование структур данных
Вы наверное заметили, что пока мы составляли лишь обобщённые функции. Эти функции комбинируют
другие функции, они не выполняют никаких действий над элементами. Что если нам захочется вычислять
логические значения или воспользоваться числами?
Оказывается, что логические значения, числа, пары, списки и другие конструкции могут быть закодиро-
ваны с помощью термов лямбда-исчисления. Тезис Чёрча утверждает, что с помощью лямбда-терма можно
представить любую вычислимую числовую функцию. В 1936 году Чёрч с помощью лямбда-исчисления дока-
зал существование неразрешимых проблем в теории чисел. Из этого следовала неразрешимость арифметики
и неразрешимость исчисления логики предикатов первого порядка. Система аксиом называется разрешимой
в том случае, если существует такой алгоритм, который позволяет по виду формулы определить следует ли
она из заданных аксиом или нет.
Посмотрим как с помощью термов кодируются структуры данных. Далее для сокращения записи мы бу-
дем считать, что в лямбда исчислении можно определять синонимы с помощью знака равно. Запись N = M
говорит о том, что мы дали обозначение N терму M. Этой операции нет в лямбда-исчислении, но мы будем
пользоваться ею для удобства.
Логические значения
Суть логических значений заключается в операторе If, с помощью которого мы можем организовывать
ветвление алгоритма. Есть два терма T rue и F alse, которые для любых термов a и b, обладают свойствами:
If T rue a b
=
a
If F alse a b
=
b
Термы T rue, F alse и If, удовлетворяющие таким свойствам выглядят так:
T rue
=
λt f. t
F alse
=
λt f. f
If
=
λb x y. bxy
220 | Глава 14: Лямбда-исчисление
Проверим выполнение свойств:
If T rue a b ⇒ ( λb x y. bxy)( λt f. t) a b ⇒ ( λt f. t) a b ⇒ a
If F alse a b ⇒ ( λb x y. bxy)( λt f. f ) a b ⇒ ( λt f. f ) a b ⇒ b
Свойства выполнены. Логические константы кодируются постоянными функциями двух аргументов.
Функция True возвращает первый аргумент, игнорируя второй. А функция False делает то же самое, но на-
оборот. В такой интерпретации логическое отрицание можно закодировать с помощью функции flip. Также
мы можем выразить и другие логические операции:
And
=
λa b. a b F alse
Or
=
λa b. a T rue b
Мы определили логические значения не конкретными значениями, а свойствами функций. Мы построили
функции, которые ведут себя как логические значения. Этот способ определения напоминает, определение
класса типов. Мы объявили три метода T rue, F alse и If и сказали, что экземпляр класса должен удовле-
творять определённым свойствам, которые накладывают взаимные ограничения на методы класса. Ни один
из методов не имеет смысла по отдельности, важно то как они взаимодействуют.
Натуральные числа
Оказывается, что с помощью термов лямбда исчисления можно закодировать и натуральные числа с
арифметическими операциями. Мы будем кодировать числа Пеано. Для этого нам понадобится нулевой
элемент и функция определения следующего элемента. Их можно закодировать так:
Zero
=
λsz. z
Succ
=
λnsz. s( nsz)
Как и в случае логических значений числа кодируются функциями двух аргументов. Число определяется
по терму, подсчётом цепочки первых аргументов s. Например так выглядит число два:
Succ ( Succ Zero) ⇒ ( λnsz. s( nsz))( Succ Zero) ⇒ λsz. s(( Succ Zero) sz) ⇒
λsz. s(( λnsz. s( nsz)) Zero) sz ⇒ λsz. s( s( Zero s z)) ⇒ λsz. s( sz)
И мы получили два вхождения первого аргумента в теле функции. Определим сложение и умножение.
Сложение принимает две функции двух аргументов и возвращает функцию двух аргументов.
Add = λ m n s z. m s ( n s z)
В этой функции мы применяем m раз аргумент s к значению, в котором аргумент s применён n раз, так
мы и получаем m + n применений аргумента s. Сложим 3 и 2:
Add 3 2 ⇒ λs z. 3 s (2 s z) ⇒ λs z. 3 s ( s ( s z)) ⇒ λs z. s ( s ( s ( s ( s z)))) ⇒ 5
В умножении чисел m и n мы будем m раз складывать число n:
M ul = λm n s z. m ( Add n) Zero
Лямбда исчисление без типов | 221
Конструктивная математика
В конструктивной математике существование объекта может быть доказано только описанием алгорит-
ма, с помощью которого можно построить объект. Например доказательство методом “от противного” от-
вергается.
Лямбда исчисление строит конструктивное описание функции. По лямбда-терму мы можем не только
вычислять значения функции, но и понять как она была построена. В классической теории, функция это
множество пар ( x, f( x)) аргумент-значение, которое обладает свойством:
x = y ⇒ f ( x) = f ( y)
По этому определению мы ничего не можем сказать о внутренней структуре функции. Мы можем со-
бирать из одних функций другие с помощью подстановки значений, но мы никак не сможем понять, что
находится внутри функции. Лямбда исчисление решает эту проблему.
Расширение лямбда исчисления
Предположим, что мы решили написать язык программирования на основе лямбда-исчисления. Было бы
очень неэффективно представлять числа с помощью чисел Пеано. Ведь у нас есть процессор и мы можем
спросить у него чему равно значение и получить ответ очень быстро.
В этом случае пользуются расширенным лямбда исчислением. В нём два типа примитивов это перемен-
ные и константы. Для констант мы можем определять специальные правила редукции. Например мы можем
дополнить исчисление константами:
+ , ∗, 0 , 1 , 2 , ...
И ввести для них правила редукции, которые запрашивают ответ у процессора:
a + b
=
AddW ithCP U ( a, b)
a ∗ b = M ulW ithCP U ( a, b)
Так же мы можем определить и константы для логических значений:
T rue, F alse, If, N ot, And, Or
И определить правила редукции:
If T rue a b
=
a
If F alse a b
=
b
N ot T rue
=
F alse
N ot F alse
=
T rue
Add F alse a
=
F alse
Add T rue b
=
b
. . .
Такие правила называют δ-редукцией (дельта-редукция).
14.2 Комбинаторная логика
Одновременно с лямбда-исчислением развивалась комбинаторная логика. Она отличается более ком-
пактным представлением. Есть всего лишь одно правило, это применение функции к аргументу. А функции
строятся не из произвольных термов, а из набора основных функций. Набор основных функций называют
базисом.
Рассмотрим лямбда-термы:
λx. x,
λy. y,
λz. z
Все эти термы несут один и тот же смысл. Они представляют тождественную функцию. Они равны, но с
точностью до обозначений. Эта навязчивая проблема с переобозначением аргументов была решена в комби-
наторной логике. Посмотрим как строятся термы:
222 | Глава 14: Лямбда-исчисление
• Есть набор переменных x, y, z, …. Переменная – это терм.
• Есть две константы K и S, они являются термами.
• Если M и N – термы, то ( MN) – терм.
• Других термов нет.
Определены правила редукции для базисных термов:
Kxy
=
x
Sxyz
=
xz( yz)
В этих правилах мы пользуемся соглашением о расстановки скобок. Также как и в лямбда исчислении в
применении скобки группируются влево. Когда мы пишем Kxy, мы подразумеваем (( Kx) y). Термы в ком-
бинаторной логике принято называть комбинаторами. Редукция происходит до тех пор пока мы можем за-
менять вхождения базисных комбинаторов. Так если мы видим связку KXY или SXY Z, где X, Y , Z произ-
вольные термы, то мы можем их заменить согласно правилам редукции. Такие связки называют редексами.
Если в терме нет ни одного редекса, то он находится в нормальной форме. Замену редекса принято называть
свёрткой
Интересно, что комбинаторы K и S совпадают с определением класса Applicative для функций:
instance Applicative (r-> ) where
pure a r = a
(<*> ) a b r = a r (b r)
В этом определении у функций есть общее окружение r, из которого они могут читать значения, так же как
и в случае типа Reader. В методе pure (комбинатор K) мы игнорируем окружение (это константная функция),
а в методе <*> (комбинатор S) передаём окружение в функцию и аргумент и составляем применение функции
в контексте окружения r к значению, которое было получено в контексте того же окружения.
Вернёмся к проблеме различного представления тождественной функции в лямбда-исчислении. В ком-
бинаторной логике тождественная функция выражается так:
I = SKK
Проверим, определяет ли этот комбинатор тождественную функцию:
Ix = SKKx = Kx( Kx) = x
Сначала мы заменили I на его определение, затем свернули по комбинатору S, затем по левому комби-
натору K. В итоге получилось, что
Ix = x
Связь с лямбда-исчислением
Комбинаторная логика и лямбда-исчисление тесно связаны между собой. Можно определить функцию
φ, которая переводит термы комбинаторной логики в термы лямбда-исчисления:
φ( x)
=
x
φ( K)
=
λxy. x
φ( S)
=
λxyz. xz( yz)
φ( XY )
=
φ( X) φ( Y )
В первом уравнении x – переменная. Также можно определить функцию ψ, которая переводит термы
лямбда-исчисления в термы комбинаторной логики.
Комбинаторная логика | 223
ψ( x)
=
x
ψ( XY )
=
ψ( X) ψ( Y )
ψ( λx. Y )
=
[ x] . ψ( Y )
Запись [ x] . T , где x – переменная, T – терм, обозначает такой терм D, из которого можно получить терм
T подстановкой переменной x, выполнено свойство:
([ x] . T ) x = T
Эта запись означает параметризацию терма T по переменной x. Терм [ x] . T можно получить с помощью
следующего алгоритма:
[ x] . x
=
SKK
[ x] . X
=
KX,
x /
∈ V ( X)
[ x] . XY
=
S([ x] . X)([ x] . Y )
В первом уравнении мы заменяем переменную на тождественную функцию, поскольку переменные сов-
падают. Запись V ( X) во втором уравнении обозначает множество всех переменных в терме X. Поскольку
переменная по которой мы хотим параметризовать терм (или абстрагировать) не участвует в самом терме,
мы можем проигнорировать её с помощью постоянной функции K. В последнем уравнении мы параметри-
зуем применение.
С помощью этого алгоритма можно для любого терма T , все переменные которого содержатся в
{x 1 , ...xn} составить такой комбинатор D, что Dx 1 ...xn = T . Для этого мы последовательно парметризуем
терм T по всем переменным:
[ x 1 , ..., xn] . T = [ x 1] . ([ x 2 , ..., xn] . T )
Так постепенно мы придём к выражению, считаем что скобки группируются вправо:
[ x 1] . [ x 2] . ... [ xn] . T
Немного истории
Комбинаторную логику открыл Моисей Шейнфинкель. В 1920 году на докладе в Гёттингене он рассказал
основные положения этой теории. Комбинаторная логика направлена на выделение простейших строитель-
ных блоков математической логики. В этом докладе появилось понятие частичного применения. Шейнфин-
кель показал как функции многих переменных могут быть сведены к функциям одного переменного. Далее
в докладе описываются пять основных функций, называемых комбинаторами:
Ix
= x
– функция тождества
Cxy = x
– константная функция
T xyz = xzy
– функция перестановки
Zxyz = x( yz)
– функция группировки
Sxyz = xz( yz)
– функция слияния
С помощью этих функций можно избавиться в формулах от переменных, так например свойство комму-
тативности функции A можно представить так: T A = A. Эти комбинаторы зависят друг от друга. Можно
убедиться в том, что:
I
=
SCC
Z
=
S( CS) S
T
=
S( ZZS)( CC)
Все комбинаторы выражаются через комбинаторы C и S. Ранее мы пользовались другими обозначениями
для этих комбинаторов. Обозначения K и S ввёл Хаскель Карри (Haskell Curry). Независимо от Шейнфинкеля
он переоткрыл комбинаторную логику и существенно развил её. В современной комбинаторной логике для
обозначения комбинаторов I, C, T , Z и S (по Шейнфинкелю) принято использовать имена I, K, C, B, S
(по Карри).
224 | Глава 14: Лямбда-исчисление
14.3 Лямбда-исчисление с типами
Мы можем добавить в лямбда-исчисление типы. Предположим, что у нас есть множество V базовых типов.
Тогда тип это:
T = V | T → T
Тип может быть либо одним элементом из множества базовых типов. Либо стрелочным (функциональ-
ным) типом. Выражение “терм M имеет тип α” принято писать так: Mα. Стрелочный тип α → β как и в
Haskell говорит о том, что если у нас есть значение типа α, то с помощью операции применения мы можем
из терма с этим стрелочным типом получить терм типа β.
Опишем правила построения термов в лямбда-исчислении с типами:
• Переменные xα, yβ, zγ, … являются термами.
• Если Mα→β и Nα – термы, то ( Mα→βNα) β – терм.
• Если xα – переменная и Mβ – терм, то ( λxα. Mβ) α→β – терм
• Других термов нет.
Типизация накладывает ограничение на то, какие выражения мы можем комбинировать. В этом есть
плюсы и минусы. Теперь наша система является строго нормализуемой, это означает, что любой терм име-
ет нормальную форму. Но теперь мы не можем выразить все функции на числах. Например мы не можем
составить Y -комбинатор, поскольку теперь самоприменение ( ee) невозможно.
Мы ввели типы, но лишились рекурсии. Как нам быть? Эта проблема решается с помощью введения
специальной константы Y ( τ→τ) →τ
τ
, которая обозначает комбинатор неподвижной точки. Правило редукции
для Y :
( Yτ f τ→τ ) τ = ( f τ→τ ( Yτ f τ→τ )) τ
Можно убедиться в том, что это правило роходит проверку типов. Типизированное лямбда-исчисление
дополненное комбинатором неподвижной точки способно выразить все числовые функции.
14.4 Краткое содержание
В этой главе мы познакомились с лямбда-исчислением и комбинаторной логикой, двумя конструктив-
ными теориями функций. Конструктивными в том смысле, что определение функции содержит не набор
значений, а рецепт получения этих значений. В лямбда-исчислении мы видим как функция была построена,
из каких простейших частей она состоит. Редукция термов позволяет вычислять функции.
Мы узнали, что функциями можно кодировать логические значения и числа. Узнали, что все численные
функции могут быть закодированы лямбда-термами.
14.5 Упражнения
• С помощью редукции убедитесь в том, что верны формулы (в терминах Карри) :
B
=
S( KS) S
C
=
S( BBS)( KK)
Bxyz
=
xzy
Cxyz
=
x( yz)
• Попробуйте закодировать пары с помощью лямбда термов. Вам необходимо построить три функции:
P air, F st, Snd, которые обладают свойствами:
Лямбда-исчисление с типами | 225
F st ( P air a b)
=
a
Snd ( P air a b)
=
b
• в комбинаторной логике тоже есть комбинатор неподвижной точки, найдите его с помощью алгоритма
приведения термов лямбда исчисления к термам комбинаторной логики. Для краткости лучше вместо
SKK писать просто I.
• Напишите типы Lam и App, которые описывают лямбда-термы и термы комбинаторной логики в Haskell.
Напишите функции перевода из значений Lam в App и обратно.
226 | Глава 14: Лямбда-исчисление
Глава 15
Теория категорий
Многие понятия в Haskell позаимствованы из теории категорий, например это функторы, монады. Теория
категорий – это скорее язык, математический жаргон, она настолько общая, что кажется ей нет никакого
применения. Возможно это и так, но в этом языке многие сущности, которые лишь казались родственными
и было смутное интуитивное ощущение их близости, становятся тождественными.
Теория категорий занимается описанием функций. В лямбда-исчислении основной операцией была под-
становка значения в функцию, а в теории категорий мы сосредоточимся на операции композиции. Мы будем
соединять различные объекты так, чтобы структура объектов сохранялась. Структура объекта будет опреде-
ляться свойствами, которые продолжают выполнятся после преобразования объекта.
15.1 Категория
Мы будем говорить об объектах и связях между ними. Связи принято называть “стрелками” или “мор-
физмами”. Далее мы будем пользоваться термином стрелка. У стрелки есть начальный объект, его называют
доменом (domain) и конечный объект, его называют кодоменом (codomain).
f
A
B
В этой записи стрелка f соединяет объекты A и B, в тексте мы будем писать это так f : A → B, словно
стрелка это функция, а объекты это типы. Мы будем обозначать объекты большими буквами A, B, C, …, а
стрелки – маленькими буквами f, g, h, … Для того чтобы связи было интереснее изучать мы введём такое
правило:
f
A
B
g
f ; g
C
Если конец стрелки f указывает на начало стрелки g, то должна быть такая стрелка f ; g, которая обозна-
чает составную стрелку. Вводится специальная операция “точка с запятой”, которая называется композицией
стрелок: Это правило говорит о том, что связи распространяются по объектам. Теперь у нас есть не просто
объекты и стрелки, а целая сеть объектов, связанных между собой. Тот факт, что связи действительно рас-
пространяются отражается свойством:
f ; ( g ; h) = ( f ; g) ; h
Это свойство называют ассоциативностью. Оно говорит о том, что стрелки, которые образуют составную
стрелку являются цепочкой и нам не важен порядок их группировки, важно лишь кто за кем идёт. Подра-
зумевается, что стрелки f, g и h имеют подходящие типы для композиции, что их можно соединять. Это
свойство похоже на интуитивное понятие пути, как цепочки отрезков.
Связи между объектами можно трактовать как преобразования объектов. Стрелка f : A → B – это способ,
с помощью которого мы можем перевести объект A в объект B. Композиция в этой аналогии приобретает
естественную интерпретацию. Если у нас есть способ f : A → B преобразования объекта A в объект B, и
способ g : B → C преобразования объекта B в объект C, то мы конечно можем, применив сначала f, а
затем g, получить из объекта A объект C.
Когда мы думаем о стрелках как о преобразовании, то естественно предположить, что у нас есть преобра-
зование, которое ничего не делает, как тождественная функция. В будем говорить, что для каждого объекта
A есть стрелка idA, которая начинается из этого объекта и заканчивается в нём же.
| 227
idA : A → A
Тот факт, что стрелка idA ничего не делает отражается свойствами, которые должны выполняться для
всех стрелок:
idA ; f
=
f
f ; idA
=
f
Если мы добавим к любой стрелке тождественную стрелку, то от этого ничего не изменится.
Всё готово для того чтобы дать формальное определение понятия категории (category). Категория это:
• Набор объектов (object).
• Набор стрелок (arrow) или морфизмов (morphism).
• Каждая стрелка соединяет два объекта, но объекты могут совпадать. Так обозначают, что стрелка f
начинается в объекте A и заканчивается в объекте B:
f : A → B
При этом стрелка соединяет только два объекта:
f : A → B, f : A → B
⇒
A = A , B = B
• Определена операция композиции или соединения стрелок. Если конец одной стрелки совпадает с
началом другой, то их можно соединить вместе:
f : A → B, g : B → C
⇒ f ; g : A → C
• Для каждого объекта есть стрелка, которая начинается и заканчивается в этом объекте. Эту стрелку
называют тождественной (identity):
idA : A → A
Должны выполняться аксиомы:
• Тождество id
id ; f = f
f ; id = f
• Ассоциативность ;
f ; ( g ; h) = ( f ; g) ; h
Приведём примеры категорий.
• Одна точка с одной тождественной стрелкой образуют категорию.
• В категории Set объектами являются все множества, а стрелками – функции. Стрелки соединяются с
помощью композиции функций, тождественная стрелка, это тождественная функция.
• В категории Hask объектами являются типы Haskell, а стрелками – функции, стрелки соединяются с
помощью композиции функций, тождественная стрелка, это тождественная функция.
• Ориентированный граф может определять категорию. Объекты – это вершины, а стрелки это связанные
пути в графе. Соединение стрелок – это соединение путей, а тождественная стрелка, это путь в котором
нет ни одного ребра.
228 | Глава 15: Теория категорий
• Упорядоченное множество, в котором есть операция сравнения на больше либо равно задаёт катего-
рию. Объекты – это объекты множества. А стрелки это пары объектов таких, что первый объект меньше
второго. Первый объект в паре считается начальным, а второй конечным.
( a, b) : a → b
если a ≤ b
Стрелки соединяются так:
( a, b) ; ( b, c) = ( a, c)
Тождественная стрелка состоит из двух одинаковых объектов:
ida = ( a, a)
Можно убедиться в том, что это действительно категория. Для этого необходимо проверить аксиомы
ассоциативности и тождества. Важно проверить, что те стрелки, которые получаются в результате ком-
позиции, не нарушали бы основного свойства данной структуры, то есть тот факт, что второй элемент
пары всегда больше либо равен первого элемента пары.
Отметим, что бывают такие области, в которых стрелки или преобразования с одинаковыми именами
могут соединять несколько разных объектов. Например в Haskell есть классы, поэтому функции с одними
и теми же именами могут соединять разные объекты. Если все условия категории для объектов и стрелок
выполнены, кроме этого, то такую систему называют прекатегорией (pre-category). Из любой прекатегории
не сложно сделать категорию, если включить имена объектов в имя стрелки. Тогда у каждой стрелки будут
только одна пара объектов, которые она соединяет.
15.2 Функтор
Вспомним определение класса Functor:
class Functor f where
fmap :: (a -> b) -> (f a -> f b)
В этом определении участвуют тип f и метод fmap. Можно сказать, что тип f переводит произвольные
типы a в специальные типы f a. В этом смысле тип f является функцией, которая определена на типах. Метод
fmap переводит функции общего типа a -> b в специальные функции f a -> f b.
При этом должны выполняться свойства:
fmap id
= id
fmap (f . g) = fmap f . fmap g
Теперь вспомним о категории Hask. В этой категории объектами являются типы, а стрелками функции.
Функтор f отображает объекты и стрелки категории Hask в объекты и стрелки f Hask. При этом оказывается,
что за счёт свойств функтора f Hask образует категорию.
• Объекты – это типы f a.
• Стрелки – это функции fmap f.
• Композиция стрелок это просто композиция функций.
• Тождественная стрелка это fmap id.
Проверим аксиомы:
fmap f . fmap id = fmap f . id = fmap f
fmap id . fmap f = id . fmap f = fmap f
fmap f . (fmap g . fmap h)
=
fmap f . fmap (g . h)
=
fmap (f . (g . h))
=
fmap ((f . g) . h)
=
fmap (f . g) . fmap h
=
(fmap f . fmap g) . fmap h
Функтор | 229
Видно, что аксиомы выполнены, так функтор f порождает категорию f Hask. Интересно, что поскольку
Hask содержит все типы, то она содержит и типы f Hask. Получается, что мы построили категорию внутри
категории. Это можно пояснить на примере списков. Тип [] погружает любой тип в список, а функцию для
любого типа можно превратить в функцию, которая работает на списках с помощью метода fmap. При этом с
помощью класса Functor мы проецируем все типы и все функции в мир списков [a]. Но сам этот мир списков
содержится в категории Hask.
С помощью функторов мы строим внутри одной категории другую категорию, при этом внутренняя ка-
тегория обладает некоторой структурой. Так если раньше у нас были только произвольные типы a и произ-
вольные функции a -> b, то теперь все объекты имеют тип [a] и все функции имеют тип [a] -> [b]. Также и
функтор Maybe переводит произвольное значение, в значение, которое обладает определённой структурой. В
нём выделен дополнительный элемент Nothing, который обозначает отсутствие значения. Если по типу val
:: a мы ничего не можем сказать о содержании значения val, то по типу val :: Maybe a, мы знаем один
уровень конструкторов. Например мы уже можем проводить сопоставление с образцом.
Теперь давайте вернёмся к теории категорий и дадим формальное определение понятия. Пусть A и B –
категории, тогда функтором из A в B называют отображение F , которое переводит объекты A в объекты B
и стрелки A в стрелки B, так что выполнены следующие свойства:
F f
:
F A →B F B если f : A →A B
F idA
=
idF A
для любого объекта A из A
F ( f ; g)
=
F f ; F g
если ( f ; g) подходят по типам
Здесь запись →A и →B означает, что эти стрелки в разных категориях. После отображения стрелки f
из категории A мы получаем стрелку в категории B, это и отражено в типе F f : F A →B F B. Первое
свойство говорит о том, что после отображения стрелки соединяют те же объекты, что и до отображения.
Второе свойства говорит о сохранении тождественных стрелок. А последнее свойство, говорит о том, что
“пути” между объектами также сохраняются. Если мы находимся в категории A в объекте A и перед нами
есть путь состоящий из нескольких стрелок в объект B, то неважно как мы пойдём в F B либо мы пройдём
этот путь в категории A и в самом конце переместимся в F B или мы сначала переместимся в F A и затем
пройдём по образу пути в категории F B. Так и так мы попадём в одно и то же место. Схематически это
можно изобразить так:
f
g
A
B
C
F
F
F
F A
F B
F C
F f
F g
Стрелки сверху находятся в категории A, а стрелки снизу находятся в категории B. Функтор F : A → A,
который переводит категорию A в себя называют эндофунктором (endofunctor). Функторы отображают одни
категории в другие сохраняя структуру первой категории. Мы словно говорим, что внутри второй категории
есть структура подобная первой. Интересно, что последовательное применение функторов, также является
функтором. Мы будем писать последовательное применение функторов F и G слитно, как F G. Также можно
определить и тождественный функтор, который ничего не делает с категорией, мы будем обозначать его как
IA или просто I, если категория на которой он определён понятна из контекста. Это говорит о том, что мы
можем построить категорию, в которой объектами будут другие категории, а стрелками будут функторы.
15.3 Естественное преобразование
В программировании часто приходится переводить данные из одной структуры в другую. Каждая из
структур хранит какие-то конкретные значения, но мы ничего с ними не делаем мы просто перекладываем
содержимое из одного ящика в другой. Например в нашем ящике только один отсек, но вдруг нам пришло
бесконечно много подарков, что поделать нам приходится сохранить первый попавшийся, отбросив осталь-
ные. Главное в этой аналогии это то, что мы ничего не меняем, а лишь перекладываем содержимое из одной
структуры в другую.
В Haskell это можно описать так:
onlyOne :: [a] -> Maybe a
onlyOne []
= Nothing
onlyOne (a:as)
= Just a
В этой функции мы перекладываем элементы из списка [a] в частично определённое значение Maybe.
Тоже самое происходит и в функции concat:
230 | Глава 15: Теория категорий
concat :: [[a]] -> [a]
Элементы перекладываются из списка списков в один список. В теории категорий этот процесс называ-
ется естественным преобразованием. Структуры определяются функторами. Поэтому в определении будет
участвовать два функтора. В функции onlyOne это были функторы [] и Maybe. При перекладывании элемен-
тов мы можем просто выбросить все элементы:
burnThemALl :: [a] -> ()
burnThemAll = const ()
Можно сказать, что единичный тип также определяет функтор. Это константный функтор, он переводит
любой тип в единственное значение (), а функцию в id:
data Empty a = Empty
instance Functor Empty where
fmap = const id
Тогда тип функции burnThemAll будет параметризован и слева и справа от стрелки:
burnThemAll :: [a] -> Empty a
burnThemAll = const Empty
Пусть даны две категории A и B и два функтора F, G : A → B. Преобразованием (transformation) в B из
F в G называют семейство стрелок ε:
εA : F A →B GA
для любого A из A
Рассмотрим преобразование onlyOne :: [a] -> Maybe a. Категории A и B в данном случае совпадают~–
это категория Hask. Функтор F – это список, а функтор G это Maybe. Преобразование onlyOne для каждого
объекта a из Hask определяет стрелку
onlyOne :: [a] -> Maybe a
Так мы получаем семейство стрелок, параметризованное объектом из Hask:
onlyOne :: [Int] -> Maybe Int
onlyOne :: [Char] -> Maybe Char
onlyOne :: [Int -> Int] -> Maybe (Int -> Int)
...
...
Теперь давайте определим, что значит перекладывать из одной структуры в другую, не меняя содержа-
ния. Представим, что функтор – это контейнер. Мы можем менять его содержание с помощью метода fmap.
Например мы можем прибавить единицу ко всем элементам списка xs с помощью выражения fmap (+1) xs.
Точно так же мы можем прибавить единицу к частично определённому значению. С точки зрения теории ка-
тегорий суть понятия “останется неизменным при перекладывании” заключается в том, что если мы возьмём
любую функцию к примеру прибавление единицы, то нам неважно когда её применять до функции onlyOne
или после. И в том и в другом случае мы получим одинаковый ответ. Давайте убедимся в этом:
onlyOne $ fmap (+1) [1,2,3,4,5]
=>
onlyOne [2,3,4,5,6]
=>
Just 2
fmap (+1) $ onlyOne [1,2,3,4,5]
=>
fmap (+1) $ Just 1
=>
Just 2
Результаты сошлись, обратите внимание на то, что функции fmap (+1) в двух вариантах являются раз-
ными функциями. Первая работает на списках, а вторая на частично определённых значениях. Суть в том,
что если при перекладывании значение не изменилось, то нам не важно когда выполнять преобразование
внутри функтора [] или внутри функтора Maybe. Теперь давайте выразим это на языке теории категорий.
Преобразование ε в категории B из функтора F в функтор G называют естественным (natural), если
F f ; εB = εA ; Gf
для любого f : A →A B
Естественное преобразование | 231
Это свойство можно изобразить графически:
ε
F A
A
GA
F f
Gf
F B
GB
εB
По смыслу ясно, что если у нас есть три структуры данных (или три функтора), если мы просто пере-
ложили данные из первой во вторую, а затем переложили данные из второй в третью, ничего не меняя. То
итоговое преобразование, которое составлено из последовательного применения перекладывания данных
также не меняет данные. Это говорит о том, что композиция двух естественных преобразований также явля-
ется естественным преобразованием. Также мы можем составить тождественное преобразование, для двух
одинаковых функторов F : A → B, это будет семейство тождественных стрелок в категории B. Получает-
ся, что для двух категорий A и B мы можем составить категорию F tr( A, B), в которой объектами будут
функторы из A в B, а стрелками будут естественные преобразования. Поскольку естественные преобразова-
ния являются стрелками, которые соединяют функторы, мы будем обозначать их как обычные стрелки. Так
запись η : F → G обозначает преобразование η, которое переводит функтор F в функтор G.
Интересно, что изначально создатели теории категорий Саундедерс Маклейн и Сэмюэль Эйленберг при-
думали понятие естественного преобразования, а затем, чтобы дать ему обоснование было придумано поня-
тие функтора, и наконец для того чтобы дать обоснование функторам были придуманы категории. Катего-
рии содержат объекты и стрелки, для стрелок есть операция композиции. Также для каждого объекта есть
тождественная стрелка. Функторы являются стрелками в категории, в которой объектами являются другие
категории. А естественные преобразования являются стрелками в категории, в которой объектами являются
функторы. Получается такая иерархия структур.
15.4 Монады
Монадой называют эндофунктор T : A → A, для которого определены два естественных преобразования
η : I → T и µ : T T → T и выполнены два свойства:
• T ηA ; µA = idTA
• T µA ; µTA = µTTA ; µA
Преобразование η – это функция return, а преобразование µ – это функция join. В теории категорий в
классе Monad другие методы. Перепишем эти свойства в виде функций Haskell:
join . fmap return
= id
join . fmap join
= join . join
Порядок следования аргументов изменился, потому что мы пользуемся обычной композицией (через
точку). Выражение T ηA означает применение функтора T к стрелке ηA. Ведь преобразование это семейство
стрелок, которые параметризованы объектами категории. На языке Haskell это означает применить fmap к
полиморфной функции (функции с параметром).
Также эти свойства можно изобразить графически:
T η
T A
A
µ
T T A
A
T A
T µ
T T T A
A
T T A
µT A
µA
T T A
T A
µA
Категория Клейсли
Если у нас есть монада T , определённая в категории A, то мы можем построить в этой категории кате-
горию специальных стрелок вида A → T B. Эту категорию называют категорией Клейсли.
• Объекты категории Клейсли AT – это объекты исходной категории A.
232 | Глава 15: Теория категорий
• Стрелки в AT это стрелки из A вида A → T B, мы будем обозначать их A →T B
• Композиция стрелок f : A →T B и g : B →T C определена с помощью естественных преобразований
монады T :
f ; T g = f ; T g ; µ
Значок ; T указывает на то, что слева от равно композиция в AT . Справа от знака равно используется
композиция в исходной категории A.
• Тождественная стрелка – это естественное преобразование η.
Можно показать, что категория Клейсли действительно является категорией и свойства операций компо-
зиции и тождества выполнены.
15.5 Дуальность
Интересно, что если в категории A перевернуть все стрелки, то снова получится категория. Попробуйте
нарисовать граф со стрелками, и затем мысленно переверните направление всех стрелок. Все пути исход-
ного графа перейдут в перевёрнутые пути нового графа. При этом пути будут проходить через те же точки.
Сохранятся композиции стрелок, только все они будут перевёрнуты. Такую категорию обозначают Aop. Но
оказывается, что переворачивать мы можем не только категории но и свойства категорий, или утверждения
о категориях, эту операцию называют дуализацией. Определим её:
dual A
=
A
если A является объектом
dual x
=
x
если x обозначает стрелку
dual ( f : A → B) = dual f : B → A
A и B поменялись местами
dual ( f ; g)
=
dual g ; dual f
f и g поменялись местами
dual ( idA)
=
idA
Есть такое свойство, если и в исходной категории A выполняется какое-то утверждение, то в перевёр-
нутой категории Aop выполняется перевёрнутое (дуальное) свойство. Часто в теории категорий из одних
понятий получают другие дуализацией. При этом мы можем не проверять свойства для нового понятия,
они будут выполняться автоматически. К дуальным понятиям обычно добавляют приставку “ко”. Приведём
пример, получим понятие комонады.
Для начала вспомним определение монады. Монада – это эндофунктор (функтор, у которого совпадают
начало и конец или домен и кодомен) T : A → A и два естественных преобразования η : I → T и
µ : T T → T , такие что выполняются свойства:
• T η ; µ = id
• T µ ; µ = µ ; µ
Дуализируем это определение. Комонада – это эндофунктор T : A → A и два естественных преобразо-
вания η : T → I и µ : T T → T , такие что выполняются свойства
• µ ; T η = id
• µ ; T µ = µ ; µ
Мы просто переворачиваем домены и кодомены в стрелках и меняем порядок в композиции. Проверьте
сошлись ли типы. Попробуйте нарисовать графическую схему свойств комонады и сравните со схемой для
монады.
Можно также определить и категорию коКлейсли. В категории коКлейсли все стрелки имеют вид T A →
B. Теперь дуализируем композицию из категории Клейсли:
f ; T g = f ; T g ; µ
Теперь получим композицию в категории коКлейсли:
g ; T f = µ ; T g ; f
Мы перевернули цепочки композиций слева и справа от знака равно. Проверьте сошлись ли типы. Не
забывайте что в этом определении η и µ естественные преобразования для комонады. Нам не нужно прове-
рять является ли категория коКлейсли действительно категорией. Нам не нужно опять проверять свойства
Дуальность | 233
стрелки тождества и ассоциативности композиции, если мы уже проверили их для монады. Следовательно
перевёрнутое утверждение будет выполняться в перевёрнутой категории коКлейсли. В этом основное пре-
имущество определения через дуализацию.
Этим приёмом мы можем воспользоваться и в Haskell, дуализируем класс Monad:
class Monad m where
return
:: a -> m a
(>>=)
:: m a -> (a -> m b) -> m b
Перевернём все стрелки:
class Comonad c where
coreturn
:: c a -> a
cobind
:: c b -> (c b -> a) -> c a
15.6 Начальный и конечный объекты
Начальный объект
Представим, что в нашей категории есть такой объект 0, который соединён со всеми объектами. При-
чём стрелка начинается из этого объекта и для каждого объекта может быть только одна стрелка которая
соединят данный объект с 0. Графически эту ситуацию можно изобразить так:
. . .
A 1
A 2
. . .
0
A 3
. . .
. . .
A 4
Такой объект называют начальным (initial object). Его принято обозначать нулём, словно это начало от-
счёта. Для любого объекта A из категории A с начальным объектом 0 существует и только одна стрел-
ка f : 0 → B. Можно сказать, что начальный объект определяет функцию, которая переводит объекты A в
стрелки f : 0 → A. Эту функцию обозначают специальными скобками ( | · |), она называется катаморфизмом
(catamorphism).
( | A |) = f : 0 → A
У начального объекта есть несколько важных свойств. Они очень часто встречаются в разных вариациях,
в понятиях, которые определяются через понятие начального объекта:
( | 0 |) = id 0
тождество
f, g : 0 → A ⇒ f = g
уникальность
f : A → B
⇒ ( | A |) ; f = ( | B |)
слияние (fusion)
Эти свойства следуют из определения начального объекта. Свойство тождества говорит о том, что стрелка
ведущая из начального объекта в начальный является тождественной стрелкой. В самом деле по определе-
нию начального объекта для каждого объекта может быть только одна стрелка, которая начинается в 0 и
заканчивается в этом объекте. Стрелка ( | 0 |) начинается в 0 и заканчивается в 0, но у нас уже есть одна та-
кая стрелка, по определению категории для каждого объекта определена тождественная стрелка, значит эта
стрелка является единственной.
Второе свойство следует из единственности стрелки, ведущей из начального объекта в данный. Третье
свойство лучше изобразить графически:
f
A
B
( | A |)
( | B |)
0
Поскольку стрелки ( | A |) и f можно соединить, то должна быть определена стрелка ( | A |) ; f : 0 → B, но
поскольку в категории с начальным объектом из начального объекта 0 в объект B может вести лишь одна
стрелка, то стрелка ( | A |) ; f должна совпадать с ( | B |).
234 | Глава 15: Теория категорий
Конечный объект
Дуализируем понятие начального объекта. Пусть в категории A есть объект 1, такой что для любого
объекта A существует и только одна стрелка, которая начинается из этого объекта и заканчивается в объекте
1. Такой объект называют конечным (terminal object):
. . .
A 1
A 2
. . .
1
A 3
. . .
. . .
A 4
Конечный объект определяет в категории функцию, которая ставит в соответствие объектам стрелки,
которые начинаются из данного объекта и заканчиваются в конечном объекте. Такую функцию называют
анаморфизмом (anamorphism), и обозначают специальными скобками [( · )], которые похожи на перевёрнутые
скобки для катаморфизма:
[( A )] = f : A → 1
Можно дуализировать и свойства:
[( 1 )] = id 1
тождество
f, g : A → 1 ⇒ f = g
уникальность
f : A → B
⇒ f ; [( B )] = [( A )]
слияние (fusion)
Приведём иллюстрацию для свойства слияния:
f
A
B
[( A )]
[( B )]
1
15.7 Сумма и произведение
Давным-давно, когда мы ещё говорили о типах, мы говорили, что типы конструируются с помощью двух
базовых операций: суммы и произведения. Сумма говорит о том, что значение может быть либо одним зна-
чением либо другим. А произведение обозначает сразу несколько значений. В Haskell есть два типа, которые
представляют собой сумму и произведение в общем случае. Тип для суммы это Either:
data Either a b = Left a | Right b
Произведение в самом общем виде представлено кортежами:
data (a, b) = (a, b)
В теории категорий сумма и произведение определяются как начальный и конечный объекты в специаль-
ных категориях. Теория категорий изучает объекты по тому как они взаимодействуют с остальными объек-
тами. Взаимодействие обозначается с помощью стрелок. Специальные свойства стрелок определяют объект.
Например представим, что мы не можем заглядывать внутрь суммы типов, как бы мы могли взаимодей-
ствовать с объектом, который представляет собой сумму двух типов A+ B? Нам необходимо уметь создавать
объект типа A + B из объектов A и B извлекать их из суммы. Создание объектов происходит с помощью
двух специальных конструкторов:
inl : A → A + B
inr : B → A + B
Сумма и произведение | 235
Также нам хочется уметь как-то извлекать значения. По смыслу внутри суммы A+ B хранится либо объект
A либо объект B и мы не можем заранее знать какой из них, поскольку внутреннее содержание A + B от
нас скрыто, но мы знаем, что это только A или B. Это говорит о том, что если у нас есть две стрелки A → C
и B → C, то мы как-то можем построить A + B → C. У нас есть операция:
out( f, g) : A + B → C
f : A → C, g : B → C
При этом для того, чтобы стрелки inl, inr и out были согласованы необходимо, чтобы выполнялись
свойства:
inl ; out( f, g) = f
inr ; out( f, g) = g
Для любых функций f и g. Графически это свойство можно изобразить так:
A
inl
A + B
inr
B
out
f
g
C
Итак суммой двух объектов A и B называется объект A + B и две стрелки inl : A → A + B и inr : B →
A + B такие, что для любых двух стрелок f : A → C и g : B → C определена одна и только одна стрелка
h : A + B → C такая, что выполнены свойства:
inl ; h = f
inr ; h = g
В этом определении объект A + B вместе со стрелками inl и inr, определяет функцию, которая по
некоторому объекту C и двум стрелкам f и g строит стрелку h, которая ведёт из объекта A + B в объект
C. Этот процесс определения стрелки по объекту напоминает определение начального элемента. Построим
специальную категорию, в которой объект A+ B будет начальным. Тогда функция out будет катаморфизмом.
Функция out принимает две стрелки и возвращает третью. Посмотрим на типы:
f : A → C
inl : A → A + B
g : B → C
inr : B → A + B
Каждая из пар стрелок в столбцах указывают на один и тот же объект, а начинаются они из двух разных
объектов A и B. Определим категорию, в которой объектами являются пары стрелок ( a 1 , a 2), которые на-
чинаются из объектов A и B и заканчиваются в некотором общем объекте D. Эту категорию ещё называют
клином. Стрелками в этой категории будут такие стрелки f : ( d 1 , d 2) → ( e 1 , e 2), что стрелки в следующей
диаграмме коммутируют (не важно по какому пути идти из двух разных точек).
A
B
d
e
1
2
e 1
d 2
D
E
f
Композиция стрелок – это обычная композиция в исходной категории, в которой определены объекты A
и B, а тождественная стрелка для каждого объекта, это тождественная стрелка для того объекта, в котором
сходятся обе стрелки. Можно проверить, что это действительно категория.
Если в этой категории есть начальный объект, то мы будем называть его суммой объектов A и B. Две
стрелки, которые содержит этот объект мы будем называть inl и inr, а общий объект в котором эти стрелки
сходятся будем называть A + B. Теперь если мы выпишем определение для начального объекта, но вме-
сто произвольных стрелок и объектов подставим наш конкретный случай, то мы получим как раз исходное
определение суммы.
Начальный объект ( inl : A → A + B, inr : B → A + B) ставит в соответствие любому объекту
( f : A → C, g : B → C) стрелку h : A + B → C такую, что выполняются свойства:
236 | Глава 15: Теория категорий
A
inl
A + B
inr
B
h
f
g
C
А как на счёт произведения? Оказывается, что произведение является дуальным понятием по отношению
к сумме. Его иногда называют косуммой, или сумму называют копроизведением. Дуализируем категорию,
которую мы строили для суммы.
У нас есть категория A и в ней выделено два объекта A и B. Объектами новой категории будут пары
стрелок ( a 1 , a 2), которые начинаются в общем объекте C а заканчиваются в объектах A и B. Стрелками в
этой категории будут стрелки исходной категории h : ( e 1 , e 2) → ( d 1 , d 2) такие что следующая диаграмма
коммутирует:
A
B
e 1
d 2
d
e
1
2
D
E
f
Композиция и тождественные стрелки позаимствованы из исходной категории A. Если в этой категории
существует конечный объект. То мы будем называть его произведением объектов A и B. Две стрелки этого
объекта обозначаются как ( exl, exr), а общий объект из которого они начинаются мы назовём A×B. Теперь
распишем определение конечного объекта для нашей категории пар стрелок с общим началом.
Конечный объект ( exl : A×B → A, exr : A×B → B) ставит в соответствие любому объекту категории
( f : C → A, g : C → B) стрелку h : C → A × B. При этом выполняются свойства:
A
exl
A × B
exr
B
h
f
g
C
Итак мы определили сумму, а затем на автомате, перевернув все утверждения, получили определение
произведения. Но что это такое? Соответствует ли оно интуитивному понятию произведения?
Так же как и в случае суммы в теории категорий мы определяем понятие, через то как мы можем с ним
взаимодействовать. Посмотрим, что нам досталось от абстрактного определения. У нас есть обозначение
произведения типов A × B. Две стрелки exl и exr. Также у нас есть способ получить по двум функциям
f : C → A и g : C → B стрелку h : C → A × B. Для начала посмотрим на типы стрелок конечного объекта:
exl : A × B → A
exr : A × B → B
По типам видно, что эти стрелки разбивают пару на составляющие. По смыслу произведения мы точно
знаем, что у нас есть в A × B и объект A и объект B. Эти стрелки позволяют нам извлекать компоненты
пары. Теперь посмотрим на анаморфизм:
[( f, g )] : C → A × B
f : C → A, g : C → B
Эта функция позволяет строить пару по двум функциям и начальному значению. Но, поскольку здесь мы
ничего не вычисляем, а лишь связываем объекты, мы можем по паре стрелок, которые начинаются из общего
источника связать источник с парой конечных точек A × B.
При этом выполняются свойства:
[( f, g )] ; exl = f
[( f, g )] ; exr = g
Эти свойства говорят о том, что функции построения пары и извлечения элементов из пары согласованы.
Если мы положим значение в первый элемент пары и тут же извлечём его, то это тоже само если бы мы не
использовали пару совсем. То же самое и со вторым элементом.
Сумма и произведение | 237
15.8 Экспонента
Если представить, что стрелки это функции, то может показаться, что все наши функции являются функ-
циями одного аргумента. Ведь у стрелки есть только один источник. Как быть если мы хотим определить
функцию нескольких аргументов, что она связывает? Если в нашей категории определено произведение объ-
ектов, то мы можем представить функцию двух аргументов, как стрелку, которая начинается из произведе-
ния:
(+) : N um × N um → N um
Но в лямбда-исчислении нам были доступны более гибкие функции, функции могли принимать на вход
функции и возвращать функции. Как с этим обстоят дела в теории категорий? Если перевести определение
функций высшего порядка на язык теории категорий, то мы получим стрелки, которые могут связывать дру-
гие стрелки. Категория с функциями высшего порядка может содержать свои стрелки в качестве объектов.
Стрелки как объекты обозначаются с помощью степени, так запись BA означает стрелку A → B. При этом
нам необходимо уметь интерпретировать стрелку, мы хотим уметь подставлять значения. Если у нас есть
объект BA, то должна быть стрелка
eval : BA × A → B
На языке функций можно сказать, что стрелка eval принимает функцию высшего порядка A → B и зна-
чение типа A, а возвращает значение типа B. Объект BA называют экспонентой. Теперь дадим формальное
определение.
Пусть в категории A определено произведение. Экспонента – это объект BA вместе со стрелкой eval :
BA × A → B такой, что для любой стрелки f : C × A → B определена стрелка curry( f ) : C → BA при
этом следующая диаграмма коммутирует:
C
C × A
f
curry( f )
( curry( f ) , id)
BA
BA × A
B
Давайте разберёмся, что это всё означает. По смыслу стрелка curry( f) это каррированная функция двух
аргументов. Вспомните о функции curry из Haskell. Диаграмма говорит о том, что если мы каррированием
функции двух аргументов получим функцию высшего порядка C → BA, а затем с помощью функции eval
получим значение, то это всё равно, что подставить два значения в исходную функцию. Запись ( curry( f) , id)
означает параллельное применение двух стрелок внутри пары:
( f, g) : A × A → B × B ,
f : A → B, g : A → B
Так применив стрелки curry( f) : C → BA и id : A → A к паре C × A, мы получим пару BA × A.
Применение здесь условное мы подразумеваем применение в функциональной аналогии, в теории категорий
происходит связывание пар объектов с помощью стрелки ( f, g).
Интересно, что и экспоненту можно получить как конечный объект в специальной категории. Пусть есть
категория A и в ней определено произведение объектов A и B. Построим категорию, в которой объектами
являются стрелки вида:
C × A → B
где C – это произвольный объект исходной категории. Стрелкой между объектами c : C × A → B и
d : D × A → B в этой категории будет стрелка f : C → D из исходной категории, такая, что следующая
диаграмма коммутирует:
C
C × A
f
c
( f, id)
D
D × A
B
Если в этой категории существует конечный объект, то он является экспонентой. А функция curry явля-
ется анаморфизмом для экспоненты.
238 | Глава 15: Теория категорий
15.9 Краткое содержание
Теория категорий изучает понятия через то как эти понятия взаимодействуют друг с другом. Мы забываем
о том, как эти понятия реализованы, а смотрим лишь на свойства связей.
Мы узнали что такое категория. Категория это структура с объектами и стрелками. Стрелки связывают
объекты. Причём связи могут соединятся. Также считается, что объект всегда связан сам с собой. Мы узнали,
что есть такие категории, в которых сами категории являются объектами, а стрелки в таких категориях мы
назвали функторами. Также мы узнали, что сами функторы могут стать объектами в некоторой категории,
тогда стрелки в этой категории мы будем называть естественными преобразованиями.
Мы узнали что такое начальный и конечный объект и как с помощью этих понятий можно определить
сумму и произведение типов. Также мы узнали как в теории категорий описываются функции высших по-
рядков.
15.10 Упражнения
• Проверьте аксиомы категории (ассоциативность и тождество) для категории функторов и категории
естественных преобразований.
• Изоморфизмом называют такие стрелки f : A → B и g : B → A, для которых выполнено свойство:
f ; g = idA
g ; f = idB
Объекты A и B называют изоморфными, если они связаны изоморфизмом, это обозначают так: A ∼
= B.
Докажите, что все начальные и конечные элементы изоморфны.
• Поскольку сумма и произведение типов являются начальным и конечным объектами в специальных
категориях для них также выполняются свойства тождества, уникальности и слияния. Выпишите эти
свойства для суммы и произведения.
• Подумайте как можно определить экземпляр класса Comonad для потоков:
data Stream a = a :& Stream a
Можно ли придумать экземпляр для класса Monad?
• Дуальную категорию для категории A обозначают Aop. Если F является функтором в категории Aop,
то в исходной категории его называют контравариантным функтором. Выпишите определение функто-
ра в Aop, а затем с помощью дуализации получите свойства контравариантного функтора в исходной
категории A.
Краткое содержание | 239
Глава 16
Категориальные типы
В этой главе мы узнаем как в теории категорий определяются типы. В теории категорий типы определяют-
ся как начальные и конечные объекты в специальных категориях, которые называются алгебрами функторов.
Для понимания этой главы хорошо освежить в памяти главу о структурной рекурсии, там где мы говорили
о свёртках и развёртках.
16.1 Программирование в стиле оригами
Оригами – состоит из двух слов “свёртка” и “бумага”. При программировании в стиле оригами все функ-
ции строятся через функции свёртки и развёртки. Есть даже такие языки программрования, в которых это
единственный способ определения рекурсии. Этот стиль очень хорошо подходит для ленивых языков про-
граммирования, поскольку в связке:
fold f . unfold g
функции свёртки и развёртки работают синхронно. Функция развёртки не производит новых элементов
до тех пор пока они не понадобятся во внешней функции свёртки.
Помните в одной из глав мы говорили о том, что рекурсивные функции можно определять через функцию
fix.
Например так выглядит рекурсивная функция сложения всех чисел от одного до n:
sumInt :: Int -> Int
sumInt 0 = 0
sumInt n = n + sumInt (n-1)
Эту функцию мы можем переписать с помощью функции fix. При вычислении fix f будет составлено
значение
f (f (f (f ... )))
Теперь перепишем функцию sumInt через fix:
sumInt = fix $ \f n ->
case n of
0
-> 0
n
-> n + f (n - 1)
Смотрите лямбда функция в аргументе fix принимает функцию и число, а возвращает число. Тип этой
функции (Int -> Int) -> (Int -> Int). После применения функции fix мы как раз и получим функцию
типа Int -> Int. В лямбда функции рекурсивный вызов был заменён на вызов функции-параметра f.
Оказывается, что этот приём может быть применён и для рекурсивных типов данных. Мы можем создать
обобщённый тип, который обозначает рекурсивный тип:
newtype Fix f = Fix { unFix :: f (Fix f) }
В этой записи мы получаем уравнение неподвижной точки Fix f = f (Fix f), где f это некоторый тип
с параметром. Определим тип целых чисел:
240 | Глава 16: Категориальные типы
data N a = Zero | Succ a
type Nat = Fix N
Теперь создадим несколько конструкторов:
zero :: Nat
zero = Fix Zero
succ :: Nat -> Nat
succ = Fix . Succ
Сохраним эти определения в модуле Fix. hs и посмотрим в интерпретаторе на значения и их типы, ghc не
сможет вывести экземпляр Show для типа Fix, потому что он зависит от типа с параметром, а не от конкретно-
го типа. Для решения этой проблемы нам придётся определить экземпляры вручную и подключить несколько
расширений языка. Помните в главе о ленивых вычислениях мы подключали расширение BangPatterns? Нам
понадобятся:
{-# Language FlexibleContexts, UndecidableInstances #-}
Теперь определим экземпляры для Show и Eq:
instance Show (f (Fix f)) => Show (Fix f) where
show x = ”(” ++ show (unFix x) ++ ”)”
instance Eq (f (Fix f)) => Eq (Fix f) where
a == b = unFix a == unFix b
Определим списки-оригами:
data L a b = Nil | Cons a b
deriving (Show)
type List a = Fix (L a)
nil :: List a
nil = Fix Nil
infixr 5 ‘cons‘
cons :: a -> List a -> List a
cons a = Fix . Cons a
В типе L мы заменили рекурсивный тип на параметр. Затем в записи List a = Fix (L a) мы произ-
водим замыкание по параметру. Мы бесконечно вкладываем тип L a во второй параметр. Так получается
рекурсивный тип для списков. Составим какой-нибудь список:
*Fix> :r
[1 of 1] Compiling Fix
( Fix. hs, interpreted )
Ok, modules loaded: Fix.
*Fix> 1 ‘cons‘ 2 ‘cons‘ 3 ‘cons‘ nil
(Cons 1 (Cons 2 (Cons 3 (Nil))))
Спрашивается, зачем нам это нужно? Зачем нам записывать рекурсивные типы через тип Fix? Оказыва-
ется при такой записи мы можем построить универсальные функции fold и unfold, они будут работать для
любого рекурсивного типа.
Помните как мы составляли функции свёртки? Мы строили воображаемый класс, в котором сворачивае-
мый тип заменялся на параметр. Например для списка мы строили свёртку так:
class [a] b where
(:) :: a -> b -> b
[]
:: b
После этого мы легко получали тип для функции свёртки:
foldr :: (a -> b -> b) -> b -> ([a] -> b)
Программирование в стиле оригами | 241
Она принимает методы воображаемого класса, в котором тип записан с параметром, а возвращает функ-
цию из рекурсивного типа в тип параметра.
Сейчас мы выполняем эту процедуру замены рекурсивного типа на параметр в обратном порядке. Сначала
мы строим типы с параметром, а затем получаем из них рекурсивные типы с помощью конструкции Fix.
Теперь методы класса с параметром это наши конструкторы исходных классов, а рекурсивный тип записан
через Fix. Если мы сопоставим два способа, то мы сможем получить такой тип для функции свёртки:
fold :: (f b -> b) -> (Fix f -> b)
Смотрите функция свёртки по-прежнему принимает методы воображаемого класса с параметром, но те-
перь класс перестал быть воображаемым, он стал типом с параметром. Результатом функции свёртки будет
функция из рекурсивного типа Fix f в тип параметр.
Аналогично строится и функция unfold:
unfold :: (b -> f b) -> (b -> Fix f)
В первой функции мы указываем один шаг разворачивания рекурсивного типа, а функция развёртки
рекурсивно распространяет этот один шаг на потенциально бесконечную последовательность применений
этого одного шага.
Теперь давайте определим эти функции. Но для этого нам понадобится от типа f одно свойство. Он
должен быть функтором, опираясь на это свойство, мы будем рекурсивно обходить этот тип.
fold :: Functor f => (f a -> a) -> (Fix f -> a)
fold f = f . fmap (fold f) . unFix
Проверим эту функцию по типам. Для этого нарисуем схему композиции:
f
fmap (fold f)
f
Fix f
f (Fix f)
f a
a
Сначала мы разворачиваем обёртку Fix и получаем значение типа f (Fix f), затем с помощью fmap мы
внутри типа f рекурсивно вызываем функцию свёртки и в итоге получаем значение f a, на последнем шаге
мы выполняем свёртку на текущем уровне вызовом функции f.
Аналогично определяется и функция unfold. Только теперь мы сначала развернём первый уровень, затем
рекурсивно вызовем развёртку внутри типа f и только в самом конце завернём всё в тип Fix:
unfold :: Functor f => (a -> f a) -> (a -> Fix f)
unfold f = Fix . fmap (unfold f) . f
Схема композиции:
Fix
fmap (unold f)
f
Fix f
f (Fix f)
f a
a
Возможно вы уже догадались о том, что функция fold дуальна по отношению к функции unfold, это
особенно наглядно отражается на схеме композиции. При переходе от fold к unfold мы просто перевернули
все стрелки заменили разворачивание типа Fix на заворачивание в Fix.
Определим несколько функций для натуральных чисел и списков в стиле оригами. Для начала сделаем
L и N экземпляром класса Functor:
instance Functor N where
fmap f x = case x of
Zero
-> Zero
Succ a
-> Succ (f a)
instance Functor (L a) where
fmap f x = case x of
Nil
-> Nil
Cons a b
-> Cons a (f b)
Это всё что нам нужно для того чтобы начать пользоваться функциями свёртки и развёртки! Определим
экземпляр Num для натуральных чисел:
instance Num Nat where
(+) a = fold $ \x -> case x of
Zero
-> a
Succ x
-> succ x
(*) a = fold $ \x -> case x of
242 | Глава 16: Категориальные типы
Zero
-> zero
Succ x
-> a + x
fromInteger = unfold $ \n -> case n of
0
-> Zero
n
-> Succ (n-1)
abs = undefined
signum = undefined
Сложение и умножение определены через свёртку, а функция построения натурального числа из чис-
ла типа Integer определена через развёртку. Сравните с теми функциями, которые мы писали в главе про
структурную рекурсию. Теперь мы не передаём отдельно две функции, на которые мы будем заменять кон-
структоры. Эти функции закодированы в типе с параметром. Для того чтобы этот код заработал нам придётся
добавить ещё одно расширение TypeSynonymInstances наши рекурсивные типы являются синонимами, а не
новыми типами. В рамках стандарта Haskell мы можем определять экземпляры только для новых типов, для
того чтобы обойти это ограничение мы добавим ещё одно расширение.
*Fix> succ $ 1+2
(Succ (Succ (Succ (Succ (Zero)))))
*Fix> ((2 * 3) + 1) :: Nat
(Succ (Succ (Succ (Succ (Succ (Succ (Succ (Zero))))))))
*Fix> 2+2 == 2*(2::Nat)
True
Определим функции на списках. Для начала определим две вспомогательные функции, которые извле-
кают голову и хвост списка:
headL :: List a -> a
headL x = case unFix x of
Nil
-> error ”empty list”
Cons a _
-> a
tailL :: List a -> List a
tailL x = case unFix x of
Nil
-> error ”empty list”
Cons a b
-> b
Теперь определим несколько новых функций:
mapL :: (a -> b) -> List a -> List b
mapL f = fold $ \x -> case x of
Nil
-> nil
Cons a b
-> f a ‘cons‘ b
takeL :: Int -> List a -> List a
takeL = curry $ unfold $ \(n, xs) ->
if n == 0 then Nil
else Cons (headL xs) (n-1, tailL xs)
Сравните эти функции с теми, что мы определяли в главе о структурной рекурсии. Проверим работают
ли эти функции:
*Fix> :r
[1 of 1] Compiling Fix
( Fix. hs, interpreted )
Ok, modules loaded: Fix.
*Fix> takeL 3 $ iterateL (+1) zero
(Cons (Zero) (Cons (Succ (Zero)) (Cons (Succ (Succ (Zero))) (Nil))))
*Fix> let x = 1 ‘cons‘ 2 ‘cons‘ 3 ‘cons‘ nil
*Fix> mapL (+10) $ x ‘concatL‘ x
(Cons 11 (Cons 12 (Cons 13 (Cons 11 (Cons 12 (Cons 13 (Nil)))))))
Обратите внимание, на то что с большими буквами мы пишем Cons и Nil когда хотим закодировать
функции для свёртки-развёртки, а с маленькой буквы пишем значения рекурсивного типа. Надеюсь, что вы
разобрались на примерах как устроены функции fold и unfold, потому что теперь мы перейдём к теории,
которая за этим стоит.
Программирование в стиле оригами | 243
16.2 Индуктивные и коиндуктивные типы
С точки зрения теории категорий функция свёртки является катаморфизмом, а функция развёртки – ана-
морфизмом. Напомню, что катаморфизм – это функция которая ставит в соответствие объектам категории
с начальным объектом стрелки, которые начинаются из начального объекта, а заканчиваются в данном объ-
екте. Анаморфизм – это перевёрнутый наизнанку катаморфизм.
Начальным и конечным объектом будет рекурсивный тип. Вспомним тип свёртки:
fold :: Functor f => (f a -> a) -> (Fix f -> a)
Функция свёртки строит функции, которые ведут из рекурсивного типа в произвольный тип, поэтому в
данном случае рекурсивный тип будет начальным объектом. Функция развёртки строит из произвольного
типа данный рекурсивный тип, на языке теории категорий она строит стрелку из произвольного объекта в
рекурсивный, это означает что рекурсивный тип будет конечным объектом.
unfold :: Functor f => (a -> f a) -> (a -> Fix f)
Категории, которые определяют рекурсивные типы таким образом называются (ко)алгебрами функторов.
Видите в типе и той и другой функции стоит требование о том, что f является функтором. Катаморфизм и
анаморфизм отображают объекты в стрелки. По типу функций fold и unfold мы можем сделать вывод, что
объектами в нашей категории будут стрелки вида
f a -> a
или для свёрток:
a -> f a
А стрелками будут обычные функции одного аргумента. Теперь дадим более формальное определение.
Эндофунктор F : A → A определяет стрелки α : F A → A, которые называется F - алгебрами. Стрелку
h : A → B называют F - гомоморфизмом, если следующая диаграмма коммутирует:
F A
α
A
F h
h
F B
B
β
Или можно сказать по другому, для F -алгебр α : F A → A и β : F B → B выполняется:
F h ; β = α ; h
Это свойство совпадает со свойством естественного преобразования только вместо одного из функторов
мы подставили тождественный функтор I. Определим категорию Alg( F ), для категории A и эндофунктора
F : A → A
• Объектами являются F -алгебры F A → A, где A – объект категории A
• Два объекта α : F A → A и β : F B → B соединяет F -гомоморфизм h : A → B. Это такая стрелка из
A, для которой выполняется:
F h ; β = α ; h
• Композиция и тождественная стрелка взяты из категории A.
Если в этой категории есть начальный объект inF : F T → T , то определён катаморфизм, который
переводит объекты F A → A в стрелки T → A. Причём следующая диаграмма коммутирует:
in
F T
F
T
F ( | α |)
( | α |)
F A
A
α
Этот катаморфизм и будет функцией свёртки для рекурсивного типа . Понятие Alg( F ) можно перевернуть
и получить категорию CoAlg( F ).
244 | Глава 16: Категориальные типы
• Объектами являются F -коалгебры A → F A, где A – объект категории A
• Два объекта α : F A → A и β : F B → B соединяет F -когомоморфизм h : A → B. Это такая стрелка
из A, для которой выполняется:
h ; α = β ; F h
• Композиция и тождественная стрелка взяты из категории A.
Если в этой категории есть конечный объект, его называют outF : T → F T , то определён анаморфизм,
который переводит объекты A → F A в стрелки A → T .
Причём следующая диаграмма коммутирует:
in
T
F
F T
[( α )]
F [( α )]
A
F A
α
Если для категории A и функтора F определены стрелки inF и outF , то они являются взаимнообратными
и определяют изоморфизм T ∼
= F T . Часто объект T в случае Alg( F ) обозначают µF , поскольку начальный
объект определяется функтором F , а в случае CoAlg( F ) обозначают νF .
Типы, которые являются начальными объектами, принято называть индуктивными, а типы, которые яв-
ляются конечными объектами – коиндуктивными.
Существование начальных и конечных объектов
Мы говорили, что если начальный(конечный) объект существует, а когда он существует? Рассмотрим
один важный случай. Если категория является категорией, в которой объектами являются полные частично
упорядоченные множества, а стрелками являются монотонные функции, такие категории называют CPO, и
функтор – полиномиальный, то начальный и конечный объекты существуют.
Полные частично упорядоченные множества
Оказывается на значениях можно ввести частичный порядок. Порядок называется частичным, если отно-
шение ≤ определено не для всех элементов, а лишь для некоторых из них. Частичный порядок на значениях
отражает степень неопределённости значения. Самый маленький объект это полностью неопределённое зна-
чение ⊥. Любое значение типа содержит больше определённости чем ⊥.
Для того чтобы не путать упорядочивание значений по степени определённости с обычным числовым
порядком, пользуются специальным символом . Запись
a
b
означает, что b более определено (или информативнее) чем a.
Так для логических значений определены два нетривиальных сравнения:
data Bool = T rue | F alse
⊥
T rue
⊥
F alse
Мы будем называть нетривиальными сравнения в которых, компоненты слева и справа от не равны. На-
пример ясно, что T rue
T rue или ⊥
⊥. Это тривиальные сравнения и мы их будем лишь подразумевать.
Считается, что если два значения определены полностью, то мы не можем сказать какое из них информатив-
нее. Так к примеру для логических значений мы не можем сказать какое значение более определено T rue
или F alse.
Рассмотрим пример по-сложнее. Частично определённые значения:
data M aybe a = N othing | Just a
Индуктивные и коиндуктивные типы | 245
⊥
N othing
⊥
J ust ⊥
⊥
J ust a
J ust a
J ust b,
если a
b
Если вспомнить как происходит вычисление значения, то значение a менее определено чем b, если взрыв-
ное значение ⊥ в a находится ближе к корню значения, чем в b. Итак получается, что в категории Hask объ-
екты это множества с частичным порядком. Что означает требование монотонности функции?
Монотонность в контексте операции
говорит о том, что чем больше определён вход функции тем больше
определён выход:
a
b
⇒ f a
f b
Это требование накладывает запрет на возможность проведения сопоставления с образцом по значению
⊥. Иначе мы можем определять немонотонные функции вроде:
isBot :: Bool -> Bool
isBot undefined = True
isBot _
= undefined
Полнота частично упорядоченного множества означает, что у любой последовательности xn
x 0
x 1
x 2
...
есть значение x, к которому она сходится. Это значение называют супремумом множества. Что такое
полные частично упорядоченные множества мы разобрались. А что такое полиномиальный функтор?
Полиномиальный функтор
Полиномиальный функтор – это функтор который построен лишь с помощью операций суммы, произве-
дения, постоянных функторов, тождественного фуктора и композиции функторов. Определим эти операции:
• Сумма функторов F и G определяется через операцию суммы объектов:
( F + G) X = F X + GX
• Произведение функторов F и G определяется через операцию произведения объектов:
( F × G) X = F X × GX
• Постоянный функтор отображает все объекты категории в один объект, а стрелки в тождественнубю
стрелку этого объекта, мы будем обозначать постоянный функтор подчёркиванием:
AX
=
A
Af
=
idA
• Тождественный функтор оставляет объекты и стрелки неизменными:
IX
=
X
If
=
f
• Композиция функторов F и G это последовательное применение функторов
F GX = F ( GX)
246 | Глава 16: Категориальные типы
По определению функции построенные с помощью этих операций называют полиномиальными. Опреде-
лим несколько типов данных с помощью полиномиальных функторов. Определим логические значения:
Bool = µ(1 + 1)
Объект 1 обозначает любую константу, это конечный объект исходной категории. Нам не важны имена
конструкторов, но важна структура типа. µ обозначает начальный объект в F -алгебре.
Определим натуральные числа:
N at = µ(1 + I)
Эта запись обозначает начальный объект для F -алгебры с функтором F = 1 + I. Посмотрим на опреде-
ление списка:
ListA = µ(1 + A × I)
Список это начальный объект F -алгебры 1 + A × I. Также можно определить бинарные деревья:
BT reeA = µ( A + I × I)
Определим потоки:
StreamA = ν( A × I)
Потоки являются конечным объектом F -коалгебры, где F = A × I.
16.3 Гиломорфизм
Оказывается, что с помощью катаморфизма и анаморфизма мы можем определить функцию fix, то есть
мы можем выразить любую рекурсивную функцию с помощью структурной рекурсии.
Функция fix строит бесконечную последовательность применений некоторой функции f.
f (f (f ... )))
Сначала с помощью анаморфизма мы построим бесконечный список, который содержит функцию f во
всех элементах:
repeat f = f : f : f : ...
А затем заменим конструктор : на применение. В итоге мы получим такую функцию:
fix :: (a -> a) -> a
fix = foldr ($) undefined . repeat
Убедимся, что эта функция работает:
Prelude> let fix = foldr ($) undefined . repeat
Prelude> take 3 $ y (1:)
[1,1,1]
Prelude> fix (\f n -> if n==0 then 0 else n + f (n-1)) 10
55
Теперь давайте определим функцию fix через функции cata и ana:
fix :: (a -> a) -> a
fix = cata (\(Cons f a) -> f a) . ana (\a -> Cons a a)
Эта связка анаморфизм с последующим катаморфизмом встречается так часто, что ей дали специальное
имя. Гиломорфизмом называют функцию:
hylo :: Functor f => (f b -> b) -> (a -> f a) -> (a -> b)
hylo phi psi = cata phi . ana psi
Отметим, что эту функцию можно выразить и по-другому:
Гиломорфизм | 247
hylo :: Functor f => (f b -> b) -> (a -> f a) -> (a -> b)
hylo phi psi = phi . (fmap $ hylo phi psi) . psi
Этот вариант более эффективен по расходу памяти, мы не строим промежуточное значение Fix f, а сразу
обрабатываем значения в функции phi по ходу их построения в функции psi. Давайте введём инфиксную
операцию гиломорфизм для этого определения:
(>> ) :: Functor f => (a -> f a) -> (f b -> b) -> (a -> b)
psi >> phi = phi . (fmap $ hylo phi psi) . psi
Теперь давайте скроем одноимённую функцию из Prelude и определим несколько рекурсивных функций
с помощью гиломорфизма. Начнём с функции вычисления суммы чисел от нуля до данного числа:
sumInt :: Int -> Int
sumInt = range >> sum
sum x = case x of
Nil
-> 0
Cons a b -> a + b
range n
| n == 0
= Nil
| otherwise = Cons n (n-1)
Сначала мы создаём в функции range список всех чисел от данного числа до нуля. А затем в функции
sum складываем значения. Теперь мы можем легко определить функцию вычисления факториала:
fact :: Int -> Int
fact = range >> prod
prod x = case x of
Nil
-> 1
Cons a b -> a * b
Напишем функцию, которая извлекает из потока n-тый элемент. Сначала определим тип для потока:
type Stream a = Fix (S a)
data S a b = a :& b
deriving (Show, Eq)
instance Functor (S a) where
fmap f (a :& b) = a :& f b
headS :: Stream a -> a
headS x = case unFix x of
(a :& _) -> a
tailS :: Stream a -> Stream a
tailS x = case unFix x of
(_ :& b) -> b
Теперь функцию извлечения элемента:
getElem :: Int -> Stream a -> a
getElem = curry (enum >> elem)
where elem ((n, a) :& next)
| n == 0
= a
| otherwise = next
enum (a, st) = (a, headS st) :& (a-1, tailS st)
В функции enum мы добавляем к элементам потока убывающую последовательность чисел, она стартует
из данного числа. Элемент, который нам нужен, будет содержать в этой последовательности число ноль. В
функции elem мы как раз и извлекаем тот элемент рядом с которым хранится число ноль. Обратите внима-
ние на то, что рекурсия встроена в этот алгоритм, если данное число не равно нулю, мы просто извлекаем
следующий элемент.
С помощью этой функции мы можем вычислить n-тое число из ряда чисел Фибоначчи. Сначала создадим
поток чисел Фибоначчи:
248 | Глава 16: Категориальные типы
fibs :: Stream Int
fibs = ana (\(a, b) -> a :& (b, a+b)) (0, 1)
Теперь просто извлечём n-тый элемент из потока чисел Фибоначчи:
fib :: Int -> Int
fib = flip getElem fibs
Вычислим поток всех простых чисел. Мы будем вычислять его по алгоритму “решето Эратосфена”. В
начале алгоритма у нас есть поток целых чисел и известно, что первое число является простым.
2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 …
В процессе этого алгоритма мы вычёркиваем все не простые числа. Сначала мы ищем первое не зачёркну-
тое число и помещаем его в результирующий поток, а на следующий шаг алгоритма мы передаём исходный,
поток в котором зачёркнуты все числа кратные тому, что мы положили последним:
2
3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, …
Теперь мы ищем первое незачёркнутое число и помещаем его в результат. А на следующий шаг рекусии
передаём поток, в котором зачёркнуты все числа кратные новому простому числу:
2, 3
ТЕЛЕГРАМКанал с обзорами, анонсами новинок и книжными подборками
Книжный Вестник
Бот для удобного поиска книг (если не нашлось на сайте)
Поиск книг
Свежие любовные романы в удобных форматах
Любовные романы
О психологии, саморазвитии и личностном росте
Саморазвитие
Детективы и триллеры, все новинки
Детективы
Фантастика и фэнтези, все новинки
Фантастика
Отборные классические книги
Классика
ВКОНТАКТЕБиблиотека с любовными романами, которая наверняка придётся по вкусу женской части аудитории
Любовные романы
Библиотека с фантастикой и фэнтези, а также смежных жанров
Фантастика
Самые популярные книги в формате фб2
Топ фб2
книги