[m-dev.] subtypes proposal

[Julien Fischer]

Hi Peter,

What's the motivation for bringing this up again?

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.

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

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

> Type conversions
> ----------------
>
> I propose to not introduce any implicit conversion between subtypes and
> supertypes, for a few reasons:
>
>  - there are no implicit type conversions anywhere else in the language
>  - explicit conversions may be easier to understand
>  - I do not want to set myself up to potentially rewrite the type
>    checker ;)
>
> Rather, terms can be coerced between subtype and supertype with an
> explicit operation, say, written like a function call:
>
>    Y = coerce(X)
>
> A coercion from FromType to ToType is type correct if FromType and ToType
> are equivalent after replacing any subtypes with their base types.
>
> For example, if s =< t and non_empty_list(T) =< list(T) then coercions
> between these pairs of types should be accepted by the type checker:
>
>    s <-> t
>    list(s) <-> list(t)
>    non_empty_list(s) <-> non_empty_list(t)
>    list(s) <-> non_empty_list(s)
>    list(s) <-> non_empty_list(t)
>
> Coercions must be mode correct.
> Assume we have a coercion of X:s to Y:t.
> If Xi, Xf, Yi, Yf are the initial and final insts of X and Y
> then the coercion is mode correct iff:
>
>  - Xi is a ground inst (no partial instantiation, no uniqueness)
>
>  - Xf = Xi
>
>  - Yi is free
>
>  - Yf is the glb of Xi and the instantiatedness tree derived from t
>    where all nodes are bound.
>    The glb must exist,
>    Yf must be be ground,
>    and Yf must be a valid inst of t.
>
> Coercing a ground term from subtype to supertype is always allowed.
> We use the mode system to ensure that a coercion from supertype to
> subtype is safe at compile time.
>
> It would probably be useful to also provide a semidet coercion operation
> that can fail at runtime if the term is not valid for the result type.
>
>
> 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.

> Comparison to previous proposal
> -------------------------------
>
> Compared to Fergus's 1998 proposal
> (http://lists.mercurylang.org/pipermail/developers/1998-February/002274.html)
> the "subtypes" in this proposal works with polymorphically typed
> (but non polymorphically moded) predicates and containers in a
> straightforward way, without constrained polymorphic modes.
>
> I think the declarations of the form
>>
> would have been most useful to provide an inst for a higher order Type,
> but we have a different feature to handle that now.

For everyone's reference, further archived discussion of subtyping over
the years:

http://lists.mercurylang.org/archives/reviews/2002-November/004675.html
http://lists.mercurylang.org/archives/developers/2002-November/002285.html
http://lists.mercurylang.org/archives/developers/2002-December/012963.html

Julien.