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