rank 2-polymorphism and type checking

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


PS to my earlier message.  I am not at all certain that=20
the Odersky/Laufer thing would in fact solve Janis's problem.
You want not only a rank-3 type, but also higher-order unification,
since you want to instantiate 't' to
	\c. forall d . (c->d) -> d -> d=20

That may just be too hard. But I'm out of my depth here.=20
Maybe a types expert can help.

Simon

| -----Original Message-----
| From: Simon Peyton-Jones [mailto:simonpj@microsoft.com]=20
| Sent: 24 October 2001 09:08
| To: Janis Voigtlaender; haskell@haskell.org
| Subject: RE: rank 2-polymorphism and type checking
|=20
|=20
| Here's the story
|=20
| * GHC understands only rank-2 types; your type is rank 3
|=20
| * The reason for this is that type inference for higher-rank=20
| types is tricky.
|    GHC just squeezes through the door with rank-2 types by=20
| using a neat
|    hack, but the hack just doesn't cope with higher ranks at all.
|=20
| * GHC 4.08 didn't *check* that the type is rank-2, whereas=20
| ghc 5.02 does.
|   So all versions of your program will be rejected by GHC now, before
|   it ever gets to type checking.
|=20
| * It's true that your test' *does* typecheck in GHC 4.08, but=20
| it's a coincidence!
|   Certain very special programs will work even with higher=20
| rank types, but
|    its jolly hard to explain which, so GHC 5 chucks them all out.
|=20
| * Nevertheless your program makes perfect sense. I believe=20
| that the Right
|   Thing to do is to adopt Odersky/Laufer's idea of "Putting=20
| Type Annotations
|    To Work" (POPL 96).  They show how to typecheck=20
| arbitrarily high rank
|    type provided there are enough type annotations, and Mark=20
| Shields has
|    recently explained it all to me.  But implementing this=20
| would be real work.
|=20
| So I'm interested to know: if GHC allowed arbitrarily-ranked=20
| types, who would use them?
|=20
| Simon
|=20
|=20
|=20
| | -----Original Message-----
| | From: Janis Voigtlaender [mailto:voigt@orchid.inf.tu-dresden.de]
| | 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
| | > > > 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
| |  data T a =3D C
| |=20
| | I can write:
| |=20
| |  test' :: (forall t . (forall a . t a) -> t b) -> b -> b =20
| test' g x =3D=20
| | case g C of C -> x
| |=20
| | Here, the type checker finds out on its own that t is
| | 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)) ->
| | (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
|=20
| _______________________________________________
| Haskell mailing list
| Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
|=20