< 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. Нам нужно узнать тип выражения и проверить правильно ли оно построено.
not (Succ Zero) - ?
not :: Bool -> Bool,
Succ :: Nat -> Nat,
Zero :: Nat
----------------------------------------------------------
f x, f = not и x = (Succ Zero)
------------------------------------------------------------
f :: Bool -> Bool следовательно x :: Bool
-------------------------------------------------------------
(Succ Zero) :: Bool
Воспользовавшись правилом применения мы узнали, что тип выражения Succ Zero должен быть равен
Bool. Проверим, так ли это?
(Succ Zero) - ?
Succ :: Nat -> Nat,
Zero :: Nat
----------------------------------------------------------
f x, f = Succ, x = Zero следовательно (f x) :: Nat
----------------------------------------------------------
(Succ Zero) :: Nat
Из этой цепочки следует, что (Succ Zero) имеет тип Nat. Мы пришли к противоречию и сообщаем об
этом пользователю.
< interactive>:1:5:
Не могу сопоставить ожидаемый тип ’Bool’ с выведенным ’Nat’
В типе результата вызова ‘Succ’
В первом аргументе ‘not’, а именно ‘(Succ Zero)’
В выражении: not (Succ Zero)
Потренируйтесь в составлении неправильных выражений и посмотрите почему они не правильные. Мыс-
ленно сверьтесь с правилом применения в каждом из слагаемых.
Специализация типов при подстановке
Мы говорили о том, что тип аргумента функции и тип подставляемого значения должны совпадать, но
на самом деле есть и другая возможность. Тип аргумента или тип значения могут быть полиморфными. В
этом случае происходит специализация общего типа. Например, при выполнении выражения:
*Nat> Succ Zero + Zero
Succ (Succ Zero)
Происходит специализация общей функции (+) :: Num a => a -> a -> a до функции (+) :: Nat ->
Nat -> Nat, которая определена в экземпляре Num для Nat.
Проверка типов с контекстом
Предположим, что у функции f есть контекст, который говорит о том, что первый аргумент принадлежит
некоторому классу f :: C a => a -> b, тогда значение, которое мы подставляем в функцию, должно быть
экземпляром класса C.
Для иллюстрации давайте попробуем сложить логические значения:
*Nat Prelude> True + False
< interactive>:11:6:
No instance for (Num Bool)
arising from a use of ‘+’
Possible fix: add an instance declaration for (Num Bool)
In the expression: True + False
In an equation for ‘it’: it = True + False
Компилятор говорит о том, что для типа Bool не
определён экземпляр для класса Num.
Проверка типов | 51
No instance for (Num Bool)