Почему эта функция не выполняет проверку типа?

Во время лекции по функциональному программированию мы увидели следующую функцию Хаскелла: 

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

Ожидается, что эта функция не сможет выполнить проверку типа. Однако причина, по которой это происходит, не была объяснена. Когда я попробовал его в GHCI, я получил следующий результат: 

Prelude> :l test [1 of 1] Compiling Main             ( test.hs,
interpreted )

test.hs:2:35:
    Couldn't match expected type `a' with actual type `Bool'
      `a' is a rigid type variable bound by
          the type signature for f :: Bool -> Int -> (a -> Int) -> Int
          at test.hs:1:6
    Relevant bindings include
      z :: a -> Int (bound at test.hs:2:7)
      f :: Bool -> Int -> (a -> Int) -> Int (bound at test.hs:2:1)
    In the first argument of `z', namely `x'
    In the first argument of `(+)', namely `(z x)' Failed, modules loaded: none.

Почему это происходит?

3 5
haskell polymorphism parametric-polymorphism

3 ответа:

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)
Сигнатура типа утверждает, что наша функция z полиморфна в своем первом аргументе. Он принимает значение любого типа a и возвращает значение Int. Однако область видимости переменной типа a также означает, что она должна быть того же типа a при всех видах использования. a нельзя создавать экземпляры для разных типов на одном и том же сайте использования. Это "полиморфизм 1 ранга".

Вы можете прочитать тип как на самом деле: 

f :: forall a. Bool -> Int -> (a -> Int) -> Int

Итак: 

z (x :: Bool) + z (y :: Int)

Является недопустимым, так как a ограничен два разных, независимых типа.

Расширение языка позволяет нам изменять область действия a таким образом, чтобы она могла быть инстанцирована в полиморфную переменную - т. е. содержать различные типы на одном и том же сайте использования, в том числе иметь полиморфные типы функций: 

Prelude> :set -XRankNTypes

Prelude> let f :: Bool -> Int -> (forall a . a -> Int) -> Int 
             f x y z = if x then y + y else (z x) + (z y)

Теперь Тип a не имеет глобальной области действия, и отдельные экземпляры могут отличаться. Это позволяет нам написать" более полиморфную " функцию f и использовать ее: 

Prelude> f True 7 (const 1)
14

Так вот как круто выше рангом полиморфизм есть. Больше повторного использования кода.

9

Это просто не так, как работает простой параметрический полиморфизм. Функция z полиморфна по сигнатуре функции, но в теле она только мономорфна.

При проверке типа определения средство проверки типа выводит мономорфный тип для переменной типа a для использования во всем определении функции. Однако ваш f пытается вызвать z с двумя различными типами, и таким образом средство проверки типов выводит два конфликтующих типа для a.

3

Даже 

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z y) + (z y)

Не будет проверять тип (как было указано в комментариях) и генерировать ту же ошибку, потому что Хаскелл выводит наименее общие типы для выражений, и ваш тип более общий, чем выводимый. Как говорит "нежное введение в Хаскелла",

Главный тип выражения или функции-это наименее общий тип, который интуитивно "содержит все экземпляры выражения".

Если указать тип в явном виде Хаскелл предполагает, что вы сделали это по какой-то причине, и настаивает на сопоставлении выводимого типа с данным типом.

Для выражения выше выводимый тип является (Num t) => Bool -> t -> (t -> t) -> t, поэтому при сопоставлении типов он видит, что вы дали Int для y и тип z становится (Int -> Int). Который является менее общим, чем (a -> Int). Но Вы настаивали на том, чтобы иметь a там (а не Int) - жесткую переменную типа. Другими словами, ваша функция f может принимать только функции типа Int -> Int, но вы настаиваете на том, что ему может быть дана любая функция :: a -> Int, включая :: String -> Int и т. д. (как указывает @augustsson в комментариях). Ваш объявленный тип слишком широк.

Аналогично, если бы у вас был только один (z x), он соответствовал бы данному типу x и достиг бы более узкого, чем объявленный тип (Bool -> Int) для функции z. И еще раз пожаловаться на жесткий тип переменной.

Фактически вы объявили тип (Num t) => Bool -> t -> (t1 -> t) -> t, но на самом деле это (Num t) => Bool -> t -> (t -> t) -> t. Оно это другой тип.

2