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