Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Simon Peyton-Jones <simonpj <at> microsoft.com>
Subject: RE: Type error in GHC-7 but not in GHC-6.12.3
Newsgroups: gmane.comp.lang.haskell.glasgow.user
Date: Monday 1st November 2010 09:14:30 UTC (over 7 years ago)
| 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 
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
 
CD: 3ms