<p>A combinator identifier is either an identifier starting with a lowercase Latin letter (<em>lc-ident</em>), or a namespace identifier (also <em>lc-ident</em>) followed by a period and another <em>lc-ident</em>. Therefore, <code>cons</code> and <code>lists.get</code> are valid combinator identifiers.</p>
</li>
<li>
<p>A combinator has a <em>name</em>, also known as a <em>number</em> (not to be confused with the <em>designation</em>) -- a 32-bit number that unambiguously determines it. It is either calculated automatically (see below) or it is explicitly assigned in the declaration. To do this, a hash mark (<code>#</code>) and exactly 8 hexadecimal digits -- the combinator's name -- are added to the identifier of the combinator being defined.</p>
</li>
<li>
<p>A combinator's declaration begins with its identifier, to which its name (separated by a hash mark) may have been added.</p>
</li>
<li>
<p>After the combinator identifier comes the main part of the declaration, which consists of declarations of <em>fields</em> (or <em>variables</em>), including an indication of their <em>types</em>.</p>
</li>
<li>
<p>First come declarations of optional fields (of which there may be several or none at all). Then there are the declarations of the required fields (there may not be any of these either).</p>
</li>
<li>
<p>Any identifier that begins with an uppercase or lowercase letter and which does not contain references to a namespace can be a field (variable) identifier. Using <em>uc-ident</em> for identifiers of variable types and <em>lc-indent</em> for other variables is good practice. </p>
</li>
<li>
<p>Next a combinator declaration contains the equals sign (<code>=</code>) and the result type (it may be composite or appearing for the first time). The result type may be polymorphic and/or dependent; any fields of the defined constructor's fields of type <code>Type</code> or <code>#</code> may be returned (as subexpressions).</p>
</li>
<li>
<p>A combinator declaration is terminated with a semicolon.</p>
</li>
</ul>
<p>In what follows, a constructor's <em>fields</em>, <em>variables</em>, and <em>arguments</em> mean the same thing.</p>
<h3><aclass="anchor"href="#optional-field-declarations"id="optional-field-declarations"name="optional-field-declarations"><iclass="anchor-icon"></i></a>Optional field declarations</h3>
<ul>
<li>
<p>These have the form <code>{</code><em>field_1</em> ... <em>field_k</em><code>:</code><em>type-expr</em><code>}</code>, where <em>field_i</em> is a variable (field) identifier that is unique within the scope of the combinator declaration, and <em>type-expr</em> is a type shared by all of the fields. </p>
</li>
<li>
<p>If <em>k>1</em>, this entry is functionally equivalent to <code>{</code><em>field_1</em><code>:</code><em>type-expr</em><code>}</code> ... <code>{</code><em>field_k</em><code>:</code><em>type-expr</em><code>}</code>. </p>
</li>
<li>
<p>All optional fields must be explicitly named (using <code>_</code> instead of <em>field_i</em> is not allowed).</p>
</li>
<li>
<p>Moreover, at present the names of all optional fields must share the combinator's result type (possibly more than once) and themselves be of type <code>#</code> (i,e., <code>nat</code>) or <code>Type</code>. Therefore, if the exact result type is known, it is possible to determine the values of all of the combinator's implicit parameters (possibly obtaining a contradiction of the form <code>2=3</code> in doing so, which means that the combinator is not allowed in the context).</p>
</li>
</ul>
<h3><aclass="anchor"href="#required-field-declarations"id="required-field-declarations"name="required-field-declarations"><iclass="anchor-icon"></i></a>Required field declarations</h3>
<ul>
<li>
<p>These may have the form <code>(</code><em>field_1</em> ... <em>field_k</em><code>:</code><em>type-expr</em><code>)</code>, similar to an optional field declaration, but with parentheses. This entry is equivalent to <code>(</code><em>field_1</em><code>:</code><em>type-expr</em><code>)</code> ... <code>(</code><em>field_k</em> : <em>type-expr</em><code>)</code>, where the fields are defined one at a time.</p>
</li>
<li>
<p>The underscore sign (<code>_</code>) can be used as names of one or more fields (<em>field_i</em>), indicating that the field is anonymous (the exact name is unimportant).</p>
</li>
<li>
<p>One field may be declared without outer parentheses, like this: <em>field_id</em><code>:</code><em>type-expr</em>. Here, however, if <em>type-expr</em> is a complex type, parentheses may be necessary around <em>type-expr</em> (this is reflected in BNF).</p>
</li>
<li>
<p>Furthermore, one anonymous field may be declared using a <em>type-expr</em> entry, functionally equivalent to <code>_</code><code>:</code><em>type-expr</em>.</p>
</li>
<li>
<p>Required field declarations follow one after another, separated by spaces (by any number of whitespace symbols, to be more precise).</p>
</li>
<li>
<p>The declared field's type (<em>type-expr</em>) may use the declared combinator's previously defined variables (fields) as subexpressions (i.e. parameter values). For example:</p>
<p>These may only exist among required parameters. They have the form [ <em>field-id</em><code>:</code> ] [ <em>multiplicity</em><code>*</code> ] <code>[</code><em>args</em><code>]</code>, where <em>args</em> has the same format as the combinator's declaration of (several) required fields, except that all of the enclosing combinator's previously declared fields may be used in the argument types.</p>
</li>
<li>
<p>The name of a field of an enclosing combinator that receives a repetition as a value may be specified (<em>field-id</em>), or bypassed, which is equivalent to using the underscore sign as a <em>field-id</em>.</p>
</li>
<li>
<p>The <em>multiplicity</em> field is an expression of the type <code>#</code> (<code>nat</code>), which can be a real constant, the name of a preceding field of type <code>#</code>, or an expression in the form <code>(</code><em>c</em><code>+</code><em>v</em><code>)</code>, where <em>c</em> is a real constant and <em>v</em> is the name of a field of type <code>#</code>. The sense of the <em>multiplicity</em> field is to provide the length of the (repetition) vector, each element of which consists of values of the types enumerated in <em>args</em>.</p>
</li>
<li>
<p>The <em>multiplicity</em> field may be bypassed. In this case, the last preceding parameter of type <code>#</code> from the enclosing combinator is used (it must be).</p>
</li>
<li>
<p>Functionally, the repetition <em>field-id</em><code>:</code><em>multiplicity</em><code>*</code><code>[</code><em>args</em><code>]</code> is equivalent to the declaration of the single field <code>(</code><em>field-id</em><code>:</code><code>%Tuple</code><code>%AuxType</code><em>multiplicity</em><code>)</code>, where <code>aux_type</code> is an auxiliary type with a new name defined as <code>aux_type *args* = AuxType</code>. If any of the enclosing type's fields are used within <em>args</em>, they are added to the auxiliary constructor <code>aux_type</code> and to its <code>AuxType</code> result type as the first (optional) parameters. </p>
</li>
<li>
<p>If <em>args</em> consists of one anonymous field of type <em>some-type</em>, then <em>some-type</em> can be used directly instead of <code>%AuxType</code>.</p>
</li>
<li>
<p>If during implementation the repetitions are rewritten as indicated above, it is logical to use instead of <code>aux_type</code> and <code>AuxType</code>, some identifiers that contain the name of the outer combinator being defined and the repetition's index number inside its definition.</p>
</li>
</ul>
<p>Example:</p>
<pre><code>matrix {m n : #} a : m* [ n* [ double ] ] = Matrix m n;</code></pre>
matrix {m : #} {n : #} (a : %Tuple %(AuxType n) m) = Matrix m n;</code></pre>
<p>Moreover, the built-in types <code>Tuple</code> and <code>Vector</code> could be defined as:</p>
<pre><code>tnil {X : Type} = Tuple X 0;
tcons {X : Type} {n : #} hd:X tl:%(Tuple X n) = Tuple X (S n);
vector {X : Type} (n : #) (v : %(Tuple X n)) = Vector X;</code></pre>
<p>Actually, the following equivalent entry is considered the definition of <code>Vector</code> (i.e. it is specifically this entry that is used to compute the name of the <code>vector</code> constructor and its partial applications):</p>
<p>permits assigning fields which are only present if the value of a preceding mandatory or optional field of type <code>#</code> is not null (or if its chosen bit is not zero if the special binary bit-selection operator <code>.</code> is applied).
Example:</p>
<divclass="richcode">
<p>user {fields:#} id:int first_name:(fields.0?string) last_name:(fields.1?string) friends:(fields.2?%(Vector int)) = User fields;<br>
