[Haskell-cafe] Type inference

[Brian Hulley]

Cale Gibbard wrote:
> On 08/02/06, Brian Hulley <brianh at metamilk.com> wrote:
>> Fred Hosch wrote:
>>> Is type inferencing in Haskell essentially the same as in SML?
>>> Thanks.
>>
>> Well, that depends on what you mean by "essentially the same" ;-)
>>
>> Both languages are based on the same Hindley-Milner type inference
>> algorithm, so both suffer from the same problem that a function such
>> as
>>
>>        f g x y = (g x, g y)
>>
>> can't be given a very satisfactory type (ie there exist perfectly
>> good programs that will be rejected by both SML and Haskell due to
>> limitations inherent in the kinds (excuse the pun) of type system
>> that can be used with HM type inference)
>>
>> However, Haskell has a lot of advanced features that are bolted on
>> to this foundation, which SML doesn't. One such feature is arbitrary
>> rank polymorphism, which allows you to use a function argument in
>> more than one way within a function, for example (compile with ghc
>> -fglasgow-exts):
>>
>>       h :: (forall a. a->a) -> b -> c -> (b,c)
>>       h g x y = (g x, g y)  -- the argument g is used polymorphically
>>
>> This function can't be written in SML. Note that although h is
>> similar to f, there would not exist a type for h if g could be an
>> arbitrary function ie a->d instead of a->a.
>
> The type forall a d. a -> d isn't terribly useful, since there just
> aren't many functions of that type. You can give a type signature
> like:
>
> f :: (forall a b. a -> b) -> c -> d -> (e,f)
> f g x y = (g x, g y)
>
> but good luck actually applying the function in a useful way :) The
> only thing you can reasonably pass as g (barring the existence of
> functions which completely break the type system) is bottom.
>
> So what is it that you're looking for here? I'm not sure I understand.

For example, you can't have:

            f g x y = (g x, g y)

           a = f (\x -> (x,x)) 3 "hello"     -- example 1

           b = f (\x -> x) 5 "bye"          -- example 2

because there is no way to express the relationship between the arguments 
x,y and the results g x, g y without fixing down the shape of g's result in 
the definition of f.

If Haskell used intersection types instead of system F (I hope I've got this 
right) then you could write:

          f :: (a->b & c->d) -> a -> c -> (b,d)

or

          f :: (forall a m. a -> m a) -> c -> d -> (m c, m d)

where the intention is that "m" would match (,) in example 1 and the 
identity type constructor (I in type I a=a) in example 2.

Regards, Brian.