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

[Zoltan Somogyi]

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?

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.

> I suggest to start the chapter something like this:
> 
>     Recall that / as previously described,
>     the syntax for non-subtype discriminated union types is ...
> 
>     In contrast, the syntax for subtype type definitions is ...
> 
>     @var{subtype} must be a type constructor
>     applied to zero or more arguments, ...
> 
>     @var{supertype} must be a type constructor
>     applied to zero or more argument types, ...
> 
>     As with other discriminated union type definitions,
>     the @var{body} of a subtype definition is
>     a sequence of constructor definitions separated by semicolons.
>     Any universally quantified type variable
>     that occurs in @var{body} must occur in the @var{subtype} part of
>     the type definition.

My updated draft follows that overall plan.

>> +The body of the subtype may differ from the body of its supertype in two ways.
>> + at itemize @bullet
>> + at item
>> +It may omit one or more constructor definitions.
>> +The ability to do this is the main motivation for the use of subtypes.
>> + at item
>> +It may change the types of some of the arguments of some of the constructors,
>> + at emph{provided} that each replacement replaces a type with one of its subtypes.
>> +Formally, this means that
>> +if the supertype @samp{t} has a constructor @samp{f(T1, ..., Tn)},
>> +and the subtype @samp{s =< t} has a constructor @samp{f(S1, ..., Sn)}.
>> +then for each @var{Si}, the condition @samp{Si =< Ti} must hold.
> 
> Ok.
> 
>> +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.

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

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

Thanks for the review.

Zoltan.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DIFF.refman2
Type: application/octet-stream
Size: 9368 bytes
Desc: not available
URL: <http://lists.mercurylang.org/archives/developers/attachments/20210705/5f4f1403/attachment-0001.obj>