[m-rev.] for discussion: subtypes documentation

[Ralph Becket]

Mark Brown, Sunday, 24 November 2002:
> 
> Index: reference_manual.texi
> ===================================================================
> +
> + 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,

Can we standardize on "inst tree" rather than "instantiatedness tree" in
the documentation?  It's a technical term so we're free to define and
use it as we will.

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

I'm with David on this one: I find the symbolic, (partial-)order based
definition easier to understand.

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

Are we currently allowing `with_inst` as a synonym for `::'?  I think
we should for the time being.

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

That seems a little odd to me.  Wouldn't one have to explicitly
existentially quantify such variables in the body?

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

A symbolic explanation would make this clearer and perhaps make the
verbal description unnecessary.

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

I'm not sure I like this one - when I look at a subtype definition, I
don't want to also have to look at the supertype to work out whether a
particular argument is existentially quantified (or is that the
motivation for allowing anonymous variables in the body?)

> + at node Semantics of Mercury programs with subtypes
> + at section Semantics of Mercury programs with subtypes

This whole section would be clearer with some more formal, symbolic
description/definition.

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