Unknown - haskell-notes

В выражении: not (Succ Zero)

Потренируйтесь в составлении неправильных выражений и посмотрите почему они не правильные. Мыс-

ленно сверьтесь с правилом применения в каждом из слагаемых.

Специализация типов при подстановке

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

на самом деле есть и другая возможность. Тип аргумента или тип значения могут быть полиморфными. В

этом случае происходит специализация общего типа. Например, при выполнении выражения:

*Nat> Succ Zero + Zero

Succ( Succ Zero)

Происходит специализация общей функции ( +) :: Numa =>a ->a ->a до функции ( +) :: Nat ->

Nat -> Nat, которая определена в экземпляре Numдля Nat.

Проверка типов с контекстом

Предположим, что у функции f есть контекст, который говорит о том, что первый аргумент принадлежит

некоторому классу f :: Ca =>a ->b, тогда значение, которое мы подставляем в функцию, должно быть

экземпляром класса C.

Для иллюстрации давайте попробуем сложить логические значения:

*Nat Prelude> True + False

<interactive >:11 :6 :

No instancefor ( 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 instancefor ( Num Bool)

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

f :: Ca =>a ->b,

x :: T, instance C T

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

(f x) ::b

Важно отметить, что x имеет конкретный тип T. Если x – значение, у которого тип с параметром, компиля-

тор не сможет определить для какого типа конкретно мы хотим выполнить применение. Мы будем называть

такую ситуацию неопределённостью:

x :: Ta =>a

f :: Ca =>a ->b

f x :: ??

-- неопределённость

Мы видим, что тип x, это какой-то тип, одновременно принадлежащий и классу Tи классу C. Но мы не

можем сказать какой это тип. У этого поведения есть исключение: по умолчанию числа приводятся к Integer,

если они не содержат знаков после точки, и к Double– если содержат.

*Nat Prelude> letf =(1.5 +)

*Nat Prelude> :t f

f :: Double -> Double

*Nat Prelude> letx =5 +0

*Nat Prelude> :t x

x :: Integer

*Nat Prelude> letx =5 + Zero

*Nat Prelude> :t x

x :: Nat

Умолчания определены только для класса Num. Для этого есть специальное ключевое слово default. В

рамках модуля мы можем указать какие типы считаются числами по умолчанию. Например, так (такое умол-

чание действует в каждом модуле, но мы можем переопределить его):

default( Integer, Double)

Работает правило: если произошла неопределённость и один из участвующих классов является Num, а все

остальные классы – это стандартные классы, определённые в Prelude, то компилятор начинает последова-

тельно пробовать все типы, перечисленые за ключевым словом default, пока один из них не подойдёт. Если

такого типа не окажется, компилятор скажет об ошибке.

Ограничение мономорфизма

С выводом типов в классах связана одна тонкость. Мы говорили, что не обязательно выписывать типы

выражений, компилятор может вывести их самостоятельно. Например, мы постоянно пользуемся этим в ин-

терпретаторе. Также когда мы говорили о частичном применении, мы сказали об очень полезном умолчании

в типах функций. О том, что за счёт частичного применения, все функции являются функциями одного аргу-

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

краткими, и вводят компилятор в заблуждение. Зайдём в интерпретатор:

Prelude> letadd =( +)

Prelude> :t add

add :: Integer -> Integer -> Integer

Мы хотели определить синоним для метода плюс из класса Num, но вместо ожидаемого общего типа

получили более частный. Сработало умолчание для численного типа. Но зачем оно сработало? Если мы

попробуем дать синоним методу из класса Eq, ситуация станет ещё более странной: