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/
On 08/05/07, Matthew Sackman <matthew@wellquite.org> 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
On Tue, 8 May 2007, David House wrote:
On 08/05/07, Matthew Sackman <matthew@wellquite.org> 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
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/
On 08/05/07, Matthew Sackman <matthew@wellquite.org> 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
David House wrote:
On 08/05/07, Matthew Sackman <matthew@wellquite.org> 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
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
participants (4)
-
David House -
Jules Bean -
Matthew Sackman -
Tom Schrijvers