Vanishing polymorphism

newer
built-in lists vs inductively...

older
Object Files Become...

Matthew Sackman

8 May 2007 8 May '07

9:10 p.m.

Hi, 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? Cheers, Matthew -- Matthew Sackman http://www.wellquite.org/

Show replies by date

David House

8 May 8 May

9:43 p.m.

On 08/05/07, Matthew Sackman wrote:

...

...
: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?

Here fn is bound by a lambda abstraction, and is therefore monomorphic. I can't find anything in the Report about that, but that is how it works. It might be how a H-M type system works in general, I'm not sure. -- -David House, dmhouse@gmail.com

Tom Schrijvers

9 May 9 May

7:30 a.m.

On Tue, 8 May 2007, David House wrote:

...

On 08/05/07, Matthew Sackman wrote:

...
...
: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?

Here fn is bound by a lambda abstraction, and is therefore monomorphic. I can't find anything in the Report about that,

This won't be in the Haskell 98 report. I have to enable -fglasgow-exts in GHCi to get this even parsed. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be

Matthew Sackman

8 May 8 May

9:58 p.m.

New subject: Re Vanishing polymorphism

Sorry, am subscribed with digest and haven't got David House's reply via email yet, hence the broken thread. It's not to do with lambdas though:

...

:t let f r s = let g (fn::forall n . (Num n) => n -> n) = return (fn r, fn s) in (return negate) >>= g in f

<interactive>:1:98: Couldn't match expected type `a -> a' against inferred type `forall n. (Num n) => n -> n' Expected type: (a -> a) -> m b Inferred type: (forall n2. (Num n2) => n2 -> n2) -> m1 (n, n1) In the second argument of `(>>=)', namely `g' In the expression: let g (fn :: forall n. (Num n) => n -> n) = return (fn r, fn s) in (return negate) >>= g ...unless we're talking about lambdas in the definitions of return and

...

...
= which would be quite worrying.

Matthew -- Matthew Sackman http://www.wellquite.org/

David House

9 May 9 May

3:52 p.m.

New subject: Re Vanishing polymorphism

On 08/05/07, Matthew Sackman wrote:

...

...
:t let f r s = let g (fn::forall n . (Num n) => n -> n) = return (fn r, fn s) in (return negate) >>= g in f

Ah, I may have been off the mark earlier. I think the problem is due to the fact that you can't pass higher-order polymorphic functions around. I.e., the following is a classic example of something people expect to work, but doesn't: runST $ ... runST is a rank-2 polymorphic function, and you're attempting to pass it as a parameter to the ($) function, which doesn't work. I think your problem is similar. Here's the module I used to investigate goings on: {-# OPTIONS_GHC -fglasgow-exts #-} import Data.Complex g :: (Num a, Num b, Monad m) => a -> b -> (forall n. Num n => n -> n) -> m (a, b) g r s fn = return (fn r, fn s) f :: Maybe (Int, Complex Float) f = return negate >>= g (4 :: Int) (1 :+ 2) You're attempting to pass the rank-2 polymorphic function "g (4 :: Int) (1 :+ 2)" as a parameter to (>>=), which doesn't work. General point: couldn't GHC's error reporting be improved at times like these? -- -David House, dmhouse@gmail.com

Jules Bean

10 May 10 May

6:26 a.m.

New subject: Re Vanishing polymorphism

David House wrote:

...

On 08/05/07, Matthew Sackman wrote:

...
...
:t let f r s = let g (fn::forall n . (Num n) => n -> n) = return (fn r, fn s) in (return negate) >>= g in f

Ah, I may have been off the mark earlier. I think the problem is due to the fact that you can't pass higher-order polymorphic functions around. I.e., the following is a classic example of something people expect to work, but doesn't:

runST $ ...

runST is a rank-2 polymorphic function, and you're attempting to pass it as a parameter to the ($) function, which doesn't work. I think your problem is similar. Here's the module I used to investigate goings on:

It's a bit more subtle than that, I think. You can pass rank-2 functions around, but type inference will not unify ordinarily polymorphic variables with rank-2 types. So ($) has the type (a -> b) -> a -> b ; but the implicit restriction here (and in all such haskell types) is that the 'a' and 'b' are rank-1. At least if you want automatic inference. I suspect that with explicit type annotations you can declare the precise rank-2 version of ($) that you want, and then it will work. Summary: If you want to pass a rank-2 function around, the function receiving it as a parameter has to have an explicitly annotated type. Jules

Tom Schrijvers

9 May 9 May

7:27 a.m.

...

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@cs.kuleuven.be

6634

Age (days ago)

6636

Last active (days ago)

List overview

Download

6 comments

4 participants

participants (4)

David House
Jules Bean
Matthew Sackman
Tom Schrijvers