On 05-Jun-1998, Simon L Peyton Jones <[EMAIL PROTECTED]> wrote:
>
> In hbc (and soon in GHC) you can say:
>
> data OrganizationThing = forall a. Organisation a => MkOrg a
Last time I looked (at <http://www.cs.chalmers.se/~augustss/hbc/decls.html>),
hbc was using a different syntax:
data OrganizationThing = Organisation ?a => MkOrg ?a
> (Some people would write "exists" instead of "forall", and that's
> reasonable. But the type of MkOrg really is
>
> MkOrg :: forall a. Organization a => a -> OrganizationThing
> )
I'm not sure that I entirely buy this argument. The type of MkOrg
depends on the context in which it is used -- if you're using
it as a constructor, then yes it has that (universally quantified)
type, but if you're using it as a deconstructor then it has the
converse (existentially quantified) type.
So, which is a data declaration more like, construction or
deconstruction? Well, the `|' to seperate alternatives in a data
declaration is similar to the `|' used to seperate alternatives in a
pattern match or in a case expression. Indeed, the form of the data
declaration parallels the form of the code needed to perform a
recursive traversal of it.
data Blah = Foo
| Bar
| Baz
case blah in Foo => ...
| Bar => ...
| Baz => ...
func Foo = ...
| Bar = ...
| Baz = ...
This suggests to me that maybe it
would be better to treat functors in data declarations like deconstructors
rather than like constructors and thus to use "exists" rather than
"forall".
If you're going to use the syntax `forall', will you start calling
them "universal types" rather than "existential types"?
Quantifiers can be very confusing even if everyone agrees on the
same terminology. Are you sure you want to go against the established
terminology here?
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
