[m-rev.] for discussion: subtypes documentation

[Fergus Henderson]

On 24-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> The following diff is a draft of the subtypes documentation.  I'm not
> intending to commit this yet; I'm posting this now to allow any early
> review comments on the design.
> 
> A couple of notes about the diff:
> 
> 	- The given syntax cannot express some subtypes that we may wish
> 	  to use.  For example, there is no way for the supertype to be
> 	  a pred or func type.  We may therefore need one or more
> 	  additional variants on the syntax, such as the first variant
> 	  in Fergus' proposal.

Definitely.

> 	- I've expounded on subtypes a little bit more in the modes
> 	  section, describing subtype information as being attached
> 	  to the and-nodes of a type tree.  That was the simplest way I
> 	  could find of describing the semantics of subtypes.

The existing documentation in the modes chapter is not good, IMHO.
It probably needs a complete rewrite.  I think we should start off
by describing the simplest modes `in' and `out', and then add
each new feature one at a time (subtypes, partially instantiated modes,
dynamic modes, unique modes) and then giving a formal definition
which encompasses all of these.

One problem with your proposed wording is that it uses the names "free" and
"bound" for annotations on and-nodes; these annotations are recording
subtype information, not boundedness information, so they should have
different names, e.g. "reachable" and "unreachable".

Another problem is that it further complicates an
already-too-complicated part of the reference manual.
I think addressing this properly would probably require a more
general rewrite along the lines outlined above, so I guess
that could be done as a separate change.

> Index: reference_manual.texi
...
>  The type system is based on many-sorted logic, and supports polymorphism,
> -type classes (@pxref{Type classes}), and existentially quantified types
> -(@pxref{Existential types}).
> +type classes (@pxref{Type classes}), existentially quantified types
> +(@pxref{Existential types}), and subtypes (@pxref{Subtypes}).

I suggest
s/and subtypes/and (in conjunction with the mode system) subtypes/

> + at node Subtypes
> + at chapter Subtypes
> +
> +Subtype information about variables is expressed by Mercury's mode system.
> +For a given or-node in an instantiatedness tree,
> +the set of function symbols which may occur at that location in a term
> +is specified by which of the children of the or-node are bound.
> +This set does not necessarily include every function symbol
> +in the corresponding type,
> +since some and-nodes may be free.
> +A variable's instantiatedness tree therefore describes (for first order terms)
> +a subset of the values of the variable's type.
> +
> +To make subtypes easier to use,
> +Mercury allows users to declare subtypes such as
> +
> + at example
> +:- subtype non_empty_list(T) < list(T) ---> [T | list(T)].
> + at end example

"Easier to use" than what?
Did the documentation explain how to use subtypes with `:- inst'
declarations yet?  If not, then the bit about "To make subtypes
easier to use" won't make sense to readers.

> +This subtype describes a list whose top function symbol is @code{[|]/2},
> +whose first argument has a subtype given by the parameter @code{T},
> +and whose second argument is any list of @code{T}'s.
> +If this subtype is used in an argument of a predicate or function
> +declaration, the subtype information is propagated into the
> +corresponding modes in a way we describe below.
> +
> + at menu
> +* Subtype declarations::
> +* Semantics of Mercury programs with subtypes::
> +* An example using subtypes::
> + at c * Abstract subtypes::
> +* Higher-order subtypes::
> + at end menu
> +
> + at node Subtype declarations
> + at section Subtype declarations
> +
> +Subtype declarations have the form
> +
> + at example
> +:- subtype @var{Sub} < @var{Super} ---> @var{Body}.
> + at end example
> +
> + at noindent
> + at var{Sub} is a non-variable type
> +whose arguments (if any) are distinct variables.
> + at var{Super} is a type or subtype.
> + at var{Body} is a sequence of constructors separated by semi-colons,
> +whose arguments are types or subtypes.

s/@var{Sub}/where @var{Sub}/
and s/variables./variables;/
and s/subtype./type; and/

(Or alternatively, s/is/must be/g.)

> +Types or subtypes in the body of the definition may be inst qualified
> +using the @code{::} operator,
> +provided that the specified inst is compatible with @code{ground}.

This should either explain what "compatible" means,
or give a cross-reference to the place where it is explained.

> +Any type variable appearing in @var{Super} must also appear in @var{Sub}.
> +Any type variable appearing in @var{Body} must also appear in @var{Super},
> +except that anonymous variables (i.e., variables beginning with @code{_})
> +are allowed to appear in the body.

Why the special treatment for variables beginning with @code{_}?
This is not consistent with the way we handle them in other parts of
the language.

Only variables whose name is "_" are anonymous.
Variables whose name merely begins with "_" are ordinary variables.
The use of "_"-prefixed names for singletons is a style issue
enforced by compiler warnings, not an official part of the language.

> +Circularities are not allowed, so it is an error if some part of @var{Super}
> +is ultimately defined to be a subtype of @var{Sub}.

This is a bit too vague.  Neither "circularities" nor "ultimately defined"
are defined.

Also, I think some kinds of circularities should be allowed.
For example, I think it should be OK to do

	:- type t ---> foo(subt) ; bar.
	:- subtype subt < t ---> bar.

> +The only subtype of a universally quantified type variable
> +is the variable itself,
> +so where the supertype uses such a variable the subtype must use the
> +same variable in the corresponding location.
> +Similarly, where the supertype uses an existentially quantified type variable
> +the subtype must use an anonymous type variable in the corresponding location.
> +Existential quantifiers and class constraints are always implicitly
> +determined from the supertype, and should not be explicitly given.

Hmm.  What about the case where an existentially quantified type
variable occurs twice?

	:- type t ---> some [T] f(T, T, list(int)).

If I write

	:- subtype s < t ---> f(_, _, non_empty_list(int)).
or
	:- subtype s < t ---> f(_T1, _T2, non_empty_list(int)).

then the body of the subtype definition is not really a subtype of
the original type definition, since the original definition has
the constraint _T1 = _T2 which is not present in the subtype
definition.

If that is allowed, then is it allowed to write e.g.

	:- type t ---> f(int, list(int)).
	:- subtype s < t ---> f(_, non_empty_list(int)).

i.e. to use `_' in the subtype where a concrete type such as `int'
is used in the supertype?  If not, this seems inconsistent with
the treatment of existential types and type class constraints.

I think we should make a decision as to whether

	(1) subtypes should implicitly inherit all the properties of the
	    supertype (with the actual subtype this being defined as the
	    intersection of the supertype with the constraints imposed by
	    the body of the subtype definition)
	    
or
	    
	(2) subtypes bodies are required to be an actual subtype of
	    the supertype.

(1) allows for more concise source code.
(2) means that the set of values which satisfy a subtype declaration
    can be understood directly without needing to reference the supertype
    definition.

If we go with (1), then examples like the ones I gave above should be allowed.
If we go with (2), then subtype declarations would be allowed to contain
existential types and type class constraints (which would be required
to match that in the main type).

[to be continued]

-- 
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.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------