[m-rev.] for discussion: subtypes documentation

[Mark Brown]

On 25-Nov-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 24-Nov-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:

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

Ok; I suspected you might consider that an abuse of terminology.

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

The insts that are derived by propagating subtype information can be
expressed as valid Mercury insts, so users can write them by hand if they
want to even without using subtype declarations.  However, the existing
documentation explaining how to do this is, at best, subtle, so a rewrite
of the Modes chapter along the lines you suggested should also fix this
problem.

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

That is just a piece of shorthand that indicates the base inst should be
ground.  From the original proposal:

| Any "don't care" (underscore) variables in `Functors' are
| replaced with `ground'.

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

Ok.  The parenthetical remark should have read "(i.e., variables whose name
is @code{_})".

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

Yes, that is not a circularity in the sense that I mean.  Here is a better
definition:

A "circularity" in the subtype definitions is a sequence of types
S_1, T_1, ..., S_n, T_n, such that

	1) For 1 =< i =< n, there is a subtype declaration of the form

		:- subtype S_i < T_i ---> ...

	2) For 1 =< i < n, some instance of S_i+1 occurs in T_i.

	3) Some instance of S_1 occurs in T_n.

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

Well, the original definition constrains the first two arguments of f/3
to have the same type, but the same inst?  I'm not really sure.  I think
the crucial decision is the one you mention below ...

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

Yes.

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

Incidentally, how do I write an inst that covers some constructor
containing existentially type data?  If I had the type

	:- type foo
		--->	some [T] (f(T) => c(T))
		;	g(int).

how would I write the inst that covers only elements of foo whose top
functor is f/1?

Cheers,
Mark.

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