CODEWITHSUNDEEP
haskell
haskellHQ
haskellHQ

Reputation: 1047

Type mysteries. Why does this code compile?

This code does not compile:

default ()

f :: RealFloat a => a
f = 1.0

g :: RealFloat a => a
g = 1.0

h :: Bool
h = f < g --Error. Ambiguous.

This is expected because it's ambiguous. The two possibilities are Float and Double and the compiler doesn't know which < to pick.

However, this code does compile:

default ()

f :: RealFloat a => a
f = 1.0

g :: RealFloat a => a
g = 1.0

h :: RealFloat a => a
h = f + g --Why does this compile?

Why? Why isn't Haskell confused here, in a similar manner as in the example above, about which + to pick (for Float or Double)?

Upvotes: 17

Views: 1050

Answers (3)

chi
chi

Reputation: 116139

To precisely understand the meaning of polymorphism, I find it convenient to think about functional languages with explicit type arguments -- either theoretical ones, such as System F, or real-world ones such as Agda, Idris, Coq, etc.

In these languages, types are passed as function arguments as values normally are. If we have a polymorphic function

f :: forall a. T a

this actually expects a type as a first argument, like this:

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

Note how the a in the resulting type gets instantiated to the type argument.

Adding typeclass constraints, we have that

f :: RealFloat a => a
f = 1.0

can be seen as a function expecting: 1) a type argument a, 2) a proof that the chosen type is a RealFloat (e.g. a typeclass dictionary). When this is provided, a result of the chosen type a will be returned. A more pedantic definition could be

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

where \\ is used as a type-level lambda, for the additional arguments described earlier. A call could then be as follows:

-- pseudo syntax
f Double double_is_a_RealFloat_proof

which will return 1.0 :: Double.

Now, what happens if we write the posted code?

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

Well, now f and g expect type arguments, as well as h, since all three are polymorphic values. During type inference, a few additional arguments are added by the compiler as follows:

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

(technically, even +, being polymorphic, has additional arguments, but let's put that under the rug for readability's sake...)

Note that now it is clear what type f should produce: it's a, the same type which is produced by h. In other words, h asks its caller which type is wanted, and forwards the same type to f. Ditto for g.

By comparison, in

h :: Bool
h = f < g

there's no polymorphism in h, but f and g are still polymorphic. During type inference the compiler reaches

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

and has to invent a? and proof? out of thin air, since h is not asking them to its caller. Hence the ambiguity error.

Finally, note that it is possible to see the additional type arguments which are added by GHC during type inference. To do that, it suffices to dump the GHC Core intermediate language, e.g. with the -ddump-simpl GHC flag. In GHC 8.x, which is not yet released, rumors say that we will be even allowed to specify explicit type arguments in our code when we want to, and let the compiler infer them as usual otherwise. It sounds fun!

Upvotes: 5

Andr&#225;s Kov&#225;cs
Andr&#225;s Kov&#225;cs

Reputation: 30113

With h = f < g :: Bool, the type Bool doesn't contain the polymorphic a variable. To actually compute the Bool result, the a needs to be instantiated, and the resulting Bool value can depend on the choice of a (through the RealFloat instance), so instead of making an arbitrary choice GHC refuses to compile.

With h = f + g, the a parameter is in the type of the result, therefore there is no ambiguity. The choice for a has not yet been made, we can still instantiate a as we like (or more precisely, we re-generalized the type of f + g).

Upvotes: 11

Ben
Ben

Reputation: 71400

In your second example h also has a polymorphic type. So the type at which + is used isn't ambiguous; it just hasn't been chosen yet.

The context where h is used will determine which type's + is chosen (and different use-sites can make different choices). The user of h can ask it to provide any RealFloat type they please; f and g can also provide any RealFloat type, so h will just ask them for exactly the type its user is asking for.

Upvotes: 24

Related Questions