Fri, 5 Nov 1999 22:26:17 +1300, Nigel Perry <[EMAIL PROTECTED]> pisze:
> I missed the start of this and am a bit confused - I keep seeing
> "forall", which is universal, not "there exists", which is
> existential - at least as I know them. Are the existentials talked
> about in relation to Haskell something different, or has the notation
> just got confused?
This is explained in GHC User's Guide.
A value of type
data Action = forall b. Act (IORef b) (b -> IO ())
is something like "there exists some type b, such that this is a pair
of IORef b and b -> IO ()".
The forall notation of existentials reflects the type of constructor
function. Here the constructor has type
Act :: forall b. IORef b -> (b -> IO ()) -> Action
which in Haskell 98 is written simply as
Act :: IORef b -> (b -> IO ()) -> Action
(GHC and Hugs allow writing foralls explicitly). But it is almost
isomorphic to
Act' :: (exist b. (IORef b, b -> IO ())) -> Action
(there is no actual 'exist' keyword). Existential quantification in
the function's argument is equivalent to universal quantification of
the whole function type.
Mark P. Jones in his great paper ``First-class Polymorphism with
Type Inference'' <http://www.cse.ogi.edu/~mpj/pubs/popl97-fcp.ps>
explains that the dual equivalence (exist. <-> univ.) would be
incorrect. I have yet to read about Curry-Howard isomorphism to
understand these things...
In some sense values having existentially quantified types are hard
to deconstruct, while those with universally quantified components
are hard to build. GHC has quite complicated rules of what is legal
regarding quantification. Some constructs are surprisingly not legal
where there are legal versions obtained by innocent changes like
eta-expansion, binding function arguments on the left side of `='
instead of with a lambda, case-matching a bound variable instead of
direct binding to a pattern, deconstructing by case instead of by let,
and adding type signatures.
Instead of providing separate pack+open constructs, GHC/Hugs extend
the syntax of declarations of datatypes, so that building and using
values of quantified types simply looks like using constructors and
pattern matching, modulo those non-obvious rules about what is actually
legal. I like this approach, because although the implementation is
non-trivial, IMHO the need of quantified types seems to occur in not
so "special" cases and there may be a smooth transition between using
quantified types and solving the problem without them, with quite
similar datatype structures. Disclaimer: I don't have experience,
just feeling.
Anybody with a practical example of both existential and local
universal quantification in a single constructor? :-)
--
__("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a22 C+++>+++$ UL++>++++$ P+++ L++>++++$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP->+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e>++++ h! r--%>++ y-
