[m-dev.] subtypes proposal

[Peter Wang]

On Tue, 19 Jan 2021 17:24:22 +1100 Julien Fischer <jfischer at opturion.com> wrote:
> 
> Hi Peter,
> 
> What's the motivation for bringing this up again?
> 

I've wanted some sort of subtyping feature before, this idea seems
relatively easy to implement, and I probably have time to implement it.

> On Thu, 14 Jan 2021, Peter Wang wrote:
> 
> > In this proposal, subtypes are distinct d.u. types that share a data
> > representation with a base type, which is a normal d.u. type.
> > Subtypes of subtypes are allowed.
> > Every term of a given subtype must also be valid term in the supertype
> > (recursively, up to the base type), with the same data representation.
> >
> > A subtype can be introduced like this:
> >
> >    :- type SUBTYPE =< SUPERTYPE
> >        --->    BODY.
> 
> I would be inclined to retain the ':- subtype' declaration of
> the original subtypes proposal.
> 

':- subtype' in the original proposal makes sense as it introduces a
sort of type synonym, and the body of the declaration was an inst,
not constructors.

I preferred ':- type' in this proposal as it really does introduce a new
d.u. type. The only difference from the programmer's point of view is
that it enables coercions between types that share a base type.

If an type is abstractly exported, the fact that it is a subtype of some
other type should not be visible to the user. The user of a module
should see

    :- type foo.

instead of

    :- subtype foo.

in the module interface.
(Assuming we won't mix ':- type' and ':- subtype'.)

> > The constructor definitions in BODY must be a (non-strict) subset of the
> > constructors of the supertype. If the supertype t has constructor
> > f(T1, ..., Tn) then a subtype s =< t may have a constructor
> > f(S1, ..., Sn) such that Si =< Ti.
> >
> > TODO: requires further thought
> >
> >  - higher order types can have inst constraints now
> >  - existential class constraints must match exactly?
> 
> The existentially quantified variables in the subtype should definitely
> be at least as constrained as they are in the supertype.  The question
> is: can they be more constrained in the subtype?  Personally, I cannot
> see any utility in allowing that.  Also, if subtypes were allowed to be
> more constrained, then supertype -> subtype coercions could not in
> general be checked at compile time and the runtime checks would require
> runtime type class membership tests to be implemented.

Right, I agree.

> 
> > Any type variable that occurs in SUBTYPE must also occur in SUPERTYPE.
> > Any universally quantified type variable that occurs in BODY
> > must also occur in SUBTYPE.
> >
> > Examples:
> >
> >    :- type empty_list =< list(T)
> >        --->    [].
> >
> >    :- type non_empty_list(T) =< list(T)
> >        --->    [T | list(T)].
> >
> >    :- type non_empty_list_of_foo =< list(foo)
> >        --->    [foo | list(foo)].
> >
> >    :- type maybe_univ
> >        --->    none
> >        ;       some [T] univ(T).
> >
> >    :- type yes_univ =< maybe_univ
> >        --->    some [T] univ(T).
> 
> Do any existential class constraints have to be repeated in the subtype
> declaration?
> 

Yes. I don't see why we should allow them to be omitted.

> > Interaction with modules
> > ------------------------
> >
> > The compiler needs to know the definition of the base type in order to
> > construct, deconstruct and coerce terms of a subtype.
> >
> > If a subtype is defined in the interface section of a module M
> > then its supertype must either
> >
> > - be defined in the interface section of M, or
> > - be defined in a module imported in the interface section of M.
> >
> > If a subtype is defined in the implementation section of a module M,
> > then its supertype must either
> >
> >  - be defined in M, or
> >  - be defined in the interface section of a module imported by M.
> >
> > A subtype may be abstractly exported, like other d.u. types.
> > Coercions to/from the subtype cannot be checked in modules without
> > visibility of the subtype definition (and its supertype),
> > and will be rejected at compile time.
> 
> In the case where there is an abstract type and an abstract subtype and
> it makes sense for the to be an "abstract coercion", the programmer can
> easily export such an operation, so I don't see this as a restriction.

Right.

Peter