Existentials

[Hans Aberg]

At 09:02 +0100 2003/04/17, Simon Peyton-Jones wrote:
>	Allow 'exists'
>	Deprecate 'forall' (for defining existentials, that is)
>	Eventually allow only 'exists'
>
>
>Does anyone have any opinions on this topic?  It's a small point, but
>one that bites quite frequently.

I have to come to think about this type of questions, but in another
context, namely, when I was implementing a version of Prolog in the form of
a proof-verification system building on metamathematics (= metalogic)
rather than the standard logic. See for example, Elliott Mendelson,
"Introduction to Mathematical Logic". You might pick down a program called
"Qu-Prolog" to get an input on similar metalogical ideas in the form of a
generalized Prolog system for bound variables:
 Qu-Prolog:
  http://www.svrc.it.uq.edu.au/pages/QuProlog_release.html
  Earlier versions
  http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?00-20
  http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?00-21
 Ergo
  http://www.svrc.it.uq.edu.au/pages/Ergo_release.html

In such a context, it looks as though the natural extension of the type
theory is axiomatic set theory. So I am therefore inclined to think that
one should do whatever is correct in math, in order to pave the way for a
natural development.

As for naming conventions, I favor a naming without prepositions and
endings, if possible. For example, "+" might be called "addition", even
though "a + b" is read "a added to b". So one might use the words "all" and
"exist" simply.

At 10:05 +0200 2003/04/17, Doaitse Swierstra wrote:
>I think that (in line with the other type notation conventions where
>you do not have to be explicit) you should not be forced to write
>anything at all, but I am sure I will remain a minority ;-}

Actually, in metamathematics, there is a difference between quantified and
unquantified formulas (variables with "all").

>Many of you have grown to love existential data types, which we current
>write like this:
>
>	data T = forall a. Foo a (a -> Int)
>
>Mark and I chose 'forall' rather than 'exists' to save grabbing another
>keyword from the programmer.  And indeed, the type of the constructor
>Foo is
>	Foo :: forall a. a -> (a->Int) -> T
>
>But every single time I explain this to someone, I find I have to make
>excuses for using the term 'forall'.  I say "it really means 'exists',
>but we didn't want to lose another keyword".

A mathematical formulation of T is perhaps:
    T := V_{a in I} a x Hom(a, Int)
where V sands for the disjoint union (= coproduct in the category of sets).

So one computer approximating analogue might then be "exist".

  Hans Aberg