[Haskell-cafe] Vanishing polymorphism

[Tom Schrijvers]

>
> To cut a long story short, could someone explain why:
>
>> :t negate
> negate :: forall a. (Num a) => a -> a
>
>> :t let f (fn :: forall a . Num a => a -> a) r s = (fn r, fn s) in f negate
>     let f (fn :: forall a . Num a => a -> a) r s = (fn r, fn s) in f negate
>        :: forall r s. (Num r, Num s) => r -> s -> (r, s)
>
> but
>
>> :t let f r s = (return negate) >>= (\fn -> return (fn r, fn s)) in f
>     let f r s = (return negate) >>= (\fn -> return (fn r, fn s)) in f
>        :: forall a (m :: * -> *). (Num a, Monad m) => a -> a -> m (a, a)
>
> and
>
>> :t let f r s = (return negate) >>= (\(fn::forall n . (Num n) => n -> n) -> return (fn r, fn s)) in f
>
> <interactive>:1:35:
>    Couldn't match expected type `a -> a'
>           against inferred type `forall n. (Num n) => n -> n'
>    In the pattern: fn :: forall n. (Num n) => n -> n
>    In a lambda abstraction:
>        \ (fn :: forall n. (Num n) => n -> n) -> return (fn r, fn s)
>    In the second argument of `(>>=)', namely
>        `(\ (fn :: forall n. (Num n) => n -> n) -> return (fn r, fn s))'
>
> I.e. why does the polymorphism get destroyed?

Unless annotated otherwise, functions destroy the polymorphism of their 
arguments.

In your first example f's argument is annotated to be 
polymorphic, hence you can call it with two different types.

In your second example, the lambda abstraction does not declare it expects 
a polymorphic argument. So you get a monomorhpic one. Neither does return 
or >>=. So that all works fine.

In your third example, return destroys the polymorphism of negate. becomes 
monomorphic for some a, the a -> a without forall. >>= is happy with the 
monomorphism. Then it is received by the lambda abstraction that expects a 
polymorphic type and causes the error.

You can read more about this in the paper:
Practical type inference for arbitrary-rank types
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields
http://research.microsoft.com/~simonpj/papers/higher-rank/index.htm

Basically, it comes down to the fact that preserving polymorphism is too 
hard for type inference, unless you the prorgrammer provide 
sufficient declarations for it.

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be