[Haskell-cafe] A voyage of undiscovery

Jason Dagit dagit at codersbase.com
Thu Jul 16 15:50:06 EDT 2009


On Thu, Jul 16, 2009 at 12:40 PM, Andrew Coppin <andrewcoppin at btinternet.com
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090716/597c34ae/attachment.html


More information about the Haskell-Cafe mailing list