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:[EMAIL PROTECTED]]
| Sent: 24 October 2001 09:08
| To: Janis Voigtlaender; [EMAIL PROTECTED]
| 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:[EMAIL PROTECTED]]
| | Sent: 24 October 2001 08:00
| | To: [EMAIL PROTECTED]
| | 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:[EMAIL PROTECTED]
| |
| |
| | _______________________________________________
| | Haskell mailing list
| | [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
| |
|
| _______________________________________________
| Haskell mailing list
| [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
|
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
