[Haskell-cafe] Re: Aren't type system extensions fun? [Further
analysis]
Roberto Zunino
zunino at di.unipi.it
Wed May 28 06:58:42 EDT 2008
Andrew Coppin wrote:
> (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.
When you type some expression such as
\x -> x
you have to choose among an infinite number of valid types for it:
Int -> Int
Char -> Char
forall a . a -> a
forall a b . (a,b) -> (a,b)
...
Yet the type inference is smart enough to choose the "best" one:
forall a. a -> a
because this is the "most general" type.
Alas, for code like yours:
foo = \f -> (f 'J', f True)
there are infinite valid types too:
(forall a. a -> Int) -> (Int, Int)
(forall a. a -> Char)-> (Char, Char)
(forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool))
...
and it is much less clear if a "best", most general type exists at all.
You might have a preference to type it so that
foo :: (forall a . a->a) -> (Char,Bool)
foo id ==> ('J',True) :: (Char,Bool)
but one could also require the following, similarly reasonable code to work:
foo :: (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool))
foo (\y -> (y,y)) ==> (('J','J'),(True,True))
:: ((Char,Char),(Bool,Bool))
And devising a type inference system allowing both seems to be quite
hard. Requiring a type annotation for these not-so-common code snippets
seems to be a fair compromise, at least to me.
Regards,
Zun.
More information about the Haskell-Cafe
mailing list