Re: [Haskell-cafe] Type inference

Cale Gibbard wrote:

On 08/02/06, Brian Hulley 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.