forall vs. exists

George Russell
Thu, 17 Apr 2003 18:26:24 +0200

1) The problem is basically whether you regard the type constructor
as a way of constructing a type or of taking it apart.
So using the current notation

    data A = forall x . B x => C x

forall seems sensible if you think of a constructor as a way of
constructing a type (for all x that's a B, C gives you an A), but
not if want to take it apart, where your attitude is
(there exists an x that's a B that's inside this C).

I really can't see any reason for preferring the viewpoint of the
constructor to the destructor, or vice-versa.  So my vote would be for
keeping things as they are.

2) I currently existential datatypes 17 times or thereabout.  Replacing
"forall" by "exists" through all these would be annoying, but not take
very long.  Also there seem to be two modules which use the variable name
"exists", but while having to replace that would be annoying, again it
wouldn't take very long.  Altogether perhaps 20 minutes, if that.
So while the suggested change-over would be a pain, it wouldn't be a major