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

Julien Fischer jfischer at opturion.com
Tue Feb 16 14:38:39 AEDT 2021


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

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

> -----
>
> This is the first step towards implementing a subtypes feature.
> It introduces type definitions of the form
>
>    :- type subtype =< supertype ---> body.
>
> Later, terms of a subtype should share a data representation with their
> supertype, and it will be possible to convert terms between two types
> that share "base types" using a coerce operation.
>
> 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.  That last one needs to be listed in
the NEWS file as a possible breaking change.

...

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

> Note that excessive overloading of constructors
> can slow down type checking
> and can make the program confusing for human readers,

...

> @node Exception handling
> @chapter Exception handling
> 
> @@ -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?

...

> diff --git a/tests/invalid/subtype_circular.err_exp b/tests/invalid/subtype_circular.err_exp
> new file mode 100644
> index 000000000..c732bdf4d
> --- /dev/null
> +++ b/tests/invalid/subtype_circular.err_exp
> @@ -0,0 +1,3 @@
> +subtype_circular.m:008: Error: circularity in subtype definition.
> +subtype_circular.m:011: Error: circularity in subtype definition.
> +subtype_circular.m:014: Error: circularity in subtype definition.

Not essential for now, but it would be nice if a verbose version of this
message listed the types involved in the cicularity.

...

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

> +
> +:- type s2 =< {}
> +    --->    s.
> +
> +:- type s3 =< (func(int) = int)
> +    --->    s.
> +
> +:- type s4 =< (pred)
> +    --->    s.
> +
> +:- type s5 =< undefined
> +    --->    s.
> +
> +:- type s6 =< t(1, 2)
> +    --->    s.

Julien.


More information about the reviews mailing list