How does haskell determine the order of type variables in implicit foralls?

  • A+
Category:Languages

So I just recently learned about and started using TypeApplications, and was wondering how we can generally know what type variables we're assigning. The documentation on TypeApplications I found mentions:

What order is used to instantiate the type variables?

Left-to-right order of the type variables appearing in the foralls. This is the most logical order that occurs when the instantiation is done at the type-variable level. Nested foralls work slightly differently, but at a single forall location with multiple variables, left-to-right order takes place. (See below for nested foralls).

However I haven't found mention of how order of type variables in implicit foralls is determined. I tried looking at different examples with -fprint-explicit-foralls to see if there was a simple pattern, but I'm getting different results in different versions of ghci. :/

In ghci version 8.0.2, I get:

> :t (,,) (,,) :: forall {c} {b} {a}. a -> b -> c -> (a, b, c) 

while in ghci version 8.4.3, I get:

> :t (,,) (,,) :: forall {a} {b} {c}. a -> b -> c -> (a, b, c) 

Then again, maybe that's simply a bug in how foralls were being printed in 8.0.2, because otherwise type applications seem to be done right-to-left with the variables of forall, contrary to what the documentation says:

> :t (,,) @Bool (,,) @Bool :: forall {c} {b}. Bool -> b -> c -> (Bool, b, c) 

So are type variables put in implicit foralls always in the order they appear first left-to-right in the type body (including the constraints)?

 


TL;DR: When interested in TypeApplication, use :type +v.

Don't use :type

Using :type is misleading here. :type infers the type of a whole expression. So when you write :t (,), the type checker looks at

(,) :: forall a b. a -> b -> (a, b) 

and instantiates all the forall’s with fresh type variables

(,) :: a1 -> b1 -> (a1, b1) 

which is necessary if you would apply (,). Alas, you don’t, so type inference is almost done, and it generalizes over all free variables, and you get, for example,

(,) :: forall {b} {a}. a -> b -> (a, b) 

This step makes no guarantees over the order of the free variable, and the compiler is free to change.

Also note that it writes forall {a} instead of forall a, which means that you can’t use visible type application here.

Use :type +v

But of course you can use (,) @Bool – but here the type-checker treats the first expression differently and does not do this instantiation/generalization step.

And you can get this behaviour in GHCi as well – pass +v to :type:

:type +v (,) (,) :: forall a b. a -> b -> (a, b) :type +v (,) @Bool (,) @Bool :: forall b. Bool -> b -> (Bool, b) 

Look, no {…} around type variables!

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: