[m-dev.] subtypes proposal
mark at mercurylang.org
Tue Jan 19 23:39:55 AEDT 2021
On Thu, Jan 14, 2021 at 12:55 PM Peter Wang <novalazy at gmail.com> 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.
> 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.
> :- 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
> 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?
> 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.)
> developers mailing list
> developers at lists.mercurylang.org
More information about the developers