[m-dev.] subtypes proposal

[Fastmail]

Hello,

I do not have any direct feedback about the details of this proposal, but I did want to chime in to say that this feature would be extremely helpful for simplifying a code base that I am working on.
On Jan 13, 2021, 5:56 PM -0800, 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.
>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/developers/attachments/20210114/fb3cc9d2/attachment-0001.html>