Введите тайны. Почему этот код компилируется?

Ответ 1

В вашем втором примере h также имеет полиморфный тип. Таким образом, тип, в котором используется +, не является двусмысленным; он еще не выбран.

Контекст, в котором используется h, определит, какой тип + выбран (и различные сайты использования могут делать разные варианты). Пользователь h может попросить его указать любой тип RealFloat, который им нравится; f и g также могут предоставлять любой тип RealFloat, поэтому h будет просто запрашивать у них именно тот тип, который запрашивает его пользователь.

Ответ 2

С h = f < g :: Bool тип Bool не содержит полиморфную переменную a. Чтобы фактически вычислить результат Bool, необходимо создать экземпляр a, и полученное значение Bool может зависеть от выбора a (через экземпляр RealFloat), поэтому вместо произвольного выбора GHC отказывается компилировать.

С h = f + g параметр a находится в типе результата, поэтому нет никакой двусмысленности. Выбор для a еще не сделан, мы все еще можем создать a по своему усмотрению (или, точнее, мы обобщили тип f + g).

Ответ 3

Чтобы точно понять значение полиморфизма, мне удобно думать о функциональных языках с явными аргументами типа - теоретическими, такими как System F или real-world, такими как Agda, Idris, Coq и т.д.

В этих языках типы передаются как аргументы функции, как обычно. Если мы имеем полиморфную функцию

f :: forall a. T a

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

f Int :: T Int
f Char :: T Char
f String :: T String
...

Обратите внимание, как a в результирующем типе получает экземпляр аргумента типа.

Добавляя ограничения типа typeclass, мы имеем, что

f :: RealFloat a => a
f = 1.0

можно рассматривать как функцию, ожидающую: 1) аргумент типа a, 2) доказательство того, что выбранный тип является RealFloat (например, словарный словарь). Когда это предусмотрено, результат выбранного типа a будет возвращен. Более педантичное определение может быть

f :: forall a. RealFloat a => a
f = \\a -> \\proof ->  ... -- use proof to generate 1.0 :: a

где \\ используется как лямбда уровня уровня для дополнительных аргументов, описанных ранее. Тогда вызов мог бы быть следующим:

-- pseudo syntax
f Double double_is_a_RealFloat_proof

который вернет 1.0 :: Double.

Теперь, что произойдет, если мы напишем опубликованный код?

h :: RealFloat a => a
h = f + g

Итак, теперь f и g ожидают типы аргументов, а также h, поскольку все три являются полиморфными значениями. Во время вывода типа компилятор добавляет несколько дополнительных аргументов следующим образом:

h :: forall a. RealFloat a => a
h = \\a -> \\proof -> (f a proof) + (g a proof)

(технически, даже +, будучи полиморфным, имеет дополнительные аргументы, но пусть это под ковриком для удобства чтения...)

Обратите внимание, что теперь ясно, какой тип f должен произвести: it a, тот же тип, который создается h. Другими словами, h запрашивает у своего вызывающего абонента желаемый тип и пересылает один и тот же тип в f. То же самое для g.

Для сравнения, в

h :: Bool
h = f < g

нет полиморфизма в h, но f и g по-прежнему являются полиморфными. Во время вывода типа компилятор достигает

h = (f a? proof?) < (g a? proof?)

и должен изобретать a? и proof? из воздуха, так как h не просит их вызывающего абонента. Отсюда ошибка неоднозначности.

Наконец, обратите внимание, что можно видеть дополнительные аргументы типа, которые добавляются GHC во время вывода типа. Для этого достаточно выгрузить промежуточный язык ядра GHC, например. с флагом -ddump-simpl GHC. В GHC 8.x, который еще не выпущен, слухи говорят, что нам даже будет разрешено указывать явные аргументы типа в нашем коде, когда мы захотим, и пусть компилятор выводит их как обычно в противном случае. Это звучит весело!