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

[Peter Wang]

On Wed, 30 Jun 2021 09:08:33 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> This extra field requires slight changes to a nontrivial number of files,
> which have caused repeated conflicts as other changes are made
> to the affected modules. I would therefore like to commit the
> change-in-progress I am working on. Almost all the code in the diff
> is executed only if experiment flags, which default off, are explicitly
> switched on, so there should be no interference with the normal
> operation of the compiler. The remainder of the change involves
> tweaks to the types containing type representation information,
> and to the code that generates or consumes values of those types.
> I would of course bootcheck each change before checkin.
> 
> Does anyone object to me committing such work-in-progress?

No objection from me.

> 
> The logical reviewer for this work is Peter, since he was the last
> person, and maybe the only one, to work on du_type_layout.m
> apart from me. Peter, do you want to review each  change I make
> as I make them, either pre- or post-commit, or should I just make
> progress checkins without review, with a review of the whole thing
> after it is done, but before switching it on?

You can commit and I'll try to review them post-commit. I don't want to
block your progress, and reviewing the changes will take more than
a quick glance.

> 
> My current draft does not handle subtypes as yet, because I am
> not sure I have a full understanding of them as yet. I am fuzzy
> on two questions.
> 
> First, would it be fair to say that a subtype may two differ from
> its supertype in only two ways:
> 
> - it may delete one or more of the supertype's constructors; and/or
> - in the remaining constructors, it may replace some arguments' types
>   with subtypes of those types.
> 
> If so, I would prefer to include this in the reference manual, replacing
> the existing text that talks about such restrictions.

That's right.

> Second, I don't understand this sentence in the reference manual:
> 
> Any variable that occurs in @var{supertype} must occur in @var{subtype}.
> 
> Is it talking about the each type constructor's parameters, or about
> all the type vars in each type's definition? The wording implies
> the latter,

It is the latter. The restriction is that there cannot be free variables
in the supertype part of the subtype definition.

At the start of the section is written:

   A subtype is defined using the form
     :- type SUBTYPE =< SUPERTYPE ---> BODY.

So for the definition:

    :- type citrus =< fruit(T) ---> ...

SUBTYPE is citrus.
SUPERTYPE is fruit(T).
Since T occurs in SUPERTYPE but not SUBTYPE, this definition is invalid.

> but that can't be correct, since the subtype may omit
> a data constructor that has an existentially typed argument.

Existentially quantified type variables can only occur in the BODY part
of the definition, so don't have anything to do with that sentence.

I hope that clears it up. We should of course improve the wording
since you found it confusing.

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

Type parameters that occur in the SUBTYPE part but not the SUPERTYPE
part would have to be phantom types.

> or to permute any existing type parameters?

I think this question comes from an assumption that a type parameter
in the supertype remains a type parameter in the subtype.
That's not necessarily the case, as in:

    :- type non_empty_list_of_citrus =< list(citrus)
        --->    [citrus | list(citrus)].

> And where is this restriction enforced?
> I couldn't find anything related to this in check_subtype_defn in add_type.m.

It's checked in check_supertype_vars in parse_type_defn.m.

Peter