Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

Tags:

haskell

ghc

ghci

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)?

like image 399
JoL Avatar asked Oct 20 '18 03:10

JoL


1 Answers

TL;DR: Type variable order is determined by first left-to-right encounter. When in doubt, 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!

Where does this order come from?

The the GHC user's guide section on visible type application states:

If an identifier’s type signature does not include an explicit forall, the type variable arguments appear in the left-to-right order in which the variables appear in the type. So, foo :: Monad m => a b -> m (a c) will have its type variables ordered as m, a, b, c.

That this only applies to things that have an explicit type signature. There is no guaranteed order to variables in inferred types, but you also can't use expressions with inferred types with VisibleTypeApplication.

like image 180
Joachim Breitner Avatar answered Sep 20 '22 20:09

Joachim Breitner