[m-dev.] getting type representation decisions from .int files

[Peter Wang]

On Mon, 05 Jul 2021 10:15:57 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 2021-07-04 14:13 GMT+10:00 "Peter Wang" <novalazy at gmail.com>:
> >> Is there some special reason why this check is not in add_type.m, with all
> >> the other checks on subtype definitions? I would have thought that
> >> having all the semantic checks for a given construct being in one place
> >> is a good thing.
> > 
> > It's the same place where we check for free variables in constructors.
> 
> OK. I will add comments to add_type.m for both the subtype and non-subtype
> cases pointing that out.
> 
> I have tried to address most of your concerns about the update to the
> reference manual, as shown by the attached updated diff.
> However, I still have some concerns.
> 
> > The other thing I don't like is describing the body before the head.
> 
> The reason I did that is that the changes to the body are *the reason*
> one may want to use subtypes in the first place. The changes to the head
> are just administrivia compared to that. Do you disagree?

No, you're right that the motivation is buried.

> 
> However, while I my draft update can describe the rules for the
> subtype =< supertype head, I cannot describe the *rationale* for
> those rules, since I do not understand the rationale. My original email
> in this thread asked about that, but your reply was not on-point,
> at least not to my mind. Accordingly, I have not yet updated
> this part of my diff.

See below.

> >> +This is often required when one wants to create
> >> +subtypes of two or more mutually recursive types.
> >> + at end itemize
> > 
> > I'm not sure what this sentence is saying.
> 
> If you have two mutually recursive types, say p and q,
> and you want to create a subtype of p, say psub, then
> 
> - an argument of a constructor p1 in psub may have type q,
> - the definition of q will have a constructor q2, one of whose args is type p,
>   when you want type psub.
> 
> To prevent this,
> 
> - that argument of constructor p1 in psub will have to have type qsub,
> - with the definition of qsub changing the type of the argument of q2
>   from p to psub.
> 
> I can add some more refined text about this, and maybe an example,
> if you think that would help.

I see. I think a more common case where you might want to replace an
argument type with a subtype would not involve mutually recursive types,
which is why the mention of them confused me.

    :- type basket
        --->    basket(int, fruit).

    :- type lemon_basket =< basket
        --->    basket(int, lemon).

You might want to do this to ensure that some part of your program deals
only in lemon_baskets and lemons, whereas other parts of the program
may need to deal with baskets and fruit.

> >> +However, the list of parameters in @var{subtype} is not otherwise restricted;
> >> +for example, it need not have any particular relationship
> >> +with the list of parameters
> >> +of the principal type constructor of @var{supertype}.
> >> + at c There should be some discussion here
> >> + at c of the possible uses of this flexibility.
> > 
> > I think the "not otherwise restricted" part is misleading. There *are*
> > restrictions on the parameters in @var{subtype} as stated elsewhere.
> 
> That is what the "otherwise" is meant to allow for. The wording should
> make that clearer.
> 
> > I'm inclined to leave the paragraph out, unless it is clarified.
> 
> I can't clarify it until I know *why* it is useful to allow the type argument
> vectors of the subtype and the supertype to differ in so drastic ways,
> subject only to the type var inclusion test. Can you please enlighten me?
> 

Thinking back on it now, while earlier subtype proposals would have
worked very differently in the end, syntactically the starting point was
the same. Both Fergus and Mark's proposals didn't place any restrictions
on the supertype, except to prevent free variables. As I was developing
my proposal and implementation, I never encountered any need to deviate
from that, technically or subjectively.

In response to your original questions:

> then why does it say only "must occur"

To prevent free variables in the supertype.

> instead of requiring the subtype's and the supertype's
> type parameter lists to be identical?

This is the subjective part. It would disallowing even simple cases
like:

    :- type bar(T, U) =< foo(T, U, U)

or

    :- type bar(T, U) =< foo(T, pair(U, U))

> What is there to be gained
> by allowing the subtype to add type parameters,

As discussed previously, those additional type parameters would have to
be phantom types. It's not something that was specifically designed for,
but does seem at least a little bit useful.

> or to permute any existing type parameters?

It's indeed hard to imagine why you would go around permuting type
parameters for no reason, but the idea of permuting only makes sense if
there was a correspondence between the subtype parameters and the
supertype parameters.

I tried to come up with an example that takes advantage of the current
design:

    :- type result(E, Ex)
        --->    ok(value)
        ;       error(E)
        ;       exception(Ex).

    :- type parse_result(E) =< result(non_empty_list(E), E)
        --->    ok(simple_value)
                % the parser only returns simple values
        ;       error(non_empty_list(E))
                % the parser can return multiple errors
        ;       exception(E).
                % the parser throws/catches errors of the same type

It is contrived, but at least a little bit realistic.

> >> + at c This should not be here. It should be replaced by a statement at the top
> >> + at c that says: these cases list *all* the situations in which S =< T may hold
> >> + at c without S = T. In every other situation, S =< T if and only if S = T."
> >>  @samp{P =< Q} holds if @var{P} and @var{Q} are both
> >>  existentially quantified type variables, and @samp{P = Q}.
> > 
> > That should be okay.
> 
> Ok. I have rewritten this part of the section using more formal wording,
> though I have no idea how to make the result pretty. Does anyone
> know how to nicely typeset this kinds of maths in texinfo?

>From a quick look, you can insert TeX commands with @math but that will
do nothing for HTML and Info output. @sub does subscripts which can be
rendered in HTML, but results in something like S_{i} in Info. I don't
see that as better.

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index 7f59c058f..78f714d0b 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
...
> + at item
> +If @samp{S} and @samp{T} have different principal type constructors,
> +and if @samp{S = f(S1, ..., Sn)}, @samp{S =< T} holds if
> +    @itemize @minus
> +    @item
> +    there is a visible subtype definition starting with
> +    @w{@samp{:- type f(R1, ..., Rn) =< U}},
> +    @item
> +    for all @var{i} in @samp{1..n}, @w{@samp{Si = Ri}} (unification), and
> +    @item
> +    @samp{U =< T}.
> +    @end itemize
> +In other words, if all occurrences of @var{Ri} in @var{U}
> +are replaced by the corresponding for @var{Si} to give @var{Usub},
> +then @samp{Usub =< T} must hold.
> + at end itemize

Delete the "for" in "corresponding for".

The rest is okay.

Peter