On Thu, Jul 16, 2009 at 12:40 PM, Andrew Coppin wrote: Robert Greayer wrote: f0 _ = (foo True, foo 'x') where foo = id is well-typed. Really? That actually works? How interesting... This suggests to me that
where-clauses also do strange things to the type system. You could think of it that way. You mentioned GADTs in your OP. Well, it
turns out GADTs often do not play nicely with where/let and it happens to
all be related. As I understand it, functions bind their parameters
monomorphically and let/where bind things polymorphically. And then we have
the misfeature known as the monomorphism restriction which adds special
cases. whereas f1 foo = (foo True, foo 'x') requires 'foo' to be polymorphic in its first argument. This does
require a higher rank type, which can't be inferred: You could type f1 as
f1 :: (forall a . a -> a) -> (Bool, Char) and apply it to 'id'. Or you could type it as something like:
f1 :: (forall a . a -> ()) -> ((),()) and apply it to 'const ()' ...all of which is beyond Haskell-98, which is what I am limiting myself to
at present. (Actually, even that is a lie. I don't have type-classes yet...) Congrats on the type inference engine you're writing. It's on my list of
things to do, and I was even reading up on TaPL a month or two back, but I
put it down and haven't picked it up again yet. I think writing one would
help flush out my understand of all this stuff.
Jason