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

[Peter Wang]

On Sat, 03 Jul 2021 10:24:34 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> I am attaching a proposed diff to the reference manual, for review by both
> Peter and Julien.
> 
> > 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.
> 
> 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.

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index 7f59c058f..be8c2c47a 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
> @@ -2525,17 +2525,30 @@ in that every term of a subtype is a valid term in the supertype.
>  It is possible to convert terms between subtype and supertype
>  using type conversion expressions (@pxref{Type conversions}).
>  
> -A subtype is defined using the form
> +While the syntax for non-subtype discriminated union types is
> + at example
> +:- type @var{type} ---> @var{body}.
> + at end example
> +the syntax for subtypes is
>  @example
>  :- type @var{subtype} =< @var{supertype} ---> @var{body}.
>  @end example
> -
> - at var{subtype} must be a name term
> -whose arguments (if any) are distinct variables.
> -
> - at var{supertype} must be a type (that may contain variables).

> +In both cases, @var{body} is
> +a sequence of constructor definitions separated by semicolons.
> +In both cases, any universally quantified type variable
> +that occurs in @var{body} must occur in the @var{head} of the type definition,
> +i.e. in the part before @code{--->}.
> +

By describing both non-subtype and subtype du type definitions together,
you have to state a restriction that is true for both:

    any universally quantified type variable
    that occurs in @var{body} must occur in the @var{head} of the type definition,
    i.e. in the part before @code{--->}.

and then refine the restriction for subtypes later on:

    Any universally quantified type variable
    that occurs in @var{body} must occur also in @var{subtype}.

The other thing I don't like is describing the body before the head.

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.

> + at var{subtype} must be a type constructor
> +applied to zero or more arguments,
> +which (if any) must be distinct variables.
> +
> + at var{supertype} must be a type constructor
> +applied to zero or more argument types,
> +which @emph{may} be type variables, but they do not have to be,
> +and if they are, do not need to be distinct.

Add:

    Any type variables in @var{supertype} must also occur
    in @var{subtype}.

>  After expanding out equivalences,
> -the principal constructor must specify a discriminated union type
> +the principal type constructor must specify a discriminated union type
>  whose @emph{definition} is in scope where the subtype definition occurs,
>  by normal module visibility rules.

Ok.

> @@ -2543,32 +2556,60 @@ The discriminated union type specified by @var{supertype}
>  may itself be a subtype.
>  Following a chain of visible subtype definitions,
>  it must be possible to arrive at a @emph{base type},
> -which is not a subtype.
> +which is a discriminated union type but @emph{not} a subtype.

Ok.

> -
> -Any variable that occurs in @var{supertype} must occur in @var{subtype}.
>  

It seems this sentence was lost.

> -The @var{body} term is defined as
> -a sequence of constructor definitions separated by semicolons.
> -Any universally quantified type variable that occurs in @var{body}
> -must occur in @var{subtype}.
> +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.

> -The constructor definitions must be a
> -subset of the constructors of the supertype;
> -we recommend they appear in the same relative order
> +Since the subtype cannot add definitions of constructors,
> +the set of constructor definitions in the subtype
> +must be a subset of the constructors definitions in the supertype.
> +We recommend that they should appear in the same relative order
>  as in the supertype definition.

Ok.

> -If the supertype @samp{t} has constructor @samp{f(T1, ..., Tn)} then
> -a subtype @samp{s =< t} may have a constructor @samp{f(S1, ..., Sn)}.
> -For each @var{Si}, it must be that @samp{Si =< Ti}.
> +
> +If the subtype retains a constructor from the super type
> +that has one or more existentially quantified type variables, then
> +there must be a one-to-one mapping between
> +the existentially quantified type variables
> +for the constructor in the subtype definition
> +and the same constructor in the supertype definition.
> +The subtype constructor must repeat
> +exactly the same set of existential class constraints
> +on its existentially quantified type variables as in the supertype;
> +the subtype constructor cannot add or remove any existential class constraints.
> +

Ok.

> +Any universally quantified type variable
> +that occurs in @var{body} must occur also in @var{subtype}.

(This would be moved earlier per my suggestion.)

> +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.
I'm inclined to leave the paragraph out, unless it is clarified.

>  (In the following discussion,
> -assume that equivalence types are expanded out
> -as required.)
> +assume that all equivalence types have been expanded out.)
>  

Ok.

> @@ -2590,18 +2632,12 @@ and purity.
>  (The current implementation does not admit subtyping in
>  higher-order arguments.)
>  
> + 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.

Peter