Existential and universal types (was: Re: univ and functor/arg)

[Harald Sondergaard]

Fergus Henderson <fjh at cs.mu.OZ.AU> writes:
>Peter Schachte, you wrote:
> > 
> > > However, if you think of `univ' as conceptually defined
> > > by
> > > 
> > > 	:- type univ == some [T] T.
> > 
> > For the clueless among us, can you briefly explain what the type
> > 
> > 	some [T] T 
> > 
> > means?

>I'm not really sure whether `some [T] T' does mean anything;
>that's why I said I wasn't quite sure that the above definition of `univ'
>as an equivalence type makes sense.

It seems perfectly sensible to say that `some [T] T' is the universal type,
by duality with the universal quantifier.  Universal quantification on 
types means taking the intersection of (possibly infinitely many) monotypes.
Similarly existential quantification ought to mean taking the union.  For
example, 
		forall [T] list(T)

has a single inhabitant, the empty list, while

		some [T] list(T)

is inhabited by every list.

>What does `all [T]' well_typed(X, list(T))' mean?
>It means that `X' must be assigned a polymorphic type.

Yes, the intuition here is clear.  X must be the empty list, right?

>Higher-order polymorphic predicates get even more confusing, so
>I won't go into them.

Actually that would be very useful work -- to explain Mercury's entire type
system with all the formal details.  For example, existential types aside,
does the type system agree with Milner's (Damas-Milner) on the functional 
subset?  Milner needs to distinguish a free type ...T... from the
universally quantified `forall [T] ...T...', to allow correct type assignment
to variables that have multiple occurrences (in the same scope).  Is there 
a similar distinction in Mercury's type system?  For example, with Damas-
Milner,
		len = length [42] + length [True]

is well-typed, while

		len = (\fn => fn [42] + fn [True]) length

is not.  Would that still be the case when these expressions are suitably
translated to Mercury?

Harald