[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:
> > +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?

That remark shouldn't be there; I'll remove it.

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

Ok.

> 
> > +The only subtype of a universally quantified type variable
> > +is the variable itself,
> 
> What about the empty subtype (the one with inst "not_reached")?

I didn't think of that.  If there is a way to express the empty subtype,
then this would also be allowed as the subtype of a universal type.

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

That is likely to have the same problems as using a subtype on the RHS of
a `with_type` qualifier.  I have an alternative proposal that will allow us
to achieve the same effect, but I'm going to get some lunch very soon
so I'll have to explain that later.

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

That would allow the users to attempt to use abstract subtypes, since
they can define an abstract equivalence type that uses a subtype in the
implementation.  Maybe we can let them do that provided we warn them about
any limitations on the current implementation, but in this first version
of subtypes I'd rather sacrifice some flexibility than have parts of the
specification be a little hazy.  We can add more flexibility later.

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