=>
| M
= Succ M1
| M1 = Succ M2
| M2 = Zero
-- выбираем первое уравнение для foldNat:
|
=> Succ (Succ (add M M))
|
-- раскрываем самый верхний синоним:
|
=> Succ (Succ (foldNat M Succ M))
|
-- теперь, поскольку M уже вычислялось, в
|
-- памяти уже записан верхний конструктор,
|
-- мы знаем, что это Succ и выбираем второе |
-- уравнение:
|
=> Succ (Succ (Succ (foldNat M Succ M1)))
|
-- и M1 тоже уже вычислялось, сразу
|
-- выбираем второе уравнение
|----+
=> Succ (Succ (Succ (Succ (foldNat M Succ M2)))) |
-- M2 вычислено, идём на первое уравнение
|----+
=> Succ (Succ (Succ (Succ (Succ M))))
|
-- далее остаётся только подставить уже
|
-- вычисленные значения M
|
-- и вернуть значение.
|
Итак подставляется не значение а ссылка на него, вычисленная часть значения используется сразу в
нескольких местах. Эта стратегия редукции называется вычислением по необходимости (call by need) или
ленивой стратегией вычислений (lazy evaluation).
Теперь немного терминологии. Значение может находится в четырёх состояниях:
• Нормальная форма (normal form, далее НФ), когда оно полностью вычислено (нет синонимов);
• Слабая заголовочная НФ (weak head NF, далее СЗНФ), когда известен хотя бы один верхний конструк-
тор;
• Отложенное вычисление (thunk), когда известен лишь рецепт вычисления;
• Дно (bottom, часто рисуют как ⊥), когда известно, что значение не определено.
Вы могли понаблюдать за значением в первых трёх состояниях на примере выше. Но что такое ⊥? Вспом-
ним определение для функции извлечения головы списка head:
head :: [a] -> a
head (a:_)
= a
head []
= error ”error: empty list”
Второе уравнение возвращает ⊥. У нас есть две функции, которые возвращают это “значение”:
undefined
:: a
error
:: String -> a
146 | Глава 9: Редукция выражений
Первая – это ⊥ в чистом виде, а вторая не только возвращает неопределённое значение, но и приводит
к выводу на экран сообщения об ошибке. Обратите внимание на тип этих функций, результат может быть
значением любого типа. Это наблюдение приводит нас к ещё одной тонкости. Когда мы определяем тип:
data Bool
= False | True
data Maybe a
= Nothing | Just a
На самом деле мы пишем:
data Bool
= undefined | False | True
data Maybe a
= undefined | Nothing | Just a
Компилятор автоматически прибавляет ещё одно значение к любому определённому пользователем ти-
пу. Такие типы называют поднятыми (lifted type). А значения таких типов принято называть запакованными
(boxed). Не запакованное (unboxed) значение – это простое примитивное значение. Например целое или дей-
ствительное число в том виде, в котором оно хранится на компьютере. В Haskell даже числа “запакованы”.
Поскольку нам необходимо, чтобы undefined могло возвращать в том числе и значение типа Int:
data Int = undefined
| I# Int#
Тип Int# – это низкоуровневое представление ограниченного целого числа. Принято писать не запа-
кованные типы с решёткой на конце. I# – это конструктор. Нам приходится запаковывать значения ещё и
потому, что значение может принимать несколько состояний (в зависимости от того, насколько оно вычис-
лено), всё это ведёт к тому, что у нас хранится не просто значение, а значение с какой-то дополнительной
информацией, которая зависит от конкретной реализации языка Haskell.
Мы решили проблему дублирования вычислений, но наше решение усугубило проблему расхода памяти.
Ведь теперь мы храним не просто значения, но ещё и дополнительную информацию, которая отвечает за
проведение вычислений. Эта проблема может проявляться в очень простых задачах. Например попробуем
вычислить сумму чисел от одного до миллиарда:
sum [1 .. 1e9]
< interactive>: out of memory (requested 2097152 bytes)
Интуитивно кажется, что для решения этой задачи нам нужно лишь две ячейки памяти. В одной мы бу-
дем постоянно прибавлять к значению единицу, пока не дойдём до миллиарда, так мы последовательно
будем получать элементы списка, а в другой мы будем хранить значение суммы. Мы начнём с нуля и будем