diff --git a/doc/mercury_reference_manual.texi b/doc/mercury_reference_manual.texi index ebed23b19..357e95d79 100644 --- a/doc/mercury_reference_manual.texi +++ b/doc/mercury_reference_manual.texi @@ -3298,7 +3298,7 @@ or as equivalence types. @node Subtypes @subsection Subtypes -(This is a new and experimental feature, subject to change.) +(This is a relatively new feature, and is subject to change.) A subtype is a discriminated union type that is a subset of a supertype, @@ -3309,7 +3309,8 @@ using type conversion expressions (@pxref{Type conversions}). As previously described, the syntax for non-subtype discriminated union types is @example -:- type @var{type} ---> @var{body}. +:- type @var{type} + ---> @var{body} @end example where @var{type} is the name of a type constructor applied to zero or more distinct type variables @@ -3321,7 +3322,8 @@ must be among @var{type}'s parameters. The syntax for subtypes is similar but slightly different: @example -:- type @var{subtype} =< @var{supertype} ---> @var{body}. +:- type @var{subtype} =< @var{supertype} + ---> @var{body}. @end example Since a subtype is also a discriminated union type, the rules for discriminated union types apply to them as well: @@ -3344,10 +3346,12 @@ by normal module visibility rules. The discriminated union type specified by @var{supertype} may itself be a subtype. -Following the chain of subtype definitions, +Following the chain of subtype-to-supertype links, it must be possible to arrive at a @emph{base type}, which is a discriminated union type but @emph{not} a subtype. +@heading Differences between subtype and supertype + The body of the subtype may differ from the body of its supertype in two ways. @itemize @bullet @item @@ -3421,6 +3425,50 @@ that does not occur in @var{supertype}. @c There should be some discussion here @c of the possible uses of this flexibility. +@c I (zs) can't think of any such uses that wouldn't be better expressed +@c using simple equivalence type definitions, such as +@c +@c :- type self_map(T) == map(T, T). +@c +@c for duplicating type parameters in the supertype, or +@c +@c :- type multi_map(K, V) == map(K, list(V)). +@c +@c for introducing type constructors into the supertype. +@c +@c As for phantom parameters in the subtype, adding them to the supertype +@c should work as well. + +@heading Lifting a subtype + +If type @samp{S} has the form @samp{S = f(S1, ..., Sn)} +and there is a visible subtype definition starting with +@w{@samp{:- type f(RP1, ..., RPn) =< U}}, +then we define @samp{lift(S)} as the type that results from +replacing all occurrences of each @samp{RPi} in @samp{U} +with the corresponding @samp{Si}. + +Since the sypertype U in that subtype definition +must have the form of a type constructor +applied to zero or more argument types, +the result of the substitution must also have the same form. +If the supertype's type constructor is also a subtype, +then lifting may be applied to it as well. + +We define @samp{lift_to(f, n, S)} as +@itemize @bullet +@item +@samp{S}, if the principal type constructor of @samp{S} is @samp{f/n}; +@item +@samp{lift_to(f, n, lift(S))}, +if the principal type constructor of @samp{S} is not @samp{f/n}, +but that principal type constructor does have a visible subtype definition; and +@item +@samp{S}, otherwise. +@end itemize + +@heading The subtype relation + (In the following discussion, we assume that all equivalence types have been expanded out.) @@ -3456,8 +3504,34 @@ and if @samp{S = f(S1, ..., Sn)}, @samp{S =< T} holds if In other words, if all occurrences of @var{Ri} in @var{U} are replaced by the corresponding @var{Si} to give @var{Usub}, then @samp{Usub =< T} must hold. +This is alternative 1. + +XXX We could replace the second item @emph{either} with just: + +If @samp{S} and @samp{T} have different principal type constructors, +@samp{S =< T} holds if @samp{lift(S) =< T}. +This is alternative 2. + +@emph{or} with + +If @samp{S} and @samp{T} have different principal type constructors, +say @samp{s/n} and @samp{t/m} respectively, +@samp{S =< T} holds if @samp{lift_to(t, m, S) =< T}. +This is alternative 3. + +Only the latter would require defining lift_to above, +but I think it would be easier for people to understand, +since it makes explicit the iteration involved. + @end itemize +And we could express the entire subtype test as just +the first item @emph{after} trying to lift S to the same typector as T. +This is alternative 4. + +Which of these four alternatives do people prefer? +I (zs) prefer #4. + @noindent 2. For two tuple types @samp{S = @{S1, ..., Sn@}} and @samp{T = @{T1, ..., Tn@}}, @@ -3488,6 +3562,7 @@ if and only if all of the following conditions hold: @var{P} and @var{Q} have the same argument types (the current implementation does not allow subtyping in higher-order arguments), and + @c XXX say why: which args are input will depend on modes @item if either of @var{P} and @var{Q} has higher-order inst information, then @var{P} and @var{Q} must have @@ -3496,6 +3571,9 @@ if and only if all of the following conditions hold: the same argument modes, determinism, and purity. @end itemize @end itemize +@c XXX I (zs) do not see how this differs from +@c requiring P and Q to be identical. +@c If there *is* a difference, we should use S and T, not P and Q. @noindent 4. For all other types, @@ -8507,7 +8585,7 @@ good_example3_univ("bar"::in(bound("bar")), univ("blah")::out). @node Type conversions @chapter Type conversions -(This is a new and experimental feature, subject to change.) +(This is a relatively new feature, and is subject to change.) A term may be converted from one type @var{FromType} to another type @var{ToType} @@ -8520,39 +8598,76 @@ coerce(@var{Term}) The expression is type-correct if and only if @var{FromType} and @var{ToType} are both discriminated union types, and after replacing the principal type constructors with base types +@c XXX This reads like a category error: +@c you replace a type_ctor with another type_ctor, +@c or a type_ctor with another type; +@c you do not replace a type_ctor with a complete type. (@pxref{Subtypes}) the two types have the same type constructor, and the arguments of the common type constructor satisfy the type parameter variance restrictions below. +The expression is type-correct if and only if +@var{FromType} and @var{ToType} are both discriminated union types, +and, after replacing each of their principal type constructors +with their base type constructors, +@itemize @bullet +@item +the resulting types have the @emph{same} principal type constructor, and +@item +the arguments of that principal type constructor +satisfy the type parameter variance restrictions below. +@end itemize + Let @var{FromType} expand out to @samp{base(S1, ..., Sn)} +@c XXX In the subtype section, we use "expand" only in the sense of +@c expanding out equivalence types. Here, we also include replacing each +@c subtype with its supertype, using the head of the subtype's definition. +@c Do we have a specific name for that operation? +@c If not, *should* we give it a name? and @var{ToType} expand out to @samp{base(T1, ..., Tn)}, where @samp{base(B1, ..., Bn)} is the common base type, and @var{Bi} is the i'th type parameter, which is bound to @var{Si} in @var{FromType} and @var{Ti} in @var{ToType}. +@c XXX Wouldn't Fi be better notation than Si? +@c Si would make sense if we talked about source types, but +@c we call them about from-types. +@c XXX And wouldn't BPi be better notation than just Bi? +@c It would clarify that BPi are type parameters, i.e. type variables, +@c while the Si/Fi/Ti are complete types. For each pair of corresponding type arguments, one of the following must be true: @itemize @item -@samp{Si = Ti} -if the two types are the same +@samp{Si = Ti}, +meaning the two types are the same @item -@samp{Si < Ti} -if @var{Si} is a subtype of @var{Ti} +@samp{Si < Ti}, +meaning @var{Si} is a subtype of @var{Ti} by the relation below @item -@samp{Ti < Si} -if @var{Ti} is a subtype of @var{Si} +@samp{Ti < Si}, +meaning @var{Ti} is a subtype of @var{Si} by the relation below @end itemize -Otherwise, the @code{coerce} expression is not type-correct. +If none of the above is true, i.e.@: if @samp{Si} and @samp{Ti} are not related. +then the @code{coerce} expression is not type-correct. @c NOTE: we deliberately disallow coercion between arbitrary phantom types. +@c I wouild approach the above by +@c - first defining the @samp{S =< T} relation, +@c - defining four categories (2x2) based on whether S=