Учебник по Haskell

В этом выражении аргумент 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)

Запишем это в виде правила:

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)