Unknown - haskell-notes

мы лишь расшифровываем синонимы значений.

Вкратце вспомним то, что мы уже знаем о вычислениях. Сначала мы с помощью типов определяем мно-

жество всех возможных значений. Значения – это деревья в узлах которых записаны конструкторы, которые

мы определяем в типах. Так например мы можем определить тип:

data Nat = Zero | Succ Nat

Этим типом мы определяем множество допустимых значений. В данном случае это цепочки конструкто-

ров Succ, которые заканчиваются конструктором Zero:

Zero, Succ Zero, Succ( Succ Zero), ...

Затем начинаем давать им новые имена, создавая константы (простые имена-синонимы)

zero

= Zero

one

= Succzero

two

= Succone

и функции (составные имена-синонимы):

foldNat ::a ->(a ->a) -> Nat ->a

foldNat z

s

Zero

=z

foldNat z

s

( Succn)

=s (foldNat z s n)

add a =foldNat a

Succ

mul a =foldNat one (add a)

Затем мы передаём нашу программу на проверку компилятору. Мы просим у него проверить не создаём

ли мы случайно какие-нибудь бессмысленные выражения. Бессмысленные потому, что они пытаются создать

значение, которое не вписывается в наши типы. Например если мы где-нибудь попробуем составить выра-

жение:

add Zeromul

Компилятор напомнит нам о том, что мы пытаемся подставить функцию mul на место обычного значения

типа Nat. Тогда мы исправим выражение на:

add Zerotwo

Компилятор согласится. И передаст выражение вычислителю. И тут мы говорили, что вычислитель начи-

нает проводить расшифровку нашего описания. Он подставляет на место синонимов их определения, правые

части из уравнений. Этот процесс мы называли редукцией . Вычислитель видит два синонима и одно значение.

С какого синонима начать? С add или two?

142 | Глава 9: Редукция выражений

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

Этот вопрос приводит нас к понятию стратегии вычислений. Поскольку вычисляем мы только константы,

то наше выражение также можно представить в виде дерева. Только теперь у нас в узлах записаны не только

конструкторы, но и синонимы. Процесс редукции можно представить как процесс очистки такого дерева от

синонимов. Посмотрим на дерево нашего значения:

Оказывается у нас есть две возможности очистки синонимов.

Cнизу-вверх начинаем с листьев и убираем все синонимы в листьях дерева выражения. Как только в данном

узле и всех дочерних узлах остались одни конструкторы можно переходить на уровень выше. Так мы

поднимаемся выше и выше пока не дойдём до корня.

Cверху-вниз начинаем с корня, самого внешнего синонима и заменяем его на определение (с помощью урав-

нения на правую часть от знака равно), если на верху снова окажется синоним, мы опять заменим его

на определение и так пока на верху не появится конструктор, тогда мы спустимся в дочерние деревья

и будем повторять эту процедуру пока не дойдём до листьев дерева.

Посмотрим как каждая из стратегий будет редуцировать наше выражение. Начнём со стратегии от ли-

стьев к корню (снизу-вверх):

add Zerotwo

-- видим два синонима add и two

-- раскрываем two, ведь он находится ниже всех синонимов

=>

add Zero( Succone)

-- ниже появился ещё один синоним, раскроем и его

=>

add Zero( Succ( Succzero))

-- появился синоним 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))

-- снова раскрываем foldNat, но на этот раз нам подходит

-- первое уравнение из определения foldNat

=>

Succ( Succ Zero)

-- синонимов больше нет можно вернуть значение

-- результат:

Succ( Succ Zero)

В этой стратегии для каждой функции мы сначала вычисляем до конца все аргументы, потом подставляем

расшифрованные значения в определение функции.

Теперь посмотрим на вычисление от корня к листьям (сверху-вниз):