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