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

Peter Wang novalazy at gmail.com
Mon Jul 12 11:44:32 AEST 2021


On Fri, 09 Jul 2021 16:46:32 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 2021-07-05 18:20 GMT+10:00 "Peter Wang" <novalazy at gmail.com>:
> 
> > 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.
> 
> Ok, I used your example, as well as an expanded version of mine,
> in the attached diff, which I present for your review.

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index 7f59c058f..e2096db05 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
...
> +
> +In the case of a set of mutually recursive types,
> +omitting some constructor definitions from a type may not be enough;
> +it may be necessary to replace some argument types with their subtypes as well.
> +Consider this pair of mutually recursive types representing a bipartite graph,
> +i.e.@ a graph in which there are two kinds of nodes,
> +and edges always connect two nodes of different kinds.
> +In this bipartite graph,
> +the two kinds of nodes are @var{or} nodes and @var{and} nodes,
> +and each kind of node can be connected to zero, two or more nodes
> +of the other kind.
> +
> + at example
> +:- type or_node
> +    --->    or_source(source_id)
> +    ;       logical_or(and_node, and_node)
> +    ;       logical_or_list(and_node, and_node, and_node, list(and_node)).
>  
> -The constructor definitions must be a
> -subset of the constructors of the supertype;
> -we recommend they appear in the same relative order
> -as in the supertype definition.
> -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}.
> +:- type and_node
> +    --->    and_source(source_id)
> +    ;       logical_and(or_node, or_node)
> +    ;       logical_and_list(or_node, or_node, or_node, list(or_node)).
> + at end example
> +
> +If we wanted a subtype to represent graphs in which
> + at var{or} node could be connected to more than two @var{and} nodes,

_each_ @var{or} node

_no_ more than

> +one might think that it would be enough
> +to delete the @var{logical_or_list} constructor from the @var{or_node} type,
> +like this:
> +
> + at example
> +:- type binary_or_node =< or_node
> +    --->    or_source(source_id)
> +    ;       logical_or(and_node, and_node).
> + at end example
> +
> +However, this would not work,
> +because the @var{and_node}s have constructors
> +whose arguments have type @var{or_node}, not @var{binary_or_node}.

> +One would have to create a subtype of the @var{and_node} type
> +that constructs @var{and} nodes
> +from @var{binary_or_node}s, not plain @var{or_node}s,
> +like this:
> +
> + at example
> +:- type binary_or_node =< or_node
> +    --->    or_source(source_id)
> +    ;       logical_or(binary_or_and_node, binary_or_and_node).
> +
> +:- type binary_or_and_node =< and_node
> +    --->    and_source(source_id)
> +    ;       logical_and(binary_or_node, binary_or_node)
> +    ;       logical_and_list(binary_or_node, binary_or_node, binary_or_node,
> +                list(binary_or_node)).
> + at end example
> +
> +That is the end of that example.
> +Now back to the rules for subtypes.

I suggest moving the digression on mutually recursive types to the end
of the chapter, under a heading "A tip on mutually recursive types"
or something like that.

Otherwise, it looks okay.

Peter


More information about the developers mailing list