Подсказка: если совсем не получается, ответ можно подсмотреть в библиотеке TypeCompose. Но пока мы
не знаем как устанавливать библиотеки и где они живут, всё-таки попытайтесь решить это упражнение
самостоятельно.
Упражнения | 141
Глава 9
Редукция выражений
В этой главе мы поговорим о том как вычисляются программы. В самом начале мы говорили о том, что
процесса вычисления значений нет. В том смысле, что у нас нет новых значений, у нас ничего не меняется,
мы лишь расшифровываем синонимы значений.
Вкратце вспомним то, что мы уже знаем о вычислениях. Сначала мы с помощью типов определяем мно-
жество всех возможных значений. Значения – это деревья в узлах которых записаны конструкторы, которые
мы определяем в типах. Так например мы можем определить тип:
data Nat = Zero | Succ Nat
Этим типом мы определяем множество допустимых значений. В данном случае это цепочки конструкто-
ров Succ, которые заканчиваются конструктором Zero:
Zero, Succ Zero, Succ (Succ Zero), ...
Затем начинаем давать им новые имена, создавая константы (простые имена-синонимы)
zero
= Zero
one
= Succ zero
two
= Succ one
и функции (составные имена-синонимы):
foldNat :: a -> (a -> a) -> Nat -> a
foldNat z
s
Zero
= z
foldNat z
s
(Succ n)
= s (foldNat z s n)
add a = foldNat a
Succ
mul a = foldNat one (add a)
Затем мы передаём нашу программу на проверку компилятору. Мы просим у него проверить не создаём
ли мы случайно какие-нибудь бессмысленные выражения. Бессмысленные потому, что они пытаются создать
значение, которое не вписывается в наши типы. Например если мы где-нибудь попробуем составить выра-
жение:
add Zero mul
Компилятор напомнит нам о том, что мы пытаемся подставить функцию mul на место обычного значения
типа Nat. Тогда мы исправим выражение на:
add Zero two
Компилятор согласится. И передаст выражение вычислителю. И тут мы говорили, что вычислитель начи-
нает проводить расшифровку нашего описания. Он подставляет на место синонимов их определения, правые
части из уравнений. Этот процесс мы называли редукцией. Вычислитель видит два синонима и одно значение.
С какого синонима начать? С add или two?
142 | Глава 9: Редукция выражений
9.1 Стратегии вычислений
Этот вопрос приводит нас к понятию стратегии вычислений. Поскольку вычисляем мы только константы,
то наше выражение также можно представить в виде дерева. Только теперь у нас в узлах записаны не только
конструкторы, но и синонимы. Процесс редукции можно представить как процесс очистки такого дерева от
синонимов. Посмотрим на дерево нашего значения:
Оказывается у нас есть две возможности очистки синонимов.
Cнизу-вверх начинаем с листьев и убираем все синонимы в листьях дерева выражения. Как только в данном
узле и всех дочерних узлах остались одни конструкторы можно переходить на уровень выше. Так мы
поднимаемся выше и выше пока не дойдём до корня.
Cверху-вниз начинаем с корня, самого внешнего синонима и заменяем его на определение (с помощью урав-
нения на правую часть от знака равно), если на верху снова окажется синоним, мы опять заменим его
на определение и так пока на верху не появится конструктор, тогда мы спустимся в дочерние деревья
и будем повторять эту процедуру пока не дойдём до листьев дерева.
Посмотрим как каждая из стратегий будет редуцировать наше выражение. Начнём со стратегии от ли-
стьев к корню (снизу-вверх):
add Zero two
-- видим два синонима add и two
-- раскрываем two, ведь он находится ниже всех синонимов
=>
add Zero (Succ one)
-- ниже появился ещё один синоним, раскроем и его
=>
add Zero (Succ (Succ zero))
-- появился синоним zero раскроем его
=>
add Zero (Succ (Suсс Zero))
-- все узлы ниже содержат конструкторы, поднимаемся вверх до синонима
-- заменяем add на его правую часть
=>
foldNat Succ Zero (Succ (Succ Zero))
-- самый нижний синоним foldNat, раскроем его
-- сопоставление с образцом проходит во втором уравнении для foldNat
=>
Succ (foldNat Succ Zero (Succ Zero))
-- снова раскрываем foldNat
=>
Succ (Succ (foldNat Zero Zero))