rank 2-polymorphism and type checking

Simon Peyton-Jones simonpj@microsoft.com
Wed, 24 Oct 2001 01:08:27 -0700


Here's the story

* GHC understands only rank-2 types; your type is rank 3

* The reason for this is that type inference for higher-rank types is
tricky.
   GHC just squeezes through the door with rank-2 types by using a neat
   hack, but the hack just doesn't cope with higher ranks at all.

* GHC 4.08 didn't *check* that the type is rank-2, whereas ghc 5.02
does.
  So all versions of your program will be rejected by GHC now, before
  it ever gets to type checking.

* It's true that your test' *does* typecheck in GHC 4.08, but it's a
coincidence!
  Certain very special programs will work even with higher rank types,
but
   its jolly hard to explain which, so GHC 5 chucks them all out.

* Nevertheless your program makes perfect sense. I believe that the
Right
  Thing to do is to adopt Odersky/Laufer's idea of "Putting Type
Annotations
   To Work" (POPL 96).  They show how to typecheck arbitrarily high rank
   type provided there are enough type annotations, and Mark Shields has
   recently explained it all to me.  But implementing this would be real
work.

So I'm interested to know: if GHC allowed arbitrarily-ranked types, who
would use them?

Simon



| -----Original Message-----
| From: Janis Voigtlaender [mailto:voigt@orchid.inf.tu-dresden.de]=20
| Sent: 24 October 2001 08:00
| To: haskell@haskell.org
| Subject: Re: rank 2-polymorphism and type checking
|=20
|=20
| Iavor S. Diatchki writes:=20
|=20
| > > > test :: (forall t . (forall a . t a) -> t b) -> b -> b
| > i am not an expert on this, but isnt this rank 3?
|=20
| Might be. Does this mean I cannot write it in Haskell? But, with=20
|=20
|  data T a =3D C
|=20
| I can write:
|=20
|  test' :: (forall t . (forall a . t a) -> t b) -> b -> b
|  test' g x =3D case g C of C -> x
|=20
| Here, the type checker finds out on its own that t is=20
| instantiated to T. Still,=20
| why are the annotations in the following code not enough to=20
| let it also accept=20
| the definition of "test" (see my earlier message),=20
| respectively how can I tell=20
| it that t should be instantiated to t c =3D forall d . (c->d)=20
| -> d -> d ?
|=20
|  test :: (forall t . (forall a . t a) -> t b) -> b -> b
|  test g x =3D (g           :: (forall a . (forall d . (a->d) ->=20
| d -> d)) ->=20
| (forall e . (b->e) -> e -> e))
|             ((\f y -> y) :: (forall a . (forall d . (a->d) ->=20
| d -> d)))
|             (id          :: (b -> b))=20
|             (x           :: b)
|=20
|=20
| --
| Janis Voigtlaender
| http://wwwtcs.inf.tu-dresden.de/~voigt/
| mailto:voigt@tcs.inf.tu-dresden.de
|=20
|=20
| _______________________________________________
| Haskell mailing list
| Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
|=20