[m-rev.] for discussion: subtypes documentation

[David Overton]

On Sun, Nov 24, 2002 at 10:36:55PM +1100, Mark Brown wrote:
> Hi,
> 
> 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.
> 
> 	- 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.

I've used a different approach to describing this sort of stuff in my
thesis.  I define a couple of partial order relations on insts and use
them to describe most of the other relationships and operations on
insts.  You may get some ideas there.  For example, it would allow you
to describe the propagation of base insts into modes as simply taking
the least upper bound.

You can see the latest draft by checking it out of the cvs repository at
`~dmo/repository/thesis'.  See chapters 3 and 4 in particular.

Of course, this would not fit in with the rest of the stuff in the modes
section of the manual so it would probably require rewriting a fair bit
of that which you may or may not choose to do.

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

What does it mean for anonymous type variables to appear in the body?
Ah, okay I see you explain this in the semantics section.  I found it a
bit confusing the first time I read this though.  I re-read it a couple
of times to make sure that it really is what you were saying.

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

Do the values have to be a _strict_ subset?  If not, then it might be
better to use '=<' rather than '<'.  This would also make it more
consistent with the syntax used for constrained polymorphic modes.

Also, I'm a bit concerned about the word "meant".  Is this enforced by
the compiler?

> +Existential quantifiers and class constraints are always implicitly
> +determined from the supertype, and should not be explicitly given.
> +
> + at node Semantics of Mercury programs with subtypes
> + at section Semantics of Mercury programs with subtypes
> +
> +For every subtype we define a type, the @dfn{base type},
> +which is the type used internally to represent values of the subtype,
> +and an inst, the @dfn{base inst},
> +which encompasses the subtype information about values of the subtype.
> +
> +The base type is determined by treating each subtype declaration
> +
> + at example
> +:- subtype @var{Sub} < @var{Super} ---> @var{Body}.
> + at end example
> +
> + at noindent
> +as if it is the equivalence type declaration
> +
> + at example
> +:- type @var{Sub} == @var{Super}.
> + at end example
> +
> + at noindent
> +and expanding out all of these equivalences in the usual way.
> +
> +The base inst is defined on the type tree of the base type.
> +Consider the subtype at the root or-node of the type tree:
> +
> + at itemize @bullet
> + at item
> +If it is an anonymous variable (which is allowed in subtype definitions),
> +the inst is ground.  That is, every node in the type tree maps to bound.

Ah, okay, this answers my earlier question.

> +
> + at item
> +If it is inst qualified (which is allowed in subtype definitions),
> +then the subtype information on the left hand side
> +is propagated into the inst on the right hand side
> +to form the base inst of the qualified type.
> +The propagation of a subtype into an inst is described below.

Please put in a cross-reference to the section on propagation.

> +
> + at item
> +If it is defined by a subtype declaration or a discriminated union type
> +(modulo equivalence) then the root or-node maps to bound,
> +and for each function symbol in the type or subtype definition
> +the corresponding and-node maps to bound,
> +and the children of this and-node are
> +the base insts of the arguments of the function symbol.
> +All other and-nodes (if any) map to free.
> +
> + at item
> +If it is defined by an abstract type ...
> +
> +XXX I suppose we will have to treat this as ground, which will ignore
> +any subtype information in arguments of the type.

This is a case where we want to be able to constrain abstract insts in
much the same way we constrain inst variables.  But that's a future
extension.  I would just comment this out for now.

> +
> + at item
> +If it is a pred or func type, the base inst is just the subtype itself.
> +This is not a valid Mercury inst, so attempting to use it directly
> +will result in an error.
> +However, if a base inst like this is propagated into another inst,
> +as described below, then a valid inst may result
> +and using this resulting inst would therefore not be a problem.

This sounds rather complicated.  Couldn't you just map to a base inst of
ground unless an inst qualifier is given?  I think that would work the
same when you do the propagation (provided you add a row to your
propagation table, as I've done below).

> +
> +For and-nodes, the new inst is given by the following table:
> +
> + at example
> +        base inst         existing inst       new inst
> +
> +        free              free                free
> +        bound             free                free
> +        free              bound               free
> +        bound             bound               bound

You should add

	   ground	     pred/func	 	 pred/func

Also it might be a good idea to add

	   ground	     free		 free
	   free              ground              free
	   ground	     bound		 bound
	   bound	     ground		 bound
	   ground            ground              ground

since it may not be obvious that `bound' includes `ground' insts.

> + at end example
> +

Apart from those suggestions, this look good.


David
-- 
David Overton                  Uni of Melbourne     +61 3 8344 9159
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------