[m-rev.] for review: Parse and check subtype definitions.

[Peter Wang]

On Tue, 16 Feb 2021 14:38:39 +1100 Julien Fischer <jfischer at opturion.com> wrote:
> 
> Hi Peter,
> 
> On Mon, 15 Feb 2021, Peter Wang wrote:
> 
> > (Note that I changed the documentation a fair bit since I originally
> > posted it.)
> 
> A couple of questions:
> 
> How are equality and comparison defined for subtypes?  In particular,
> what happens if the supertype has user-defined equality or comparison?
> 
> I guess the simplest thing would be to say that user-defined equality
> and comparison do not carry over to the subtypes.  OTOH, since the
> representations are the same you could implement unification and
> comparison for subtypes by:
> 
>      unify_subtype(X, Y) :-
>          unify_supertype(coerce(X), coerce(Y)).
> 
> and similarly for comparison.  (Also, it seems semantically weird for
> subtype not to have the same equality and comparison operation as the
> supertype.)
> 

There is nothing special about subtypes in this respect.
We could do something later if it's deemed necessary.

> How do subtypes and the type class system interact?  Is a subtype
> automatically an instance of a type class if its super class is?  (I
> guess the answer in this design is no, you need to add an explicit
> coercion to the base class in any method call -- if so, that point needs
> to be mentioned in the reference manual.)
> 

Right, subtypes have no special interaction with the type class system.
I'll add something to the documentation.

> > doc/reference_manual.texi:
> >    Add documentation for subtypes.
> >
> >    Add documentation for a proposed `coerce' operation, commented out
> >    for now.
> >
> >    Add "=<" to the list of reserved type names.
> 
> If you are intending to commit this to the trunk then all of the new
> doucumentation should be commited out for now with the exception of of
> "=<" being a reserved type name.

Subtype definitions do work as described. What if I just write at the
top of the section:

    (This is a new and experimental feature, subject to change.)

> That last one needs to be listed in
> the NEWS file as a possible breaking change.
> 
> ...

Will do.

> 
> > diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> > index 2c3ad70f9..894707b39 100644
> > --- a/doc/reference_manual.texi
> > +++ b/doc/reference_manual.texi
> > 
> > @@ -2274,6 +2289,7 @@ There are several categories of derived types:
> > * Discriminated unions::
> > * Equivalence types::
> > * Abstract types::
> > +* Subtypes::
> > @end menu
> > 
> > @node Discriminated unions
> > @@ -2379,6 +2395,7 @@ with the same name, arity, and result type in the same module.
> > (There is no particularly good reason for this restriction;
> > in the future we may allow several such functors
> > as long as they have different argument types.)
> > + at c That would likely conflict with subtypes.
> 
> In what way?

Reading it again, I'm not sure what that would allow that we don't
already allow.

> > @@ -8101,13 +8372,21 @@ using a declaration of the form
> > This defines @var{MercuryTypeName}
> > as a synonym for type @var{ForeignTypeDescriptor}
> > defined in the foreign language @var{Lang}.
> > -You must declare @var{MercuryTypeName}
> > -using a (possibly abstract) @samp{:- type} declaration as usual.
> > + at c You must declare @var{MercuryTypeName}
> > + at c using a (possibly abstract) @samp{:- type} declaration as usual.
> > + at var{MercuryTypeName} must be the name of an abstract type,
> > +or the name of a discriminated union type that is not a subtype.
> > +In both cases,
> > + at var{MercuryTypeName} must be declared with @samp{:- type} as usual.
> > The @samp{pragma foreign_type} must not have wider visibility
> > than the type declaration
> > (if the @samp{pragma foreign_type} declaration is in the interface,
> > the @samp{:- type} declaration must be also).
> > 
> > +The type named by @var{MercuryTypeName}
> > +cannot be the base type of any subtypes (@pxref{Subtypes}).
> > + at c XXX how can we check this?
> 
> Do we hang on to all the type definitions these days?  Or do
> we only retain the one needed by the target backend?
> 

I'll delete that XXX; I managed to check it in the end.

> > diff --git a/tests/invalid/subtype_invalid_supertype.m b/tests/invalid/subtype_invalid_supertype.m
> > new file mode 100644
> > index 000000000..3e8a1cb5b
> > --- /dev/null
> > +++ b/tests/invalid/subtype_invalid_supertype.m
> > @@ -0,0 +1,24 @@
> > +%---------------------------------------------------------------------------%
> > +% vim: ts=4 sw=4 et ft=mercury
> > +%---------------------------------------------------------------------------%
> > +
> > +:- module subtype_invalid_supertype.
> > +:- interface.
> > +
> > +:- type s1 =< int
> > +    --->    s.
> 
> You should check every builtin type here.  (In the past, the compiler's
> handling of builtin types has been far from thorough in spots, it should be
> better now, but ...)
> 

Will do.

Peter