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

[Peter Wang]

On Wed, 05 Aug 2026 11:04:06 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 
> On Wed, 5 Aug 2026 17:13:47 +1000, Peter Wang <novalazy at gmail.com> wrote:
> 
> > On Tue, 04 Aug 2026 23:39:01 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> > > + at heading Lifting a subtype
> > > +
> > > +If type @samp{S} has the form @samp{S = tc(S1, ..., Sn)}
> > > +and there is a visible subtype definition starting with
> > > + at w{@samp{:- type tc(RP1, ..., RPn) =< U}},
> > > +then we define @samp{lift(S)} as the type that results from
> > > +replacing all occurrences of each type parameter @samp{RPi} in @samp{U}
> > > +with the corresponding @samp{Si}.
> > > +
> > > +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

> > > + at item
> > > + at samp{lift_to_base(FromType)} and @samp{lift_to_base(ToType)}
> > > +have the same type constructor, being e.g.
> > > + at samp{base_tc(BaseFromArgType1, ..., BaseFromArgTypen)} and
> > > + at samp{base_tc(BaseToArgType1, ..., BaseToArgTypen)} respectively,
> > > +with the type parameters of the type constructor
> > > + at samp{base_tc} in its declaration being @samp{BP1, ..., BPn};
> > > + at item
> > > +for all @var{i} in @samp{1..n} where @samp{BPi} must be invariant,
> > > + at samp{BaseFromArgTypei} is identical to @samp{BaseToArgTypei}; and
> > > + at c XXX Should we instead phrase this as
> > > + at c "where the i'th parameter of base_tc must be invariant"?
> > > + at item
> > > +for all @var{i} in @samp{1..n} where @samp{BPi} need not be invariant,
> > > + at samp{BaseFromArgTypei} is coercable to @samp{BaseToArgTypei}.
> > > + at c XXX "coercable" is probably not the best name for this concept.
> > > + at c Alternatives may be phrases like "related by subtyping".
> > > + at end itemize
> > 
> > "coercable" sounds self referential.
> 
> Which is the main reason I don't like it either.
> 
> > 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"?

> 
> 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?

> > > +The last two conditions raise two new questions.
> > > +Given a base type constructor, which of its parameters must be invariant?
> > > +And what does it mean for one type to be coercable to another type?
> > > +
> > 
> > > + at heading Must-be-invariant type parameters
> > > +
> > 
> > Can we name this "Type parameter variance"? I don't like
> > must-be-invariant.
> 
> I think that is
> 
> I think that would be misleading for most readers. The distinction I am
> trying to make is definititely must-be-invariant vs need-not-be-invariant,
> because regardless of which category a type parameter falls into,
> the corresponding arg types in the from-type and to-type ARE allowed
> to be invariant.

See the following.

> 
> 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.

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.
]

> > > + at item
> > > + at samp{Tij} is a foreign type, a solver type, or an abstract type.
> > > + at c XXX We should not mention solver types if they cannot occur
> > > + at c in du types, but I (zs) don't know whether they can occur or not.
> > > + at c XXX We currently make a type parameter must-be-invariant for a foreign type,
> > > + at c but I (zs) don't know the justification for that.
> > > +
> > 
> > For the same reason the type parameter in any mutable type must be
> > invariant. If you can coerce a variable from mutvar(dog) to mutvar(animal),
> > then you can put a cat in where an animal is accepted,
> > then pull a cat out where a dog is expected.
> 
> OK, I will add something to that effect.
> 
> 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.

> > > +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".

Peter