[m-rev.] for review: draft documentation for proposed subtypes

[Peter Wang]

Hi,

Here is an initial attempt at the documentation
for the subtypes feature that I proposed on m-dev.

Peter


diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 2c3ad70f9..c7b5ae90d 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -99,6 +99,7 @@ into another language, under the above conditions for modified versions.
 * Type classes::      Constrained polymorphism.
 * Existential types:: Support for data abstraction and heterogeneous
                       collections.
+* Type conversions::  Converting between subtypes and supertypes.
 * Exception handling:: Catching exceptions to recover from exceptional
                       situations.
 * Semantics::         Declarative and operational semantics of Mercury
@@ -1638,6 +1639,7 @@ or an explicit type qualification.
 * Lambda expressions::
 * Higher-order function applications::
 * Explicit type qualification::
+* Type conversion expressions::
 @end menu

 @node Data-functors
@@ -1968,6 +1970,19 @@ or equivalently, as it is more commonly written,
 @var{Term} `with_type` @var{Type}
 @end example

+ at node Type conversion expressions
+ at subsection Type conversion expressions
+
+A type conversion expression is a term of the form:
+
+ at example
+coerce(Term)
+ at end example
+
+ at var{Term} must be a valid data-term.
+
+ at xref{Type conversions}.
+
 @node Variable scoping
 @section Variable scoping

@@ -2274,6 +2289,7 @@ There are several categories of derived types:
 * Discriminated unions::
 * Equivalence types::
 * Abstract types::
+* Subtypes::
 @end menu

 @node Discriminated unions
@@ -2492,6 +2508,220 @@ named in the interface section of the module.
 Abstract types may be defined as either discriminated union types
 or as equivalence types.

+ at c -----------------------------------------------------------------------
+
+ at node Subtypes
+ at subsection Subtypes
+
+A subtype is a discriminated union type
+that is a subset of a supertype,
+in that every term of a subtype is a valid term in the supertype.
+It is possible to convert terms between subtype and supertype
+using type conversion expressions (@pxref{Type conversions}).
+
+A subtype is defined using the form
+ at example
+:- type @var{subtype} =< @var{supertype} ---> @var{body}.
+ at end example
+
+ at var{subtype} must be a name term
+whose arguments (if any) are distinct variables.
+
+ at var{supertype} must specify a discriminated union type
+(after expanding out equivalence types),
+whose definition is visible in the module section
+in which the subtype definition occurs.
+ at c If the subtype definition occurs
+ at c in the interface section of a module @samp{M},
+ at c then the supertype must be defined in the interface section of @samp{M}
+ at c or in a module imported in the interface section of @samp{M}.
+ at c If the subtype definition occurs
+ at c in the implementation section of a module @samp{M},
+ at c then the supertype must be defined in @samp{M}
+ at c or in the interface section of a module imported by @samp{M}.
+
+The supertype may itself be a subtype.
+Following the chain of visible subtype definitions,
+it must be possible to arrive at a @emph{base type},
+which is not a subtype.
+
+The arguments of
+ at c the top-level functor of
+ at var{supertype} (if any)
+must be variables or types.
+
+The @var{body} term is defined as
+a sequence of constructor definitions separated by semicolons.
+Any universally quantified type variable that occurs in @var{body}
+must occur in @var{subtype}.
+Any variable that occurs in @var{subtype}
+must occur in @var{supertype}.
+
+The constructor definitions must be a
+ at c non-strict
+subset of the constructors of the supertype.
+If the supertype @samp{t} has constructor @samp{f(T1, ..., Tn)} then
+a subtype @samp{s =< t} may have a constructor @samp{f(S1, ..., Sn)}.
+ at c say arguments are optional?
+For each @samp{Si} that is not an existential quantified type variable,
+it must be that @samp{Si =< Ti}.
+
+(In the following discussion,
+assume that equivalence types are expanded out
+as required.)
+
+ at samp{S =< T} holds
+if @samp{S = f(S1, ..., Sn)}
+and @samp{T = f(T1, ..., Tn)} and
+for each pair of corresponding arguments @samp{Si =< Ti}.
+
+Otherwise, @samp{S =< T} holds
+if @samp{S = f(S1, ..., Sn)}
+and there is a visible definition @w{@samp{:- type f(R1, ..., Rn) =< U}},
+and for each pair of corresponding arguments @w{@samp{Si = Ri}} (unification),
+and @samp{U =< T}.
+
+ at c e.g.
+ at c Is ne_foo =< list(T) ?
+ at c
+ at c Use definition
+ at c
+ at c      :- type ne_foo =< ne_list(foo)
+ at c
+ at c Unify ne_foo = ne_foo. Then is ne_list(foo) =< list(T) ?
+ at c
+ at c Use definition
+ at c
+ at c      :- type ne_list(T) =< list(T)
+ at c
+ at c Unify ne_list(foo) = ne_list(T) ===> T = foo
+ at c
+ at c Is list(foo) =< list(foo) ? Yes.
+
+ at samp{P =< Q} holds for two higher order types @samp{P} and @samp{Q}
+iff the following hold:
+
+ at enumerate
+ at item
+ at samp{P} and @samp{Q} are both @samp{pred} types with the same arity, or
+ at samp{P} and @samp{Q} are both @samp{func} types with the same arity
+
+ at item
+ at samp{P} and @samp{Q} both lack inst information, or
+ at samp{P} and @samp{Q} both have inst information
+
+ at item
+If @samp{P} and @samp{Q} both lack inst information then
+
+ at itemize @bullet
+ at item
+For corresponding arguments @samp{Pi} in @samp{P}
+and @samp{Qi} in @samp{Q}:
+
+ at itemize @bullet
+ at item
+ at samp{Pi = Qi}
+ at c invariant
+ at end itemize
+ at end itemize
+
+ at item
+If @samp{P} and @samp{Q} both have inst information then
+
+ at itemize @bullet
+ at item
+ at samp{P} and @samp{Q} have the same determinism category
+
+ at item
+ at samp{P} and @samp{Q} have equivalent modes for each argument
+ at c could probably be relaxed but keep it simple
+
+ at item
+For corresponding argument types @samp{Pi} in @samp{P}
+and @samp{Qi} in @samp{Q}:
+
+ at itemize @bullet
+ at item
+ at c XXX input and output modes are not defined anywhere
+if the argument has an input mode then @samp{Pi >= Qi}
+ at c contravariant
+
+ at item
+if the argument has an output mode then @samp{Pi =< Qi}
+ at c covariant
+ at end itemize
+
+ at end itemize
+
+ at end enumerate
+
+Let @samp{ExistQVarsS} and @samp{ExistQVarsT} be the set of
+existentially quantified type variables
+of the subtype constructor and supertype constructor, respectively.
+There must exist a substitution @samp{Subn} such that
+ at samp{Subn(ExistQVarsS) = ExistQVarsT}.
+For every @samp{Si} in the subtype constructor @samp{f(S1, ..., Sn)}
+that is an existentially quantified type variable,
+it must be that @samp{Subn(Si) = Ti}.
+ at c we just want existentially typed args to appear in the same
+ at c positions in the subtype and supertype
+
+Any existential class constraints on the supertype constructor
+must be repeated on the subtype constructor.
+The subtype constructor cannot add or remove any
+existential class constraints.
+
+Examples:
+
+ at example
+:- type list(T)
+    --->    []
+    ;       [T | 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_foo
+    --->    none
+    ;       some [T] foo(T) => fooable(T).
+
+:- type foo =< maybe_foo
+    --->    some [T] foo(T) => fooable(T).
+
+:- type task
+   --->     create(pred(int::in, io::di, uo::uo) is det)
+   ;        delete(pred(int::in, io::di, io::uo) is det).
+
+:- type create_task =< task
+   --->     create(pred(int::in, io::di, uo::uo) is det).
+ at end example
+
+A subtype may be exported as an abstract type
+by declaring only the name of the subtype in the
+interface section of a module (without the @samp{=< @var{supertype}} part).
+Then the subtype definition must be given in the implementation section of
+the same module.
+
+Example:
+
+ at example
+:- interface.
+
+:- type non_empty_list(T).  % abstract type
+
+:- implementation.
+
+:- import list.
+
+:- type non_empty_list(T) =< list(T)
+    --->    [T | list(T)].
+ at end example
+
+ at c -----------------------------------------------------------------------
+
 @node Predicate and function type declarations
 @section Predicate and function type declarations

@@ -6918,6 +7148,122 @@ good_example3_univ("foo"::in(bound("foo")), univ(42)::out).
 good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).
 @end example

+ at c -----------------------------------------------------------------------
+
+ at node Type conversions
+ at chapter Type conversions
+
+A term of type @samp{T1} may be converted to type @samp{T2}
+using a type conversion expression:
+
+ at example
+coerce(Term)
+ at end example
+
+ at c XXX disallow coerce/1 as a constructor name?
+
+If @var{Term} has type @samp{T1} and the expression has type @samp{T2},
+the coercion is type-correct iff
+ at samp{T1} and @samp{T2} are equivalent after
+expanding out equivalence types
+and replacing any subtypes with their base types
+(@pxref{Subtypes}).
+
+For example, if there is a subtype @samp{s =< t} and
+a subtype @samp{non_empty_list(T) =< list(T)}
+then coercions between these pairs of types are type-correct:
+
+ at example
+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)
+ at end example
+
+If a subtype definition is not visible in the module
+in which a @samp{coerce} operation occurs,
+then the coercion is type-incorrect.
+
+Coercions must also be mode-correct.
+For a coercion where:
+
+ at itemize @bullet
+ at item
+the input is @samp{X} with type @samp{s}
+
+ at item
+the result is @samp{Y} with type @samp{t}
+
+ at item
+ at samp{Xi}, @samp{Xf} are the initial and final insts of @samp{X}
+
+ at item
+ at samp{Yi}, @samp{Yf} are the initial and final insts of @samp{Y}
+ at end itemize
+
+ at noindent
+the coercion is mode-correct iff:
+
+ at itemize @bullet
+ at item
+ at samp{Xi} is a ground inst
+
+ at item
+ at samp{Xf = Xi}
+
+ at item
+ at samp{Yi} is free
+
+ at item
+Yf is the greatest lower bound (glb) of @samp{Xi} and
+the instantiatedness tree derived from @samp{t}
+where all nodes are bound.
+The glb must exist,
+ at samp{Yf} must be be ground,
+and @samp{Yf} must be a valid inst of @samp{t}.
+ at end itemize
+
+ at c XXX partial order of insts not used elsewhere in reference manual
+
+Intuitively,
+coercing a ground term from subtype to supertype is always allowed,
+but coercion from supertype to subtype is allowed only if
+the term is approximated by an inst that indicates
+the term would be a valid in the subtype.
+
+Examples:
+
+ at example
+:- type fruit
+    --->    apple
+    ;       lemon
+    ;       orange.
+
+:- type citrus =< fruit
+    --->    lemon
+    ;       orange.
+
+:- inst citrus for fruit/0
+    --->    lemon
+    ;       orange.
+
+:- func f1(citrus) = fruit.
+
+f1(X) = coerce(X).  % correct
+
+:- func f2(fruit) = citrus.
+
+f2(X) = coerce(X).  % not mode-correct
+
+:- func f3(fruit) = citrus.
+:- mode f3(in(citrus)) = out is det.
+
+f3(X) = coerce(X).  % correct
+ at end example
+
+ at c -----------------------------------------------------------------------
+
 @node Exception handling
 @chapter Exception handling