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