Wednesday, October 15, 2008

Unordered multi-arity binders

Cool: GHC knows that "∀" doesn't care what order you bind its type variables:
{-# LANGUAGE RankNTypes, TypeOperators #-}

f1 :: ∀ a b . a → b → b
f1 x y = y

f2 :: ∀ b a . a → b → b
f2 x y = y

h :: (∀ a b . a → b → b) → c → d → d
h f x y = f x y

a = h f1
b = h f2
Think about what this means for implementing a type-checker: to match one ∀-type against another, you have to find the right permutation of bound type variables. (A naive approach requires searching through all n! permutations!) Presumably the actual implementation incrementally unifies the type variables as it recurs into the bodies of the ∀-types.

Does anyone know of a paper that describes this aspect of implementing higher-rank polymorphism?


Daniel Yokomizo said...
This comment has been removed by the author.
Daniel Yokomizo said...

Using de Bruijn indexes as type variables wouldn't solve this?

Dave Herman said...

Using de Bruijn indexes as type variables wouldn't solve this?

Nope-- try it! What do you pick for the index of each variable?

Unknown said...

One place to start might be (I don't know if it contains the answer, it has been a while since I read this paper...)

and maybe some of the citations.

Also, scanning section 12 of

some of the papers look promising.

Anonymous said...

It's easy. You just normalise the universal types as described in Daan Leijen's ICFP paper on HMF (ICFP 2008).

單中杰 said...

If I understand you correctly, this check is part of checking whether one type (scheme) is an instance of another. In your example, the type checker should try (successfully) to unify the ground term to(a,to(b,b)) with the non-ground term to(A,to(B,B)). In the more general setting of "Putting type annotations to work" (Section 5), Odersky and Läufer relate the problem of instantiation checking to unification under a mixed prefix.

Neel Krishnaswami said...

SPJ and a bunch of coauthors have a JFP paper about type inference (including higher-rank types) in GHC as of 2006, over here.

I dunno if they still do the same thing, since GHC's typechecker changes pretty often. :-)

steck said...

I haven't read the references mentioned in other comments, but
normalization sounds right to me.

One way to do this is to sort the binders according to the order of their first appearance in the type being quantified. Then you just check the two types for alpha-equivalence.

Douglas McClean said...

I was going to say exactly what Steck did. Is there a reason that can't work?