| foo :: (forall s. ST s a) -> a
| foo st = ($) runST st
This is a motivating example for type inference that can deal with
impredicative types. Consider the type of ($):
($) :: forall p q. (p->q) -> p -> q
In the example we need to instantiate 'p' with (forall s. ST s a), and that's
what impredicative polymorphism means: instantiating a type variable with a
polymorphic type.
Sadly, I know of no system of reasonable complexity that can typecheck 'foo'
unaided. There are plenty of complicated systems, and I have been a co-author
on papers on at least two, but they are all Too Jolly Complicated to live in
GHC. We did have an implementation of boxy types, but I took it out when
implementing the new typechecker. Nobody understood it.
However, people so often write
runST $ do ...
that in GHC 7 I implemented a special typing rule, just for infix uses of ($).
Just think of
(f $ x) as a new syntactic form, with the obvious typing rule, and away you go.
It's very ad hoc, because it's absolutely specific to ($), and I'll take it out
if you all hate it, but it's in GHC 7 for now.
Anyway, that's why you encountered the puzzling behaviour you describe below.
Simon
| -----Original Message-----
| From: Bas van Dijk [mailto:[email protected]]
| Sent: 30 October 2010 21:14
| To: [email protected]
| Cc: Simon Peyton-Jones
| Subject: Re: Type error in GHC-7 but not in GHC-6.12.3
|
| On Sat, Oct 30, 2010 at 1:57 AM, Bas van Dijk <[email protected]> wrote:
| > I could isolate it a bit more if you want.
|
| And so I did. The following is another instance of the problem I'm
| having but set in a more familiar setting:
|
| {-# LANGUAGE RankNTypes #-}
|
| import Control.Monad.ST
|
| foo :: (forall s. ST s a) -> a
| foo st = ($) runST st
|
| Couldn't match expected type `forall s. ST s a'
| with actual type `ST s a'
| In the second argument of `($)', namely `st'
|
| Note that: 'foo st = runST st' type checks as expected.
|
| Surprisingly 'foo st = runST $ st' also type checks!
|
| I find the latter surprising because according to the report[1]: e1 op
| e2 = (op) e1 e2. So either both should type check or both should fail.
|
| I guess that a RULE somewhere eliminates the ($) before the
| type-checker kicks in. I do find that a little strange because I
| thought RULES where applied after type checking.
|
| Regards,
|
| Bas
|
| [1] http://www.haskell.org/onlinereport/exps.html#operators
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
