[m-rev.] for review: an updated draft of coercions in the reference manual

[Zoltan Somogyi]

On Thu, 6 Aug 2026 16:49:04 +1000, Peter Wang <novalazy at gmail.com> wrote:

> > > > +Since the sypertype @samp{U} in that subtype definition
> > > 
> > > supertype
> > 
> > The definition I am referring to is the one that occurs in the
> > prior paragraph, i.e. @samp{:- type tc(RP1, ..., RPn) =< U}}.
> > That is a subtype definition.
> 
> There was a typo: sypertype

Doh! Fixed.

> > > I would say: are related by subtyping, are in a subtyping relation,
> > > or use the =< operator defined previously.
> > 
> > I am trying to avoid using the =< operator, for two reasons.
> > First, it is maths, and match operators need a non-maths name
> > as well, and second, the obvious use of =< is S =< T, and that is NOT
> > what I am trying to specify, but rather S =< B, T =< B.
> > 
> > How about "have a common ancestor"? With the first definition
> > of the phrase explicitly saying that this means S =< B, T =< B.
> > 
> > Or would "have a shared ancestor" be better?
> 
> "Where both types are subtypes of a common base type"?

Yep, that works. Thanks.

> > However, both of those phrases describe the relations needed
> > for type conversions ONLY for du types. For the relation needed
> > for type conversions for types that are not du types but CONTAIN
> > du types, we will need an acceptable name, and I still don't have one.
> 
> Is this for an extension to tuple types?

Preparing for that, yes, though that text was just a question for you guys,
and not intended for inclusion in the refman.

> > I think even "must-be-invariant" is a bit too abstract, because
> > it is not the parameter that must be invariant, but the arg types
> > bound to it. I just cannot think of a phrase to describe all that
> > that is short enough to be useful as a name for the concept.
> 
> The terminology I have seen says the _type constructor_ is
> {in,co,contra}variant, in the context of a constructor with a single
> parameter (or, presumably, if there are multiple parameters behaving in
> the same way). Otherwise, you also see "covariant in X parameter",
> etc.

I will look into using that terminology. It does look promising.

> Calling a type parameter x-variant is a statement about the relationship
> between types substituted for that parameter on either side of the
> subtyping relation. "Must-be-invariant" is unnecessary,
> as "invariant" already expresses that.
> 
> [Sample quote from Pierce (Types and Programming Languages):
> 
>   Not all type constructors are covariant or contravariant.
>   The Ref constructor, for example, must be taken to be invariant in
>   order to preserve type safety.
> 
>   For Ref S1 to be a subtype of Ref T1, we demand that S1 and T1 be
>   equivalent under the subtype relation—each a subtype of the other.

Yes, but Pierce is talking to theorists. We are not.

> > I notice you did not say anything about solver types.
> > Does anyone know whether they can occur in du type definitions?
> > I don't.
> > 
> 
> I haven't used solver types before, but this is allowed:
> 
>   :- type vars(T)
>       --->    vars(list(eqneq(T))).
> 
> where eqneq(T) is from samples/solver_types/eqneq.m
> 
> A term containing solver types will need `any' insts to be useful,
> which would prevent the term from being coerced, since coerce requires
> the term to have a ground inst.
> 
> Putting that aside, a solver type would have the same problem as other
> mutable types. Consider if you could get two references to the same
> solver variable with two different types, e.g. eqneq(animal) and
> eqneq(dog). You could then bind the variable to 'cat' through the
> eqneq(animal) reference, then read the 'cat' back out through the
> eqneq(dog) reference.

Thanks for that. I think I will use the "any vs ground" difference as the reason
for disallowing variance in solver types, since it is easier for people to
understand.

> > > > +That is the reason for the first bullet point above.
> > > > +The reason for the second is that any data constructor argument
> > > > +whose type is recursive but does not meet the imposed condition
> > > > +(possibly because it includes the parameters in a different order)
> > > > +may create a link that says
> > > > +"if this specific parameter of @samp{base_tc} must be invariant,
> > > > +then another specific parameter must also be invariant",
> > > > +and the implications of such links are hard for humans to understand.
> > > 
> > > Maybe so, but it doesn't sound very reference manual-y ;)
> > 
> > Agreed.
> > 
> > > I don't have a suggestion at this time.
> > 
> > I will keep the text until I get a suggestion for a better reason :-(
> > 
> 
> I think we can state "for simplicity".

I think I can use that.

Thanks for both reviews.

Zoltan.