[Haskell-cafe] Type inference
brianh at metamilk.com
Thu Feb 9 00:50:38 EST 2006
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?
>> 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
>> 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
>> 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
> 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)
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.
More information about the Haskell-Cafe