[m-dev.] subtypes proposal
novalazy at gmail.com
Wed Jan 20 11:03:04 AEDT 2021
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,
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
:- type foo.
:- 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
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.
More information about the developers