Error when ($) is used, but no error without - Glasgow-haskell-users - Haskell.org

newer
"A Language Based Approach to...

Error when ($) is used, but no error without

older
The 2006 GHC Hackathon

Robin Bate Boerop

27 Apr 2006 27 Apr '06

4:01 a.m.

This code compiles properly (with -fglasgow-exts on GHC 6.4.1): class CC a type C x = CC a => a x f, g :: C a -> Int f _ = 3 g x = f x But, this code: class CC a type C x = CC a => a x f, g :: C a -> Int f _ = 3 g x = f $ x -- the only change gives this error: Inferred type is less polymorphic than expected Quantified type variable `a' escapes Expected type: a a1 -> b Inferred type: C a1 -> Int In the first argument of `($)', namely `f' In the definition of `g': g x = f $ x What's going on here? -- Robin Bate Boerop

Reply

Sign in to reply online Use email software

Show replies by date

Brian Hulley

27 Apr 27 Apr

4:22 a.m.

Robin Bate Boerop wrote:

This code compiles properly (with -fglasgow-exts on GHC 6.4.1):

class CC a type C x = CC a => a x f, g :: C a -> Int f _ = 3 g x = f x

But, this code:

class CC a type C x = CC a => a x f, g :: C a -> Int f _ = 3 g x = f $ x -- the only change

gives this error:

Inferred type is less polymorphic than expected Quantified type variable `a' escapes Expected type: a a1 -> b Inferred type: C a1 -> Int In the first argument of `($)', namely `f' In the definition of `g': g x = f $ x

What's going on here?

I think the type declaration is actually equivalent to: type C x = forall a. CC a => a x so that you are declaring: f,g :: (forall a. CC a => a Int) -> Int -- not allowed instead of: f,g :: forall a. (CC a => a Int ->Int)

Reply

Sign in to reply online Use email software

Brian Hulley

4:28 a.m.

Brian Hulley wrote:

f,g :: (forall a. CC a => a Int) -> Int -- not allowed

delete the "not allowed" comment ;-) It's not so simple as I'd thought so I'd be interested to know the reason for $ making a difference too. Regards, Brian.

Reply

Sign in to reply online Use email software

Brian Hulley

5:41 a.m.

Brian Hulley wrote:

Brian Hulley wrote:

...
f,g :: (forall a. CC a => a Int) -> Int -- not allowed

delete the "not allowed" comment ;-) It's not so simple as I'd thought so I'd be interested to know the reason for $ making a difference too.

Actually I must undelete my "not allowed" comment above: you are trying to use existential types which are not supported in Haskell yet. You can simulate an existential by wrapping it in a single constructor data type eg: data Foo a = forall b. CC b => Foo (b a) Rewriting your example to use this simulation of existentials, everything works: class CC b data Foo a = forall b. CC b => Foo (b a) f :: Foo a -> Int f _ = 3 data A1 c = A1 c data A2 c = A2 c instance CC A1 instance CC A2 p = f (Foo (A1 3)) q = f (Foo (A2 3)) g x = f $ x The reason it works is that the Foo constructor keeps track of which particular 'b' has been used for any particular 'Foo a', so that class methods of the correct 'b' can be used inside the body of 'f'. Regards, Brian.

Reply

Sign in to reply online Use email software

Niklas Broberg

6:31 a.m.

On 4/27/06, Robin Bate Boerop wrote:

But, this code:

class CC a type C x = CC a => a x f, g :: C a -> Int f _ = 3 g x = f $ x -- the only change

The problem is exactly the use of $. $ is an operator, not a built-in language construct, and it has type (a -> b) -> a -> b. No forall's in there, so you cannot give it a function argument that is existentially quantified. Lots of people have been bitten by this when using the magic runST with type "forall a. (forall s. ST s a) -> a". Use parentheses when you have existentially quantified values and everything should be just fine. :-) /Niklas

gives this error:

Inferred type is less polymorphic than expected Quantified type variable `a' escapes Expected type: a a1 -> b Inferred type: C a1 -> Int In the first argument of `($)', namely `f' In the definition of `g': g x = f $ x

What's going on here?

-- Robin Bate Boerop

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply

Sign in to reply online Use email software

Brian Hulley

6:56 a.m.

Niklas Broberg wrote:

On 4/27/06, Robin Bate Boerop wrote:

...
But, this code:

class CC a type C x = CC a => a x f, g :: C a -> Int f _ = 3 g x = f $ x -- the only change

The problem is exactly the use of $. $ is an operator, not a built-in language construct, and it has type (a -> b) -> a -> b. No forall's in there, so you cannot give it a function argument that is existentially quantified. Lots of people have been bitten by this when using the magic runST with type "forall a. (forall s. ST s a) -> a". Use parentheses when you have existentially quantified values and everything should be just fine. :-)

Just to point out that in this case the problem is even more subtle, because C x is an existential type and therefore is not supported at all in Haskell at present. You cannot even apply 'f' to anything. It is made more confusing by the fact that the type checker appears to accept g x = f x. However this is a red herring, because you can't actually apply 'f' to anything in practice eg f (A1 3) where A1 is an instance of CC, would give an error also. In contrast, (forall s. ST s a) is not a true existential, since we are here just simulating an existential by making use of the ST constructor to store the info about what 's' was used so that it can be recovered by pattern matching. The previous example I posted *does* work with $. Regards, Brian.

Reply

Sign in to reply online Use email software

Brian Hulley

7:18 a.m.

Brian Hulley wrote:

In contrast, (forall s. ST s a) is not a true existential, since we are here just simulating an existential by making use of the ST constructor to store the info about what 's' was used so that it can be recovered by pattern matching.

Sorry the above paragraph is wrong ;-) (But see my previous post for how to simulate existentials by a data type (to hide the forall) and use them with $ if this is what you wanted to do) Regards, Brian.

Reply

Sign in to reply online Use email software

Bulat Ziganshin

10:04 a.m.

Hello Robin, Thursday, April 27, 2006, 8:01:16 AM, you wrote:

g x = f $ x -- the only change

gives this error:

Inferred type is less polymorphic than expected Quantified type variable `a' escapes Expected type: a a1 -> b Inferred type: C a1 -> Int In the first argument of `($)', namely `f' In the definition of `g': g x = f $ x

What's going on here?

may be, because '$' can't work with rank-2 types (at least error message is the same as i got when tried to use "runST $ ..."). i asked similar question some time ago, below are the answers (you can find them on pipermail): Bulat Ziganshin wrote: the following code can't go through typechecking

import Control.Monad.ST import Data.Array.ST main = print $ runST $ do arr <- newArray (1,10) 127 a <- readArray arr 1 writeArray arr 1 216 b <- readArray arr 1 return (a,b)

Indeed. The short answer: use runST (long expression) rather than runST $ long expression when it comes to higher-ranked functions such as runST. A longer answer: http://www.haskell.org/pipermail/haskell-cafe/2004-December/008062.html

let me know what i need to read to fix it myself MLF (see Daan Leijen, A. Loeh, `Qualified types for MLF', ICFP05)

Bulat Ziganshin wrote: ... for the same reason as this one doesn't get through: import Control.Monad.ST import Data.Array.ST main = print $ runST $ do return () ... but this one does: import Control.Monad.ST import Data.Array.ST main = print $ runST ( do return ()) it's all about rank-2 types; see SPJ's et al. paper on type inference for these types. However, I guess that the jury is still out, say this specific rank-2 behavior may be revised (and I also hope so). HTH Ralf

-----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe- bounces@haskell.org] On Behalf Of Bulat Ziganshin Sent: Tuesday, January 03, 2006 2:28 AM To: haskell-cafe@haskell.org Subject: [Haskell-cafe] ST monad

Hello

the following code can't go through typechecking. can anyone help me to fix it or, better, let me know what i need to read to fix it myself? :)

import Control.Monad.ST import Data.Array.ST main = print $ runST $ do arr <- newArray (1,10) 127 a <- readArray arr 1 writeArray arr 1 216 b <- readArray arr 1 return (a,b)

PS: error message is

b.hs:4:15: Inferred type is less polymorphic than expected Quantified type variable `s' escapes Expected type: ST s a -> b Inferred type: (forall s1. ST s1 a) -> a In the first argument of `($)', namely `runST' In the second argument of `($)', namely `runST $ (do arr <- newArray (1, 10) 127 a <- readArray arr 1 writeArray arr 1 216 b <- readArray arr 1 return (a, b))'

-- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

Reply

Sign in to reply online Use email software

7012

Age (days ago)

7012

Last active (days ago)

Download

7 comments

4 participants

tags

participants (4)

Brian Hulley
Bulat Ziganshin
Niklas Broberg
Robin Bate Boerop