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

Question

Код

default() 
h :: Bool 
h = 1.0 == 1.0 --Error. Ambiguity. 

не компилируется. Это ожидается, потому что есть двусмысленность. Это может быть либо Float, либо Double, и Haskell не знает, какой из них мы хотим.

Но код

default() 
foo :: (Fractional a, Eq a) => a -> Bool 
foo x = x == 1.0 

успешно компилируется. Я не совсем понимаю, почему. Почему это не так неоднозначно?

У меня есть ощущение, что это потому, что всякий раз, когда мы называем foo, мы гарантированно выбрали конкретный тип вместо a, то есть, мы гарантированно закрепили a либо Float или Double (или наш пользовательский тип который имеет экземпляры как Fractional, так и Eq) во время компиляции, и поэтому нет никакой двусмысленности.

Но это просто чувство, и я не знаю, является ли оно на 100% точным.

Answer 1

Определение двусмысленности в этом контексте дается в Section 4.3.4 of Haskell Report:

Мы говорим, что выражение e имеет неоднозначный тип, если в его типе forall us. cx => t, есть тип переменной u в us, что происходит в cx, но не в t. Такие типы недействительны.

В foo :: (Fractional a, Eq a) => a -> Bool, нет такой переменной (потому что a происходит в a -> Bool). В 1.0 == 1.0 тип на самом деле (Fractional a, Eq a) => Bool, поэтому есть такая переменная.

причина такого рода двусмысленности является ошибка, потому что нет никакого способа для компилятора выбирать между различными конкретизации переменной a, и результат программы может зависеть от того, какой он выберет. В этом случае 1.0 == 1.0 всегда должен быть True для любого разумным экземпляром, но 1) компилятор этого не знает; 2) не все экземпляры являются разумными.

Answer 2

Вторая часть коды компилируется, потому что

foo :: (Fractional a, Eq a) => a -> Bool 
foo x = x == 1.0 

(==) :: Eq a => a -> a 

поэтому компилятор будет знать, что поплавок число буквального 1.0 :: Rational a => a имеет один и тот же тип с x, который имеет Eq экземпляр т.е. «смысл» == в этом функция детерминирована для каждого вызова.

В то время как в первой части кода, в буквальном смысле может быть любого типа (Rational a, Eq a) => a, так что «смысл» == неоднозначна, значение часов может быть истинным или ложным, зависит от типа буквальный, который не предоставляется.

Answer 3

Here'a другого концептуальный способ поставить его:

Оба случай имеет внутреннюю неоднозначность, но первый один тупик - нет никакой надежды на компилятор, чтобы вывести свой путь из-за двусмысленности.

Второй случай также неоднозначен, но двусмысленность открыта - тот, кто называет двусмысленный код, должен устранить двусмысленность или делегировать/пузырить его дальше в стек вызовов.

Это все, что нужно - полиморфизм контролируется двусмысленностью. Первый случай - неконтролируемая двусмысленность, поэтому это не полезно (т. Е. Связанное с полиморфизмом) двусмысленность. Поэтому он отклоняется до тех пор, пока он не будет аннотирован однозначно.