*Nat> let minus = (—)
*Nat> (2 ‘minus‘ ) 1
1
*Nat> ( ‘minus‘ 2) 1
—1
Так если мы хотим на лету получить новую функцию, связав в функции второй аргумент мы можем
написать:
… = … ( ‘fun‘ x) …
Частичное применение для функций в инфиксной форме записи называют сечением (section), они бывают
соответственно левыми и правыми.
Связь с логикой
Отметим связь основного правила применения с Modus Ponens, известным правилом вывода в логике:
a -> b,
a
————-
b
Оно говорит о том, что если у нас есть выражение из a следует b и мы знаем, что a истинно, мы смело
можем утверждать, что b тоже истинно. Если перевести это правило на Haskell, то мы получим: Если у нас
определена функция типа a -> b и у нас есть значение типа a, то мы можем получить значение типа b.
Декомпозиция и сопоставление с образцом
Декомпозиция применяется слева от знака равно, при этом наша задача состоит в том, чтобы опознать
дерево определённого вида и выделить из него некоторые поддеревья. Мы уже пользовались декомпозицией
много раз в предыдущих главах, давайте выпишем примеры декомпозиции:
not :: Bool -> Bool
not True
= …
not False
= …
xor :: Bool -> Bool -> Bool
xor a b = …
show :: Show a => a -> String
show (Time h m s) = …
addZero :: String -> String
addZero (a:[])
= …
addZero as
= …
(*)
a
Zero
= …
(*)
a
(Succ b)
= …
48 | Глава 3: Типы
Декомпозицию можно проводить в аргументах функции. Там мы видим строчную запись дерева, в узлах
стоят конструкторы (начинаются с большой буквы), переменные (с маленькой буквы) или символ безразлич-
ной переменой (подчёркивание).
С помощью конструкторов, мы указываем те части, которые обязательно должны быть в дереве для дан-
ного уравнения. Так уравнение
not True
= …
сработает, только если на вход функции поступит значение True. Мы можем углубляться в дерево значе-
ния настолько, насколько нам позволят типы, так мы можем определить функцию:
is7 :: Nat -> Bool
is7
(Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))
= True
is7
_
= False
С помощью переменных мы даём синонимы поддеревьям. Этими синонимами мы можем пользоваться в
правой части функции. Так в уравнении
addZero (a:[])
мы извлекаем первый элемент из списка, и одновременно говорим о том, что список может содержать
только один элемент. Отметим, что если мы хотим дать синоним всему дереву а не какой-то части, мы просто
пишем на месте аргумента переменную, как в случае функции xor:
xor a b = …
С помощью безразличной переменной говорим, что нам не важно, что находится у дерева в этом узле.
Уравнения в определении синонима обходятся сверху вниз, поэтому часто безразличной переменной поль-
зуются в смысле “а во всех остальных случаях”, как в:
instance Eq Nat where
(==) Zero
Zero
= True
(==) (Succ a) (Succ b) = a == b
(==) _
_
= False
Переменные и безразличные переменные также могут уходить вглубь дерева сколь угодно далеко (или
ввысь дерева, поскольку первый уровень в строчной записи это корень):
lessThan7 :: Nat -> Bool
lessThan7
(Succ (Succ (Succ (Succ (Succ (Succ (Succ _)))))))
= False
lessThan7
_
= True
Декомпозицию можно применять только к значениям-константам. Проявляется интересная закономер-
ность: если для композиции необходимым элементом было значение со стрелочным типом (функция), то в
случае декомпозиции нам нужно значение с типом без стрелок (константа). Это говорит о том, что все функ-
ции будут полностью применены, то есть константы будут записаны в виде строчной записи дерева. Если мы
ожидаем на входе функцию, то мы можем только дать ей синоним с помощью с помощью переменной или
проигнорировать её безразличной переменной.
Как в
name
(Succ (Succ Zero))
= …
name
(Zero : Succ Zero : [])
= …
Но не
name
Succ
= …
name
(Zero :)
= …
Отметим, что для композиции это допустимые значения, в первом случае это функция Nat -> Nat, а во
втором это функция типа [Nat] -> [Nat].
Ещё одна особенность декомпозиции заключается в том, что при декомпозиции мы можем пользоваться
только “настоящими” значениями, то есть конструкторами, объявленными в типах. В случае композиции мы
могли пользоваться как конструкторами, так и синонимами.
Например мы не можем написать в декомпозиции:
name
(add Zero Zero)
= …
name
(or (xor a b) True)
= …
В Haskell декомпозицию принято называть сопоставлением с образцом (pattern matching). Термин намекает
на то, что в аргументе мы выписываем шаблон (или заготовку) для целого набора значений. Наборы значений
могут получиться, если мы пользуемся переменными. Конструкторы дают нам возможность зафиксировать
вид ожидаемого на вход дерева.
Структура функций | 49
3.4 Проверка типов
В этом разделе мы поговорим об ошибках проверки типов. Почти все ошибки, которые происходят в
Haskell, связаны с проверкой типов. Проверка типов происходит согласно правилам применения, которые
встретились нам в разделе о композиции значений. Мы остановимся лишь на случае для префиксной формы
записи, правила для сечений работают аналогично. Давайте вспомним основное правило:
f :: a -> b,
x :: a
—————————
(f x) :: b
Что может привести к ошибке? В этом правиле есть два источника ошибки.
• Тип f не содержит стрелок, или f не является функцией.
• Типы x и аргумента для f не совпадают.
Вот и все ошибки. Универсальное представление всех функций в виде функций одного аргумента, значи-
тельно сокращает число различных видов ошибок. Итак мы можем ошибиться применяя значение к константе
и передав в функцию не то, что она ожидает.
Потренируемся в интерпретаторе, сначала попытаемся создать ошибку первого типа:
*Nat> Zero Zero
< interactive>:1:1:
The function ‘Zero’ is applied to one argument,
but its type ‘Nat’ has none
In the expression: Zero Zero
In an equation for ‘it’: it = Zero Zero
Если перевести на русский интерпретатор говорит:
*Nat> Zero Zero
< interactive>:1:1:
Функция ’Zero’ применяется к одному аргументу,
но её тип ’Nat’ не имеет аргументов
В выражении: Zero Zero
В уравнении для ‘it’: it = Zero Zero
Компилятор увидел применение функции f x, далее он посмотрел, что x = Zero, из этого на основе
правила применения он сделал вывод о том, что f имеет тип Nat -> t, тогда он заглянул в f и нашёл там
Zero :: Nat, что и привело к несовпадению типов.
Составим ещё одно выражение с такой же ошибкой:
*Nat> True Succ
< interactive>:6:1:
The function ‘True’ is applied to one argument,
but its type ‘Bool’ has none
In the expression: True Succ
In an equation for ‘it’: it = True Succ
В этом выражении аргумент Succ имеет тип Nat -> Nat, значит по правилу вывода тип True равен (Nat
-> Nat) -> t, где t некоторый произвольный тип, но мы знаем, что True имеет тип Bool.
Теперь перейдём к ошибкам второго типа. Попробуем вызывать функции с неправильными аргументами:
*Nat> :m +Prelude
*Nat Prelude> not (Succ Zero)
< interactive>:9:6:
Couldn’t match expected type ‘Bool’ with actual type ‘Nat’
In the return type of a call of ‘Succ’
In the first argument of ‘not’, namely ‘(Succ Zero)’
In the expression: not (Succ Zero)
50 | Глава 3: Типы
Опишем действия компилятора в терминах правила применения. В этом выражении у нас есть три зна-
чения: not, Succ и Zero. Нам нужно узнать тип выражения и проверить правильно ли оно построено.
