Existentials

Lauri Alanko la@iki.fi
Thu, 17 Apr 2003 12:52:35 +0300


On Thu, Apr 17, 2003 at 09:02:45AM +0100, Simon Peyton-Jones wrote:
> 	data T = forall a. Foo a (a -> Int)

I find this perfectly acceptable and consistent. The right hand side of
a data type declaration lists the ways to construct an element of the
data type. I read

data List a = Cons a (List a) | Nil

as

"To construct an element of type 'List a', you can either build a Cons
from an 'a' and a 'List a', or you can build a Nil."

So likewise,

data T = forall a. Foo a (a -> Int)

reads as

"To construct an element of type 'T', you can, for all types 'a', build
a Foo from an 'a' and a 'a -> Int'.

An "exists" quantifier would make sense for real existential _types_:

data T = Foo (exists a . (a, a -> Int))

but for the current use, "forall" is quite appropriate, in my opinion.


Lauri Alanko
la@iki.fi