<p>In certain cases, types may depend not only on other types (polymorphism), but also on the parameters of another type (dependent types). The TL language provides very limited support for this functionality: dependence is only allowed on a natural parameter whose type is designated using <code>#</code> (alias <code>nat</code>, but this is private -- TL doesn't currently support this synonym). Values of type # are serialized as 32-bit signed numbers from 0 to 2^31-1.</p>
<p>Suppose we want to use induction to define the types “one integer”, “two integers”, and “three integers”. We could try to define them as follows:</p>
<p>The first two variations lead to the same serialization. For example, <code>(2 3 9):%triple</code> and <code>(2 (3 9)):%triple</code> serialize as three 32-bit numbers: <code>2 3 9</code>. The last variation better emphasizes the inductive version of the definition, but it uses boxed types. This is good from a theoretical perspective, but it leads to “superfluous” constructor names in serialization.</p>
<p>Therefore, we will write <code>%Type-Ident</code> to indicate the bare type that corresponds to the boxed type <code>Type-Ident</code> with a single constructor. If this constructor is named <code>constructor</code>, then according to the definition %<code>Type-Ident</code> = %<code>constructor</code>. Now we can write our definition like this:</p>
<p>If we now abstract <em>n</em> out of the name of the type name and make it like a parameter for a polymorphic (dependent, to be more exact) type, then something like the following can be written in a suitable functional language:</p>
<pre><code>NewType Tuple (n : #) :=
| tnil = Tuple 0
| tcons n:# hd:int tl:%(Tuple n) = Tuple (S n)
EndType;</code></pre>
<p>In the TL language, it looks like this:</p>
<pre><code>tnil = Tuple 0;
tcons {n:#} hd:int tl:%(Tuple n) = Tuple (S n);</code></pre>
<p>The function <code>S : # -> #</code> and the constant <code>O : #</code> (it is <code>0</code>) are the function for the next natural number (<code>S n = n + 1</code>) and the constant null. Therefore, the type <code>#</code> (alias <code>nat</code>) behaves as if it were defined in TL using the constructors</p>
<pre><code>O = nat;
S nat = nat;</code></pre>
<p>or, using syntax more typical of other functional languages,</p>
<pre><code>NewType nat :=
| O
| S nat
EndType;</code></pre>
<p>Types of all defined combinators:</p>
<pre><code>O : #
S : # -> #
Tuple : # -> Type
tnil : Tuple 0
tcons : forall n : #, int -> Tuple n -> Tuple (S n)</code></pre>
<p>or</p>
<pre><code>Tuple : forall n : #, Type;
tcons : forall n : #, forall hd : int, forall tl : Tuple n, Tuple (S n)</code></pre>
<p>Note that in this case the constructor <code>tnil</code> does not depend on the parameter <em>n</em>, while <code>tcons</code> does.</p>
<p>In an analogous manner, it is possible to define a complete binary tree of height <em>h</em> with strings in the leaf nodes:</p>
<pre><code>tleaf value:string = BinTree 0;
tnode {h:#} left:(BinTree h) right:(BinTree h) = BinTree (S h);</code></pre>
<p>Or a random tree whose leaf nodes are all a distance of <em>h</em> from the root and whose nodes are all labeled with integers:</p>
<pre><code>hleaf value:int = Tree 0;
hnode {n:#} left:(Tree n) next:(Tree (S n)) = Tree (S n)
hnil {n:#} = Tree (S n)</code></pre>
<p>Another version:</p>
<pre><code>hleaf' value:int = Tree' 0;
hnode' {n:#} children:(list (Tree' n)) = Tree' (S n)</code></pre>
<p>Let us try to define a type <code>Tuple X n</code> whose values are <em>n</em>-tuples of type <code>X</code> values. In this way, <code>Tuple</code> will be simultaneously polymorphic and dependent:</p>
<pre><code>Tuple : Type -> # -> Type;</code></pre>
<p>In the familiar syntax of functional languages:</p>
<pre><code>NewType Tuple {X : Type} {n : #} :=
| vnil : Tuple X 0
| vcons {n:#} hd:X tl:%(Tuple X n) : Tuple X (S n)
EndType</code></pre>
<p>or, in TL syntax,</p>
<pre><code>vnil {X:Type} = Tuple X 0;
vcons {X:Type} {n:#} tl:(%Tuple X n) = Tuple X S n</code></pre>
<p>In the end we obtain terms for the following types:</p>
<pre><code>vnil : forall X : Type, Tuple X 0
vcons : forall X : Type, forall n : #, X -> Tuple X n -> Tuple X (S n)</code></pre>
<p>or</p>
<pre><code>vnil : forall X : Type, Tuple X 0
vcons : forall X : Type, forall n : #, forall hd : X, forall tl : Tuple X n, Tuple X (S n)</code></pre>
<p>The <code>Tuple</code> we just defined differs from the built-in <code>Vector</code> type. Specifically, the <code>Vector</code> type formally depends on a single argument (a type), but our <code>Tuple</code> depends on two (a type and a number):</p>
<pre><code>Tuple : Type -> # -> Type;
Vector : Type -> Type;</code></pre>
<p>The built-in <code>Vector</code> could be defined in terms of our <code>Tuple</code> using “summing across all <em>n</em> : #":</p>
<pre><code>vector {X:Type} n:# v:(%Tuple X n) = Vector X;</code></pre>
<p>Nevertheless, our <code>Tuple</code> has its advantages. For example, we can define data types such as:</p>
<p>In any event, remember that during calculation of the <code>matrix_10x10</code> combinator's number, all parentheses must be removed and the CRC32 of the string <code>matrix_10x10 a:%Tuple %Tuple double 10 10 = Matrix_10x10</code> must be computed.</p>
<p>Moreover, we can define arbitrarily-sized matrices:</p>
<pre><code>matrix {X:Type} m:# n:# a:(%Tuple (%Tuple X m) n) = Matrix X;</code></pre>
<p>In this case using vector would result in storing the length of a row (<em>m</em>) in each row, e.g. <em>n</em> times.</p>
<p>Note that the serializations of values of type <code>%Tuple X n</code> and <code>vector X</code> (also known as <code>%vector X</code> and <code>%Vector X</code>) nearly match when <em>n > 0</em>: in both cases we obtain a single 32-bit number (equal to <em>n-1</em> or <em>n</em> depending on the version) followed by the serializations of <em>n</em> objects of type <em>X</em>. (This is slightly untrue: values of type <code>%Tuple X n</code> can only be serialized if <em>n</em> is a constant or value known from one of the preceding fields of the enclosing entry; but then this <em>n</em> won't be serialized explicitly anywhere).</p>
<h2><aclass="anchor"href="#special-syntax-for-repetitions"id="special-syntax-for-repetitions"name="special-syntax-for-repetitions"><iclass="anchor-icon"></i></a>Special syntax for repetitions</h2>
<p>In view of the importance of the construction presented above, it is built into the TL language in the following manner. A substructure in the form of [ <em>array-field-name</em> ":" ] [ <em>nat-ident</em> "<em>" ] "[" </em>field-descr<em> ... "]” may be used in the declaration of any combinator, where </em>nat-ident* is the name of any previously encountered field of type # (if it is not explicitly indicated, the most recent is used). In abstract, this substructure is equivalent to:</p>
<p>We have already encountered the last version as a “definition” of the “built-in type” <code>Vector</code>.</p>
<p>Of course, several fields, as complex as desired, may be within the repeating part. Furthermore, besides using <em>n</em> as a repeat counter, one may use expressions of the form <em>(n+const)</em> and <em>(const+n)</em>, where <em>const</em> is a small nonnegative constant, which are shorthand for <em>S (S ( ... (S n) ... ))</em>:</p>
<p>To calculate the CRC32 these expressions are converted to expressions of the form <code>(const+X)</code> without internal spaces. Additionally, the <code>*</code> in this case is not set off by spaces on the left and right.</p>
<h2><aclass="anchor"href="#serialization-of-dependent-types"id="serialization-of-dependent-types"name="serialization-of-dependent-types"><iclass="anchor-icon"></i></a>Serialization of dependent types</h2>
<p>Serialization of dependent types and polymorphic types is not a fundamental challenge: we have combinators with non-zero arity with Type values. For example, the type <code>Tuple double 10 : Type</code> serializes to <code>'Tuple' '%double' 10</code>. Note that at present in practice there is virtually no need to serialize types, whether dependent or not.</p>
<h2><aclass="anchor"href="#optional-combinator-parameters-in-tl"id="optional-combinator-parameters-in-tl"name="optional-combinator-parameters-in-tl"><iclass="anchor-icon"></i></a>Optional combinator parameters in TL</h2>
<p>Optional combinator parameters in TL must possess the following properties:</p>
<ul>
<li>
<p>Optional parameters must be precisely the combinator's first several arguments;</p>
</li>
<li>
<p>The value of any optional parameter must be entirely determined by the combinator's result type.</p>
</li>
</ul>
<p>For example, in <code>cons {X:Type} hd:X tl:(list X) = list X</code> the parameter <code>X</code> may be made optional, because it is located at the very beginning of the argument list and is unambiguously determined by the <code>list X</code> result type. Similarly, in <code>tcons {X:Type} {n:#} hd:X tl:(%Tuple X n) = Tuple X (S n)</code> the values of X and n are completely determined based on the <code>Tuple X (S n)</code> result type, therefore they made be made optional parameters.</p>
<p>It usually makes sense to move all of a constructor's arguments satisfying the second condition to the beginning of the list, arrange them in the order they appear in the result type's parameters, and make them optional. Given such an approach, the full version of a constructor is rarely needed -- only when we want to transmit the value of the polymorphic or dependent type as a value of type Object. In all other cases, the type of the expected value from the context is already known, which means that all optional parameters can be recovered during decomposition.</p>
<p>See also <ahref="/mtproto/TL-optargs">Optional combinator parameters and their values</a>.</p></div>
</div>
</div>
</div>
<divclass="footer_wrap">
<divclass="footer_columns_wrap footer_desktop">
<divclass="footer_column footer_column_telegram">
<h5>Telegram</h5>
<divclass="footer_telegram_description"></div>
Telegram is a cloud-based mobile and desktop messaging app with a focus on security and speed.
