
I just can't see why the following code will not type check. I have scaled it down as much as possible: ------------------------------------- -- IO with an extra level annotation newtype IO' t a = MkIO' (IO a) -- levels data H data L -- Explicitly recursive continuation type data C t a = forall t2 . C (C t2 a -> IO t a) transition :: Bool -> IO tx () -> IO t () -> IO t () transition b c d = undefined s1 :: C t () -> IO H () s1 (C k) = trans (True) (k (C s1)) -- :: IO t () (s1 (C k)) -- :: IO H () -------------------------------------- The error message is: Inferred type is less polymorphic than expected Quantified type variable `t2' is unified with `H' When checking an existential match that binds k :: C t2 a -> IO t a The pattern(s) have type(s): C t1 () The body has type: IO H () In the definition of `s1': s1 (C k) = trans (True) (k (C s1)) (s1 (C k)) The thing is, I'm perfectly happy with t2 being unified with H for this particular definition of s1, but I want to use it in other cases as well. The code that follows the one above is s2 :: C t () -> IO L () s2 (C k) = trans (True) (k (C s2)) -- :: IO t () (s2 (C k)) -- :: IO L () main = s1 (C s2) where t2 instead gets unified with L for the definition of s2. Could someone tell me why this does not work? I'm using GHC 6.2.2. Thanks, /Niklas

Am Mittwoch, 30. März 2005 10:17 schrieb Niklas Broberg:
I just can't see why the following code will not type check. I have scaled it down as much as possible:
------------------------------------- -- IO with an extra level annotation newtype IO' t a = MkIO' (IO a)
from here on you wrote just IO, not IO'.
-- levels data H data L
-- Explicitly recursive continuation type data C t a = forall t2 . C (C t2 a -> IO t a)
If you write data C t a = C (forall t2 . C t2 a -> IO' t a), it will compile (versions 6.2.2, 6.4). Whether that'll do exactly what you want, I don't know :-(
transition :: Bool -> IO tx () -> IO t () -> IO t () transition b c d = undefined
s1 :: C t () -> IO H () s1 (C k) = trans (True) (k (C s1)) -- :: IO t () (s1 (C k)) -- :: IO H ()
trans = transition, I suppose?
-------------------------------------- The error message is: Inferred type is less polymorphic than expected Quantified type variable `t2' is unified with `H' When checking an existential match that binds k :: C t2 a -> IO t a The pattern(s) have type(s): C t1 () The body has type: IO H () In the definition of `s1': s1 (C k) = trans (True) (k (C s1)) (s1 (C k))
6.4's error message is: Niklas.hs:21:26: Couldn't match the rigid variable `t2' against `H' `t2' is bound by the pattern for `C' at Niklas.hs:20:4-6 Expected type: C t21 () -> IO' t2 () Inferred type: C t21 () -> IO' H () In the first argument of `C', namely `s1' In the first argument of `k', namely `(C s1)' hugs gives ERROR "./Niklas.hs":20 - Type error in application *** Expression : k (C s1) *** Term : C s1 *** Type : C H () *** Does not match : C _3 () *** Because : cannot instantiate Skolem constant Now I'm not an expert, but I think it's roughly thus: by the original definition, from the pattern 'C k', it follows that there is some type, call it t1, such that k has type C t1 () -> IO' t (). Now applying k to C s1 requires t1 to be H, which may or may not be the case, that can't be decided by pattern matching. Says the user's guide (I'm not quite certain that this is about the case in hand): In general, you can only pattern-match on an existentially-quantified constructor in a case expression or in the patterns of a function definition. The reason for this restriction is really an implementation one. Type-checking binding groups is already a nightmare without existentials complicating the picture. Also an existential pattern binding at the top level of a module doesn't make sense, because it's not clear how to prevent the existentially-quantified type "escaping". So for now, there's a simple-to-state restriction. We'll see how annoying it is. If you shift the forall, the argument of C is required to be polymorphic, so all compilation problems disappear.
The thing is, I'm perfectly happy with t2 being unified with H for this particular definition of s1, but I want to use it in other cases as well. The code that follows the one above is
s2 :: C t () -> IO L () s2 (C k) = trans (True) (k (C s2)) -- :: IO t () (s2 (C k)) -- :: IO L ()
main = s1 (C s2)
where t2 instead gets unified with L for the definition of s2. Could someone tell me why this does not work? I'm using GHC 6.2.2.
Thanks,
/Niklas
I would like a detailed explanation, too. Daniel

-- Explicitly recursive continuation type data C t a = forall t2 . C (C t2 a -> IO t a)
If you write
data C t a = C (forall t2 . C t2 a -> IO' t a),
it will compile (versions 6.2.2, 6.4). Whether that'll do exactly what you want, I don't know :-(
Actually, I think it does. Originally I thought this would be too restrictive, since all possible continuations must then be polymorphic in their argument, but in practise that's actually the case anyway. :-)
transition :: Bool -> IO tx () -> IO t () -> IO t () transition b c d = undefined
s1 :: C t () -> IO H () s1 (C k) = trans (True) (k (C s1)) -- :: IO t () (s1 (C k)) -- :: IO H ()
trans = transition, I suppose?
Indeed... the dangers of trimming code for the sake of presentation... :-)
-------------------------------------- The error message is: Inferred type is less polymorphic than expected Quantified type variable `t2' is unified with `H' When checking an existential match that binds k :: C t2 a -> IO t a The pattern(s) have type(s): C t1 () The body has type: IO H () In the definition of `s1': s1 (C k) = trans (True) (k (C s1)) (s1 (C k)) [...]
Now I'm not an expert, but I think it's roughly thus: by the original definition, from the pattern 'C k', it follows that there is some type, call it t1, such that k has type C t1 () -> IO' t (). Now applying k to C s1 requires t1 to be H, which may or may not be the case, that can't be decided by pattern matching.
You are right of course. k is not polymorphic in its argument, since t1 is not a type variable but an actual type. we just don't know which type that is, and we certainly can't guarantee that it's H. Moving the forall to make k polymorphic solves the problem, just like you said above. Thanks a lot, /Niklas

Just to be able to understand this small thread, does someone have any pointer explaining (with examples ?) what exactly is this "forall" extension to haskell ? Thanks, -- Pierre Barbier de Reuille INRA - UMR Cirad/Inra/Cnrs/Univ.MontpellierII AMAP Botanique et Bio-informatique de l'Architecture des Plantes TA40/PSII, Boulevard de la Lironde 34398 MONTPELLIER CEDEX 5, France tel : (33) 4 67 61 65 77 fax : (33) 4 67 61 56 68

Am Donnerstag, 31. März 2005 15:30 schrieb Pierre Barbier de Reuille:
Just to be able to understand this small thread, does someone have any pointer explaining (with examples ?) what exactly is this "forall" extension to haskell ?
Thanks,
The GHC user's guide, section 7.4 says something about it. As a small remark, Haskell is full of implicit 'forall's whenever you define a polymorphic function, e.g. the type signature map :: (a -> b) -> [a] -> [b] means the same as map :: forall a b. (a -> b) -> [a] -> [b], (free) type variables are implicitly universally quantified, so you needn't give the 'forall's explicitly. The options -fglasgow-exts for ghc and -98 for hugs allow you to explicitly write them in your code, as well as to put them in various places to give them different meanings. Recall the difference between continuity of a function: forall x. forall epsilon. exists delta. forall y. |x - y| < delta => |f(x) - f(y)| < epsilon (the delta depends on epsilon and x) and uniform continuity forall epsilon. exists delta. forall x. forall y. |x - y| < delta => |f(x) - f(y)| < epsilon, where the delta depends only on epsilon. Analogously, referring to Niklas' code (inserting 'T' and 'D' to distinguish between type constructors and data constructors), data CT t a = forall t2. CD (CT t2 a -> IO' t a) means the data constructor CD is polymorphic, you may pass functions CT Int a -> IO' t a, CT Bool a -> IO' t a etc. to it, but the passed functions aren't in general polymorphic. And since the compiler can't infer the type of 'k' from the pattern 'CD k', you can't do much with it, for example, applying k to some value x isn't allowed, because the compiler can't be sure that x has the appropriate type (I haven't tried, but probably if x is polymorphic, i.e. has type forall u. CT u a, it'd be ok). If you shift the forall past the data constructor, the meaning is different: data CT1 t a = CD1 (forall t2. CT1 t2 a -> IO' t a) means the argument of the data constructor CD1 must be a polymorphic function. Then from a pattern 'CD1 k' to extract k and apply it to some value is unproblematic. And one about functions: consider applyEndo :: {- forall a. -} Ord a => (a -> a) -> a -> a applyEndo f x = f x versus applyPolyEndo :: Ord b => (forall a. Ord a => a -> a) -> b -> b applyPolyEndo f x = f x, applyEndo takes monomorphic functions as first argument, e.g. 'not :: Bool -> Bool' whereas applyPolyEndo takes only polymorphic functions like 'id' or 'error . const "too bad"' as first argument. If you give no forall explicitly, it' s inserted as in applyEndo, if you want the more restrictive applyPolyEndo, you must do it explicitly. So by putting a forall in the appropriate place, you can define 'polymorphic' datatypes and functions which you otherwise couldn't. Hope this gives a start, Daniel
participants (4)
-
Arjan van IJzendoorn
-
Daniel Fischer
-
Niklas Broberg
-
Pierre Barbier de Reuille