[Haskell-cafe] Existential problem
Daniel Fischer
daniel.is.fischer at web.de
Thu Mar 31 14:08:19 EST 2005
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
More information about the Haskell-Cafe
mailing list