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

Question

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

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,
интерпретировать)

test.hs:2:35:
    Не удалось сопоставить ожидаемый тип `a'с фактическим типом`Bool'
      "a" - это переменная жесткого типа, связанная
          сигнатура типа для f:: Bool -> Int -> (a -> Int) -> Int
          в test.hs:1:6
    Соответствующие привязки включают
      z:: a -> Int (связано с test.hs:2:7)
      f:: Bool -> Int -> (a -> Int) -> Int (привязано в test.hs:2:1)
    В первом аргументе `z', а именно`x'
    В первом аргументе `(+)', а именно`(z x)' Ошибка, загружены модули: нет.

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

Answer 1

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

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

Answer 2

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

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

Answer 3

Четное

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

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

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

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

Для выражения выше предполагаемый тип (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, Это другой тип.