[Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]

[Roberto Zunino]

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.