[Haskell-cafe] Existential problem

[Daniel Fischer]

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