[m-dev.] subtypes proposal

[Mark Brown]

Hi Peter,

On Thu, Jan 14, 2021 at 12:55 PM Peter Wang <novalazy at gmail.com> wrote:
>
> Hi,
>
> 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.
>
> 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?
>
> 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).
>
>
> 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.
>
>
> 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.

That proposal allowed you to say, for example, that reversing a
non-empty list results in a non-empty list whereas reversing a list
just gives you a list, without just writing two separate reverse
functions. Any chance of allowing something like that?

Mark

>
> I think the declarations of the form
>
>     :- subtype SubType < Type :: Inst.
>
> would have been most useful to provide an inst for a higher order Type,
> but we have a different feature to handle that now.
>
>
> I have attached a copy of a module that demonstrates what code using the
> proposed feature might look like. (Not suggesting that it would be
> better than the cord representation used in the standard library.)
>
> Peter
> _______________________________________________
> developers mailing list
> developers at lists.mercurylang.org
> https://lists.mercurylang.org/listinfo/developers