<html xmlns="http://www.w3.org/1999/xhtml"> <head> <title></title> </head> <body> <div name="messageBodySection"> <div dir="auto">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.</div> </div> <div name="messageReplySection">On Jan 13, 2021, 5:56 PM -0800, Peter Wang <novalazy@gmail.com>, wrote: <blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">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@lists.mercurylang.org https://lists.mercurylang.org/listinfo/developers </blockquote> </div> </body> </html>