5.5 Definition of Phyla

Phyla  may be introduced implicitly or explicitly.

An operator definition implicitly defines the codomain of its signature as a phylum if is not already declared. So most of the phyla in an abstract syntax will be implicitly defined.

The definition

pair : Elem # Elem -> Pair;

defines Pair as a phylum, and pair as an operator whose codomain is Pair. This definition does not define Elem that must be defined somewhere else.

5.5.1 Type Inclusion

A type inclusion  implicitly defines the container as a phylum if it is not already declared.

The following example of type inclusion expresses the fact that an identifier is also an expression.

Example:

Id < Exp;

Predefined types cannot be used in a type inclusion.

Circular definitions of phyla results in equal phyla and will be indicated by the type-checker as a warning.

5.5.2 Union of Phyla

A phylum can also be defined explicitly as the union of other phyla . In this case, it is not possible to include some other phylum in it later on, neither to use it as the co-domain of an operator.

Example:

Exp_Stat = Exp + Stat;

5.5.3 Modularity

Explicit definition of phyla and phyla inclusion may use some phyla imported from a previously defined formalism, allowing modular definition of abstract syntaxes.

Formalism Inclusion, Typed Names

5.5.4 Syntax

Here is the complete syntax of phyla inclusion and phyla union:

inclusion --> tid "<" sinclusion ";"
sinclusion -->   id
               | id "<" sinclusion
union --> id "=" tid ("+" tid)* ";"