RE: higher-order typing errors
Because GHC does not allow you to instantiate a polymorphic type
variable with a polymorphic type. For example, you can have
Maybe Int
Maybe (Int - Int)
but not
Maybe (forall a. a-a)
The Maybe type is defined thus
data Maybe b = Nothing | Just b
so the type (Maybe (forall a. a-a)) would instantiate 'b' with (forall
a. a-a), and GHC just doesn't allow that.
In your program, its the tuple type
data (,) a b = (,) a b
Admittedly the error message is not especially helpful.
Why does GHC have this restriction? Because type inference is much, much
harder without it. There may be a way to lift it, but I don't yet know
what it is.
To get around it, define your own data type:
data MyPr = MyPr (forall a.a-a) (forall a.a-a)
swap1 :: MyPr - MyPr
Simon
| -Original Message-
| From: Dean Herington [mailto:[EMAIL PROTECTED]]
| Sent: 22 January 2003 23:03
| To: [EMAIL PROTECTED]
| Subject: higher-order typing errors
|
| I don't understand why GHC (I was using 5.04.2) should reject these
two
| programs.
|
|
|
| {-# OPTIONS -fglasgow-exts #-}
|
| swap1 :: (forall a. a - a, forall a. a - a - a)
| - (forall a. a - a - a, forall a. a - a)
| swap1 (a, b) = (b, a)
|
| yields:
|
| Bug2.hs:3: parse error on input `,'
|
|
|
| {-# OPTIONS -fglasgow-exts #-}
|
| swap2 :: ((forall a. a - a), (forall a. a - a - a))
| - ((forall a. a - a - a), (forall a. a - a))
| swap2 (a, b) = (b, a)
|
| yields:
|
| Bug2.hs:3:
| Illegal polymorphic type: forall a. a - a
| In the type: (forall a. a - a, forall a. a - a - a)
| - (forall a. a - a - a, forall a. a - a)
| While checking the type signature for `swap2'
|
|
| ___
| Glasgow-haskell-bugs mailing list
| [EMAIL PROTECTED]
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
___
Glasgow-haskell-bugs mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: higher-order typing errors
Hi!
On Thu, Jan 23, 2003 at 10:28:13AM -, Simon Peyton-Jones wrote:
To get around it, define your own data type:
data MyPr = MyPr (forall a.a-a) (forall a.a-a)
swap1 :: MyPr - MyPr
I played a bit with using highed order polymorphism for this problem,
and have encountered compile errors I don't understand.
The first version doesn't compile - the error is:
Type synonym `F3' should have 1 argument, but has been given 0
In the type: Pair F3 F2
While checking the type signature for `p'
{-# OPTIONS -fglasgow-exts #-}
module T where
type F3 a = a - a - a
type F2 a = a - a
data Pair c1 c2 = Pair (forall a. c1 a) (forall b. c2 b)
swap :: Pair c1 c2 - Pair c2 c1
swap (Pair f g) = Pair g f
f2 :: F2 a
f2 = id
f3 :: F3 a
f3 = const
p :: Pair F3 F2
p = Pair f3 f2
The other version uses newtype instead of type synonyms for F2 and F3.
This one compiles without problems.
{-# OPTIONS -fglasgow-exts #-}
module T2 where
newtype F3 a = F3 (a - a - a)
newtype F2 a = F2 (a - a)
data Pair c1 c2 = Pair (forall a. c1 a) (forall b. c2 b)
swap :: Pair c1 c2 - Pair c2 c1
swap (Pair f g) = Pair g f
f2 :: F2 a
f2 = F2 id
f3 :: F3 a
f3 = F3 const
p :: Pair F3 F2
p = Pair f3 f2
There is probably some restriction I don't know about or haven't
recognized in this particular case. I hope you will enlighten me.
Simon
Best regards,
Tom
--
.signature: Too many levels of symbolic links
___
Glasgow-haskell-bugs mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
RE: higher-order typing errors
| The first version doesn't compile - the error is:
| Type synonym `F3' should have 1 argument, but has been given 0
| In the type: Pair F3 F2
| While checking the type signature for `p'
Type synonyms in Haskell must be saturated (i.e. given all their
argments).
GHC lifts this restriction slightly; see
http://haskell.cs.yale.edu/ghc/docs/latest/html/users_guide/type-extensi
ons.html#TYPE-SYNONYMS
in the user manual. (Which I hope you have read.)
| The other version uses newtype instead of type synonyms for F2 and F3.
| This one compiles without problems.
That's right. Newtypes don't need to be saturated. Reason: with
newtypes the type (F3 a) and the representation type (a-a-a) are
distinct, with explicit coercions between them. This makes type
inference work right. We can't do this for type synonyms because that'd
need higher order unification, and loss of principal types.
Simon
|
| {-# OPTIONS -fglasgow-exts #-}
|
| module T2 where
|
| newtype F3 a = F3 (a - a - a)
| newtype F2 a = F2 (a - a)
|
| data Pair c1 c2 = Pair (forall a. c1 a) (forall b. c2 b)
|
| swap :: Pair c1 c2 - Pair c2 c1
| swap (Pair f g) = Pair g f
|
| f2 :: F2 a
| f2 = F2 id
|
| f3 :: F3 a
| f3 = F3 const
|
| p :: Pair F3 F2
| p = Pair f3 f2
|
| There is probably some restriction I don't know about or haven't
| recognized in this particular case. I hope you will enlighten me.
|
| Simon
|
| Best regards,
| Tom
|
| --
| .signature: Too many levels of symbolic links
___
Glasgow-haskell-bugs mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
higher-order typing errors
I don't understand why GHC (I was using 5.04.2) should reject these two
programs.
{-# OPTIONS -fglasgow-exts #-}
swap1 :: (forall a. a - a, forall a. a - a - a)
- (forall a. a - a - a, forall a. a - a)
swap1 (a, b) = (b, a)
yields:
Bug2.hs:3: parse error on input `,'
{-# OPTIONS -fglasgow-exts #-}
swap2 :: ((forall a. a - a), (forall a. a - a - a))
- ((forall a. a - a - a), (forall a. a - a))
swap2 (a, b) = (b, a)
yields:
Bug2.hs:3:
Illegal polymorphic type: forall a. a - a
In the type: (forall a. a - a, forall a. a - a - a)
- (forall a. a - a - a, forall a. a - a)
While checking the type signature for `swap2'
___
Glasgow-haskell-bugs mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
