s
(Succ n)
= s (foldNat z s n)
Необходимо привести его к виду:
x = f x
Слева и справа мы видим повторяются выражения foldNat z s, обозначим их за x:
x :: Nat -> a
x Zero
= z
x (Succ n)
= s (x n)
Теперь перенесём первый аргумент в правую часть, сопоставление с образцом превратится в case-
выражение:
x :: Nat -> a
x = \nat -> case nat of
Zero
-> z
Succ n
-> s (x n)
В правой части вынесем x из выражения с помощью лямбда функции:
x :: Nat -> a
x = (\t -> \nat -> case nat of
Zero
-> z
Succ n
-> s (t n)) x
Смотрите мы обозначили вхождение x в выражении справа за t и создали лямбда-функцию с таким ар-
гументом. Так мы вынесли x из выражения.
Получилось, мы пришли к виду комбинатора неподвижной точки:
x :: Nat -> a
x = f x
where f = \t -> \nat -> case nat of
Zero
-> z
Succ n
-> s (t n)
Приведём в более человеческий вид:
foldNat :: a -> (a -> a) -> (Nat -> a)
foldNat z s = fix f
where f t = \nat -> case nat of
Zero
-> z
Succ n
-> s (t n)
Комбинатор неподвижной точки | 83
5.6 Краткое содержание
Основные функции высшего порядка
Мы познакомились с функциями из модуля Data.Function. Их можно разбить на несколько типов:
• Примитивные функции (генераторы функций).