> On a related note, can anyone point out a good document that lists the
> difference between universal quantification, existential quantification,
> and "normal" quantification. I assume that normal quantification /is/
> universal quantification, but why would someone desire to be explicit?
> Under what circumstances does it make sense to use existential
> quantification? It would be helpful if such a document used valid
> examples (i.e., no functions or types named "foo") so that I can see
> what Read World(tm) problem is being solved.
Universal = For all...;
Existential = There exists...;
Explicit universal quantification has the following features:
1 No "hackers in the trenches" will be able to wonder what the difference is
between "normal" quantification and universal quantification.
2 It's more consistent with mathematic syntax. Especially if your editor
supports the "upside down 'A'" char.
3 Rank 2 and higher order polymorphism require it.
Obviously 3 is the only reasonable argument of the above toward making univ.
quant. explicit. But it's an open question as to whether Rank 2+
polymorphism is useful/will make it into Haskell2. I'm curious to see if
anybody whose actually used this feature in Hugs has found it useful?
Since you're a self proclaimed hacker, I'll dispense with the mathematics:
existentials are (IMO) essential to ADTs. They allow you to do precisely the
following:
- hide the implementation type of an ADT.
The idea is that there can be many possible implementations types of an ADT.
E.g., a set as a list, a tree, a whatever. But we want to think of the type
abstractly, as a *set*, not as a list, a tree, a whatever. Only with
existentials can we do this.
Suddenly, ideas like "a list of sets" becomes possible. This list is called
"heterogeneous" when the list actually has elements of differing type even
though they're the same ADT.
One caveat of existential types is that since the type is hidden, all
functions on the type must be provided by the interface to the type, either
with a type class or predicting the existential with its functions (in the
algebraic type) or something. So, if you have a set s that's actually
implemented as a list, you can't do length s, or foldr ... s, etc.
If you're really in a pleasant mood, you can think of this less as a
restriction and more as "wow, existential types are like built in
enforcement of abstraction boundaries, neato!"
Oh an by the way, if this isn't against the law, a good paper on the utility
of existential demonstrated in a slightly non-trivial way is the following:
ftp://ftp.cs.kun.nl/pub/Clean/papers/cleanbook/II.04.OODrawing.pdf
ftp://ftp.cs.kun.nl/pub/Clean/papers/cleanbook/II.04.OODrawing.ps.gz
