Unknown - haskell-notes

могут получиться, если мы пользуемся переменными. Конструкторы дают нам возможность зафиксировать

вид ожидаемого на вход дерева.

Структура функций | 49

3.4 Проверка типов

В этом разделе мы поговорим об ошибках проверки типов. Почти все ошибки, которые происходят в

Haskell, связаны с проверкой типов. Проверка типов происходит согласно правилам применения, которые

встретились нам в разделе о композиции значений. Мы остановимся лишь на случае для префиксной формы

записи, правила для сечений работают аналогично. Давайте вспомним основное правило:

f ::a ->b,

x ::a

--------------------------

(f x) ::b

Что может привести к ошибке? В этом правиле есть два источника ошибки.

• Тип f не содержит стрелок, или f не является функцией.

• Типы x и аргумента для f не совпадают.

Вот и все ошибки. Универсальное представление всех функций в виде функций одного аргумента, значи-

тельно сокращает число различных видов ошибок. Итак мы можем ошибиться применяя значение к константе

и передав в функцию не то, что она ожидает.

Потренируемся в интерпретаторе, сначала попытаемся создать ошибку первого типа:

*Nat> Zero Zero

<interactive >:1 :1 :

Thefunction ‘ Zero’is applied to one argument,

but its type‘ Nat’has none

Inthe expression : Zero Zero

Inan 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 :

Thefunction ‘ True’is applied to one argument,

but its type‘ Bool’has none

Inthe expression : True Succ

Inan 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’tmatch expected type‘ Bool’with actual type‘ Nat’

Inthe return type ofa call of‘ Succ’

Inthe 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)’