[m-rev.] for discussion: subtypes documentation

[Fergus Henderson]

On 24-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> +A variable's instantiatedness tree therefore describes (for first order terms)
> +a subset of the values of the variable's type.

Why the restriction to first order terms?

> +The values described by a subtype are meant (for first order types)
> +to be a subset of those described by the supertype.  Hence for each
> +function symbol in the body of the subtype declaration there must be a
> +matching function symbol in the definition of the supertype, and each
> +argument of the former should in turn be a subtype of
> +the corresponding argument of the latter.

Please be careful about using "is", "must be", and "should be"
in the reference manual.  "must be" should be used for conditions
that the compiler checks (or, if it is a dynamic property, that the
system checks at run-time).  "should be" should be used for conditions
which the compiler doesn't check.  "is" should be used for definitions.

> +The only subtype of a universally quantified type variable
> +is the variable itself,

What about the empty subtype (the one with inst "not_reached")?

> +A subtype constructor can be used in some, but not all,
> +of the places where it is legal to use a type constructor.
> +Subtypes are allowed in predicate and function declarations,
> +in method declarations in the ``where'' part of typeclass declarations,
> +and in the bodies and supertypes of subtype declarations.
> +Subtypes are not allowed anywhere else;
> +in particular, they are not allowed to be used in the definition
> +of ordinary types (i.e., those defined with a @code{type} declaration),
> +or on the right hand side of a @code{with_type} qualifier in a goal.

I think we should allow subtypes in the bodies of type definitions.
Otherwise, subtypes would be too much second-class citizens.

Here is a proposed semantics for them.  For a discriminated union definition
which has parameters P_1, P_2, ..., P_n
(think of "_" as the Latex subscript operator ;)
and which uses subtypes s_1 < t_2, s_t < t_2, ..., s_m < t_m,
the type definition will be of the form

	:- type t(P_i) ---> f_j(... s_k ...).

(That is, it will be of the form

	:- type t(P_1, ..., P_n) ---> f_1(...) ; f_2(...) ; ... ; f_m(...).

where the s_k occur somewhere in the body of the type definition.)
We can define the semantics of this to be equivalent to

	:- type t_base(...)             ---> f_i(... t_j ...).
	:- subtype t(...) < t_base(...) ---> f_i(... s_j ...).

where t_base/n is a fresh name not occurring in the program.

For equivalence types, subtypes should certainly be allowed in the body;
the semantics of the equivalence type is the same as if the programmer
had referred to the subtype directly (i.e. you just replace any uses
of the equivalence type with the body, substituting the parameters as usual).

> + at node Higher-order subtypes
> + at section Higher-order subtypes
> +
> +As stated earlier, the subtype relation on first-order types
> +is the same as the subset relation.
> +For higher-order types, the subtype relation is slightly more complex.
> +We extend the relation to higher-order types with the following two cases.
> +
> + at itemize @bullet
> + at item
> +A type @code{func(@var{S1}, @dots{}, @var{SN}) = @var{S}}
> +is a subtype of @code{func(@var{T1}, @dots{}, @var{TN}) = @var{T}}
> +iff @var{S} is a subtype of @var{T},
> +and for each argument @var{i}, @var{Si} is a subtype of @var{Ti}.
> +
> + at item
> +A type @code{pred(@var{S1}, @dots{}, @var{SN})}
> +is a subtype of @code{pred(@var{T1}, @dots{}, @var{TN})}
> +iff for each argument @var{i}, @var{Si} is a subtype of @var{Ti}.
> +
> + at end itemize
> +
> + at noindent
> +In other words the subtype relation on predicate and function types
> +is @emph{covariant} in the argument values
> +and (for function types) the return values.
> + at c This is in contrast to the usual object-oriented view of subtypes,
> + at c where inputs are contravariant and outputs are covariant.  We use
> + at c covariant subtypes because they work much better with parametric
> + at c polymorphism.
> +Mercury's mode system provides enough information for the compiler
> +to statically check that the use of covariant subtypes is safe.

I think this is wrong.

The mode system uses covariant subtyping for the
final insts and contravariant subtyping for the initial insts.
Using covariant subtyping for the initial insts would be unsafe.

Hmm, looking at the source, I see that although we use contravariant
subtyping for inst_matches_final, like we should, currently we are
using covariant subtyping for inst_matches_initial.  Ouch -- that looks
like a bug... 

Yep, it sure is.  I just got it to seg fault when running an example
program.  (See attached.)

We used to get this right, I'm pretty sure -- it appears to have
been broken by dmo's change to add support for polymorphic modes.

Anyway, once that bug is fixed, the mode system will be back to using
covariant subtyping for the final insts but contravariant subtyping for
the initial insts.  For subtypes, that implies that we'll use
contravariant subtyping for input arguments and covariant subtyping
for output arguments.  Just like in the usual OOP view of subtypes.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
-------------- next part --------------
:- module bug.
:- interface.
:- import_module io.

:- pred main(io__state::di, io__state::uo) is det.

:- implementation.
:- import_module list, bool.

main -->
	( { q(p) } ->
		print("yes"), nl
	;
		print("no"), nl
	).

:- type intlist == list(int).
:- inst nonempty ---> [ground|ground].

:- pred p(intlist, intlist).
:- mode p(in(nonempty), out(nonempty)) is det.

p([X], [X]).
p([X,Y|Zs], [Y,X|Zs]).

:- pred q(pred(intlist, intlist)).
:- mode q(pred(in, out) is det) is semidet. 

q(P) :- P([], L), L \= [].