[m-dev.] Existential and universal types (was: Re: univ and functor/arg)

[Fergus Henderson]

Harald Sondergaard, you wrote:
> 
> Fergus Henderson <fjh at cs.mu.OZ.AU> writes:
> >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.

Ah, yes, you're right.  [Or at least almost right.  See below.]

Note that this is different concept to the concept I was elaborating
on in my mail.  I was explaining the meaning of quantifiers on type
declarations, you are talking about the meaning of quantifiers on types.

At the end of my previous mail I looked at

	:- all [T] type univ == T.
and
	:- some [T] type univ == T.

and explained why they wouldn't work.  However, what I failed
to point out is that they are quite different to

	:- type univ == some [T] T.

The former have an implicit quantifier on the type _declaration_,
the latter has a quantifier on the type T itself.

The semantics of universal/existential quantification on types 
could be defined by the following axioms.   These axioms state
when a term can have a universally or existentially quantified
type.

	well_typed(Term, some [TVar] Type) <=
		some [T] well_typed(Term, subst(Type, Tvar, T)).
	well_typed(Term, all [TVar] Type) <=
		all [T] well_typed(Term, subst(Type, Tvar, T)).

[Here `subst(Type, Var, T)' denotes the result of substituting
`T' for all free occurrences of `Var' in `Type' (technically
speaking, we should add axioms defining that precisely).
We can't just write

	well_typed(Term, all [TVar] Type) <=
		all [TVar] well_typed(Term, Type).

because that would be confusing the meta- and object- level
variables.]

These definitions are very natural, and your definitions
in terms of union/intersection basically follow from these
(just find the set of ground terms which satisfy those axioms).

However, including these existentially quantified types in a type
system might cause severe problems.  For example, it would be very
undesirable for the typechecker to accept `42 = "blah"' because
both sides of the unification can be assigned the type `some [T] T'.
I haven't thought about it too hard, but at very least you would
have to revisit the definition of type correctness and figure
out what "unique most general consistent type assignment" meant
in the presence of quantified types.

Also, I think there is a problem with your definitions;
in general, I don't think a universally quantified type
can be fully characterized by a set of values. 
The example below shows this.

> >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?

No.  The empty list is the only ground object-level term
with that type.  But non-ground object-level terms can have that
type (and can then become bound to non-empty ground lists at runtime).
`X' here is a meta-level variable, it ranges over both ground and
non-ground object-level terms.

> 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?

Yes.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.