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.

Brian Hulley wrote:

Brian Hulley wrote:

...

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

The above is wrong - there is no way to quantify m properly. This must be why intersection types need to be written with "&" after all....

What am I saying! It's right after all, and might be better than the & syntax because it makes the dependency clearer (assuming you can't write a function that is both Int->String and Float->Int)

On 09/02/06, Brian Hulley wrote:

Brian Hulley wrote:

...

Brian Hulley wrote:

...

Brian Hulley wrote:

...

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

The above is wrong - there is no way to quantify m properly. This must be why intersection types need to be written with "&" after all....

What am I saying! It's right after all, and might be better than the & syntax because it makes the dependency clearer (assuming you can't write a function that is both Int->String and Float->Int)

Last correction!

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

Sorry for all this confusion.

Of course this type doesn't work on your original example, since (,) is a type constructor with two parameters, not one, but this type signature does actually work just fine in GHC. --- data Pair x = Pair x x deriving Show data Id x = Id x deriving Show f :: forall m c d. (forall a. a -> m a) -> c -> d -> (m c, m d) f g x y = (g x, g y) --- *Main> f (\x -> Pair x x) 3 "hello" (Pair 3 3,Pair "hello" "hello") *Main> f (\x -> Id x) 3 "hello" (Id 3,Id "hello") --- - Cale

Brian Hulley wrote:

Fred Hosch wrote:

...

Is type inferencing in Haskell essentially the same as in SML?

The most significant difference certainly is that type inference has been beefed up with type classes in Haskell, which are quite a powerful mechanism refining Hindley/Milner inference. Besides that, Haskell allows some additional programs for which types can /not/ be inferred (e.g. the examples Brian was giving), while SML does not.

SML also has a complicated thing called the "value restriction" because it allows mutable references to be altered via side effects. Because Haskell has no side effects, there is no need for a value restriction.

Although there is no "need" for it, Haskell still has it, in minor variation. It is commonly known as "The Dreaded Monomorphism Restriction" ;). - Andreas -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB