Cale Gibbard wrote:
On 08/02/06, Brian Hulley <[EMAIL PROTECTED]> 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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
