[Haskell-cafe] Re: Aren't type system extensions fun? [Further
dons at galois.com
Tue May 27 14:26:35 EDT 2008
> Gleb Alexeyev wrote:
> >foo :: (forall a . a -> a) -> (Bool, String)
> >foo g = (g True, g "bzzt")
> So, after an entire day of boggling my mind over this, I have brought it
> down to one simple example:
> (id 'J', id True) -- Works perfectly.
> \f -> (f 'J', f True) -- Fails miserably.
> Both expressions are obviously perfectly type-safe, and yet the type
> checker stubbornly rejects the second example. Clearly this is a flaw in
> the type checker.
I'm sorry you are still confused, Andrew.
This is documented rather nicely in section 126.96.36.199 of
the GHC user's guide. In particularly, you'll want to not ethat
arbitrary rank type inference is undecidable, so GHC imposes a
simple rule requiring you to annotate those polymorphic parameters
of higher rank you want.
Read this carefully, and then read the references.
> Interestingly, if you throw in the undocumented "forall" keyword,
> everything magically works:
> (forall x. x -> x) -> (Char, Bool)
> Obviously, the syntax is fairly untidy. And the program is now not valid
> Haskell according to the written standard. And best of all, the compiler
> seems unable to deduce this type automatically either.
Please read the above link. In particular, pay attention to the word
"undecidable". Reading and comprehending Odersky and Laufer's paper, "Putting
type annotations to work", will explain precisely why you're butting
your head up against deciability.
More information about the Haskell-Cafe