[m-dev.] Re: univ and functor/arg

[Fergus Henderson]

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?

To paraphrase someone famous, I'm afraid I don't have time to explain
it briefly, but I can explain it at length.

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.

Type quantifications do make sense on type declarations for function,
predicates, and on definitions of discriminated union types, and
on function types or predicate types.

Let's start by defining the semantics of simple type declarations.
Each type declaration tells us something about the set of well-typed terms.
We can explain the declarative semantics of type declations by
converting them to predicate calculus; in particular, each
type declaration corresponds to some clauses (axioms) for a predicate
`well_typed(Term, Type)'; the semantics of this predicate are that 
`well_typed(Term, Type)' is true iff `Term' is a valid syntactic
construct of type `Type'.  Note that `well_typed' is not a function
from terms to types, because a term may have more than one type,
due to either polymorphism or overloading.

For example, here are some simple type declarations and their
semantics.  The semantics are written below as clauses for well_typed/2,
using the usual rules for implicit quantification; to get the
complete semantics, you need to make the implicit quantifications
explicit and take the Clark completion of all the clauses for
well_typed/2.

	Declaration:	:- type bool ---> yes ; no.
	Semantics:	well_typed(X, bool) <=
				X = yes ; X = no.

	Declaration:	:- type list(T) ---> [] ; [T | list(T)].
	Semantics:	well_typed(L, list(T)) <= (
				L = []
				;
				L = [Head | Tail],
				well_typed(Head, T),
				well_typed(Tail, list(T))
			).

Equivalence types are a bit different: they just add aditional type equality
axioms.

	Declaration:	:- type foo(T) == bar(T, T, int).
	Semantics:	foo(T) = bar(T, T, int).

OK, now lets try predicate declarations:

	Declaration:	:- pred p(int, string).
	Semantics:	well_typed(p(X, Y), pred) <= (
				well_typed(X, int),
				well_typed(Y, string)
			).

Actually to handle higher-order Mercury code we also need a couple
of other clauses:

			well_typed(p(X), pred(string)) <=
				well_typed(X, int).
			well_typed(p, pred(int, string)).

Next, polymorphic predicate declarations:

	Declaration:	:- pred q(list(T), int).
	Semantics:	well_typed(q(X, Y), pred) <= (
				well_typed(X, list(T)),
				well_typed(Y, int)
			).

Note that T is implicitly universally quantified over the whole scope.
The declaration is implicitly

			:- all [T] (
				pred q(list(T), int)
			).

and the semantics are implicitly

			all [T, X, Y] (
				well_typed(q(X, Y), pred) <= (
					well_typed(X, list(T)),
					well_typed(Y, int)
				)
			).

Note however that the global universal quantifier is logically equivalent
to a local existential quantifier

			all [X, Y] (
				well_typed(q(X, Y), pred) <= (
					some [T] well_typed(X, list(T)),
					well_typed(Y, int)
				)
			).

so it is easy to get confused ;-)
Higher-order polymorphic predicates get even more confusing, so
I won't go into them.

You also need a few additional clauses (axioms) for well_typed, to deal with
the builtin types, and to define well-typed clauses and well-typed goals.

A program is type-correct iff there is a unique (modulo renaming of
type variables) most general consistent assignment of types to terms
in the program such that for every term Term, if Type is the (possibly
nonground) type assigned to Term, then well_typed(Term, T) is true for
every T that is an instance of Type.


Make sense so far?

OK, now for the semantics of existential type quantifiers on predicate
declarations:

	Declaration:	:- some [T] pred p(list(T), int).
	Semantics:
			some [T] (
				well_typed(p(X, Y), pred) <= (
					well_typed(X, list(T)),
					well_typed(Y, int))
				)
			).
	or equivalently
			well_typed(p(X, Y), pred) <=
				all [T] well_typed(X, list(T)),
				well_typed(Y, int)).

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

Existential type quantifiers on type definitions are similar.
Ordinary definitions look like this:

	Declaration:	:- type foo(T) ---> f(T).
	Semantics:	well_typed(X, foo(T)) <= (
				X = f(Y), well_typed(Y, T)
			).
Here all variables are implicitly universally quantified over
the scope of the whole type declaration or the whole clause.

Now what happens if we take `T' out of the head?

	Declaration:	:- type foo ---> f(T).

This is not curently allowed in Mercury, but by analogy, if it
was, the variables should still be universally quantified over
the scope of the whole type declaration; the declaration should
be the same as

			:- all [T] (
				type foo ---> f(T)
			).

and the semantics should be

	Semantics:	% all [X, Y, T]
			well_typed(X, foo) <= (
				X = f(Y), well_typed(Y, T)
			).
	or equivalently
			well_typed(X, foo) <= (
				X = f(Y), some [T] well_typed(Y, T)
			).
	
What does this mean for type checking?
Well, this type `foo' is basically equivalent to `univ',
and the constructor `f/1' is basically equivalent to the function univ/1
in std_util.m.

(Many type systems don't allow this, because it requires run-time
type checking.)

What would

	:- type univ == T.

mean?  It would mean

	all [T] univ = T.

which would imply

	all [T1, T2] T1 = T2.

which seems kinda undesirable.

So, I don't think that is viable as a consistent model.

We could however just treat `univ' as a special case.  That would
work, but it wouldn't be very elegant.  On the other hand, the alternatives
aren't very elegant either, at least not without support for an existentially
typed univ_value/1; even then, it would be tricky to remember exactly
when to call univ_value/1, and the compiler couldn't easily catch mistakes.

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