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)
Запишем это в виде правила:
f :: C a => a -> b,
x :: T, instance C T
——————————————
(f x) :: b
Важно отметить, что x имеет конкретный тип T. Если x – значение, у которого тип с параметром, компиля-
тор не сможет определить для какого типа конкретно мы хотим выполнить применение. Мы будем называть
такую ситуацию неопределённостью:
x :: T a => a
f :: C a => a -> b
f x :: ??
— неопределённость
Мы видим, что тип x, это какой-то тип, одновременно принадлежащий и классу T и классу C. Но мы не
можем сказать какой это тип. У этого поведения есть исключение: по умолчанию числа приводятся к Integer,
если они не содержат знаков после точки, и к Double – если содержат.
*Nat Prelude> let f = (1.5 + )
*Nat Prelude> :t f
f :: Double -> Double
*Nat Prelude> let x = 5 + 0
*Nat Prelude> :t x
x :: Integer
*Nat Prelude> let x = 5 + Zero
*Nat Prelude> :t x
x :: Nat
Умолчания определены только для класса Num. Для этого есть специальное ключевое слово default. В
рамках модуля мы можем указать какие типы считаются числами по умолчанию. Например, так (такое умол-
чание действует в каждом модуле, но мы можем переопределить его):
default (Integer, Double)
Работает правило: если произошла неопределённость и один из участвующих классов является Num, а все
остальные классы – это стандартные классы, определённые в Prelude, то компилятор начинает последова-
тельно пробовать все типы, перечисленые за ключевым словом default, пока один из них не подойдёт. Если
такого типа не окажется, компилятор скажет об ошибке.
Ограничение мономорфизма
С выводом типов в классах связана одна тонкость. Мы говорили, что не обязательно выписывать типы
выражений, компилятор может вывести их самостоятельно. Например, мы постоянно пользуемся этим в ин-
терпретаторе. Также когда мы говорили о частичном применении, мы сказали об очень полезном умолчании
в типах функций. О том, что за счёт частичного применения, все функции являются функциями одного аргу-
мента. Эта особенность позволяет записывать выражения очень кратко. Но иногда они получаются чересчур
краткими, и вводят компилятор в заблуждение. Зайдём в интерпретатор:
Prelude> let add = (+)
Prelude> :t add
add :: Integer -> Integer -> Integer
Мы хотели определить синоним для метода плюс из класса Num, но вместо ожидаемого общего типа
получили более частный. Сработало умолчание для численного типа. Но зачем оно сработало? Если мы
попробуем дать синоним методу из класса Eq, ситуация станет ещё более странной:
Prelude> let eq = (==)
Prelude> :t eq
eq :: () -> () -> Bool
Мы получили какую-то ерунду. Если мы попытаемся загрузить модуль с этими определениями:
52 | Глава 3: Типы
module MR where
add = (+)
eq
= (==)
то получим:
*MR> :l MR
[1 of 1] Compiling MR
( MR. hs, interpreted )
MR. hs:4:7:
Ambiguous type variable ‘a0’ in the constraint:
(Eq a0) arising from a use of ‘==’
Possible cause: the monomorphism restriction applied to the following:
eq :: a0 -> a0 -> Bool (bound at MR.hs:4:1)
Probable fix: give these definition(s) an explicit type signature
or use -XNoMonomorphismRestriction
In the expression: (==)
In an equation for ‘eq’: eq = (==)
Failed, modules loaded: none.
Компилятор жалуется о том, что в определении для eq ему встретилась неопределённость и он не смог
вывести тип. Если же мы допишем недостающие типы:
module MR where
add :: Num a => a -> a -> a
add = (+)
eq :: Eq a => a -> a -> Bool
eq
= (==)
то всё пройдёт гладко:
Prelude> :l MR
[1 of 1] Compiling MR
( MR. hs, interpreted )
Ok, modules loaded: MR.
*MR> eq 2 3
False
Но оказывается, что если мы допишем аргументы у функций и сотрём объявления, компилятор сможет
вывести тип, и тип окажется общим. Это можно проверить в интерпретаторе. Для этого начнём новую сессию:
Prelude> let eq a b = (==) a b
Prelude> :t eq
eq :: Eq a => a -> a -> Bool
Prelude> let add a = (+) a
Prelude> :t add
add :: Num a => a -> a -> a
Запишите эти выражения в модуле без типов и попробуйте загрузить. Почему так происходит? По смыслу
определения
add a b = (+) a b
add
= (+)
ничем не отличаются друг от друга, но второе сбивает компилятор столку. Компилятор путается из-
за того, что второй вариант похож на определение константы. Мы с вами знаем, что выражение справа от
знака равно является функцией, но компилятор, посчитав аргументы слева от знака равно, думает, что это
возможно константа, потому что она выглядит как константа. У таких возможно-констант есть специальное
имя, они называются константными аппликативными формами (constant applicative form или сокращённо
CAF). Константы можно вычислять один раз, на то они и константы. Но если тип константы перегружен,
и мы не знаем что это за тип (если пользователь не подсказал нам об этом в объявлении типа), то нам
