MTProto移动协议的TL依赖类型

主条目：TL 语言。

在某些情况下，MTProto 移动协议的TL类型不仅可能依赖于其他类型（多态），还可能依赖于另一个类型的参数（依赖类型）。TL 语言对此功能的支持非常有限：仅允许依赖于使用 `#` 指定的自然参数#（别名 `#` nat，但这是私有的——TL 目前不支持此别名）。类型为 `#` 的值被序列化为 0 到 2^31-1 之间的 32 位有符号数。

例如：整数元组（向量）

假设我们想用归纳法定义“一个整数”、“两个整数”和“三个整数”这三种类型。我们可以尝试这样定义它们：

empty = Empty;
single x:int = Single;
pair x:int y:int = Pair;
triple x:int y:int z:int = Triple;
quadruple x:int y:int z:int t:int = Quadruple;
...

或者：

empty = Empty;
single x:int empty = Single;
pair x:int y:single = Pair;
triple x:int yz:pair = Triple;
quadruple x:int yzt:triple = Quadruple;

或者：

tnil = Tuple0;
tcons0 hd:int tl:Tuple0 = Tuple1;
tcons1 hd:int tl:Tuple1 = Tuple2;
tcons2 hd:int tl:Tuple2 = Tuple3;
...
tcons_n hd:int tl:Tuple_n = Tuple_(n+1)

前两种变体导致相同的序列化结果。例如，(2 3 9):%triple它们都会(2 (3 9)):%triple序列化为三个 32 位数字：2 3 9。最后一种变体更好地强调了归纳定义的版本，但它使用了装箱类型。从理论角度来看，这很好，但会导致序列化过程中出现“多余的”构造函数名称。

因此，我们将使用 ` %Type-Ident%` 来表示与装箱类型对应的裸类型，该类型Type-Ident只有一个构造函数。如果此构造函数名为`% constructor`，则根据定义，`%` Type-Ident= %` constructor。现在我们可以这样定义：

tnil = Tuple0;
tcons_n hd:int tl:%Tuple_n = Tuple_(n+1)

如果我们现在从类型名称中抽象出n ，并将其作为多态（更准确地说是依赖）类型的参数，那么就可以用合适的函数式语言编写类似下面的代码：

NewType Tuple (n : #) :=
| tnil = Tuple 0
| tcons n:# hd:int tl:%(Tuple n) = Tuple (S n)
EndType;

用目标语言来说，它看起来是这样的：

tnil = Tuple 0;
tcons {n:#} hd:int tl:%(Tuple n) = Tuple (S n);

函数S : # -> #和常量O : #（它是0）分别是下一个自然数的函数（S n = n + 1）和常量 null。因此，该类型#（别名nat）的行为就像是在 TL 中使用构造函数定义一样。

O = nat;
S nat = nat;

或者，使用其他函数式语言更典型的语法，

NewType nat :=
| O
| S nat
EndType;

所有已定义组合子的类型：

O : #
S : # -> #
Tuple : # -> Type
tnil : Tuple 0
tcons : forall n : #, int -> Tuple n -> Tuple (S n)

或者

Tuple : forall n : #, Type;
tcons : forall n : #, forall hd : int, forall tl : Tuple n, Tuple (S n)

请注意，在这种情况下，构造函数tnil不依赖于参数n，而tcons则依赖于参数 n。

类似地，也可以定义一个高度为h 的完全二叉树，其叶节点为字符串：

tleaf value:string = BinTree 0;
tnode {h:#} left:(BinTree h) right:(BinTree h) = BinTree (S h);

或者一棵随机树，其所有叶节点到根节点的距离均为h ，并且所有节点都用整数标记：

hleaf value:int = Tree 0;
hnode {n:#} left:(Tree n) next:(Tree (S n)) = Tree (S n)
hnil {n:#} = Tree (S n)

另一个版本：

hleaf' value:int = Tree' 0;
hnode' {n:#} children:(list (Tree' n)) = Tree' (S n)

多态依赖类型

让我们尝试定义一个类型，Tuple X n它的值是n 个类型X值的元组。这样，Tuple它将同时具有多态性和依赖性：

Tuple : Type -> # -> Type;

在函数式语言的常见语法中：

NewType Tuple {X : Type} {n : #} :=
| vnil : Tuple X 0
| vcons {n:#} hd:X tl:%(Tuple X n) : Tuple X (S n)
EndType

或者，用 TL 语法来说，

vnil {X:Type} = Tuple X 0;
vcons {X:Type} {n:#} tl:(%Tuple X n) = Tuple X S n

最终我们得到以下几种类型的项：

vnil : forall X : Type, Tuple X 0
vcons : forall X : Type, forall n : #, X -> Tuple X n -> Tuple X (S n)

或者

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)

相关和

我们刚才定义的类型Tuple与内置Vector类型不同。具体来说，内置Vector类型形式上依赖于单个参数（类型），而我们的类型Tuple依赖于两个参数（类型和数字）：

Tuple : Type -> # -> Type;
Vector : Type -> Type;

内置函数Vector可以用我们Tuple使用“对所有n : # 求和”来定义：

vector {X:Type} n:# v:(%Tuple X n) = Vector X;

然而，我们的方法Tuple也有其优势。例如，我们可以定义如下数据类型：

matrix_10x10 a:(%Tuple (%Tuple double 10) 10) = Matrix_10x10;

总之，请记住，在计算组合子数时，必须删除所有括号，并计算matrix_10x10字符串的 CRC32 值。matrix_10x10 a:%Tuple %Tuple double 10 10 = Matrix_10x10

此外，我们可以定义任意大小的矩阵：

matrix {X:Type} m:# n:# a:(%Tuple (%Tuple X m) n) = Matrix X;

在这种情况下，使用向量会导致在每一行中存储一行的长度（m ），例如n次。

请注意，当n > 0%Tuple X n时，类型为 ` None` 和`None` vector X（也称为 `None`和%vector X`None` ）的值的序列化结果几乎相同：两种情况下，我们都会得到一个 32 位数字（等于n-1或n ，具体取决于版本），后面跟着n 个类型为`X`的对象序列化结果。（这略有不准确：只有当n是常量或已知值时，类型为 `None` 的值才能被序列化；但此时n不会被显式地序列化。）%Vector X%Tuple X n

重复的特殊语法

鉴于上述构造的重要性，它以如下方式内置于 TL 语言中。任何组合子的声明中都可以使用形如 [数组字段名":" ] [ nat-ident * ] "["字段描述... "]” 的子结构，其中nat-ident是之前遇到的任何 # 类型字段的名称（如果未显式指定，则使用最近一次遇到的字段）。抽象而言，此子结构等价于：

aux_type *field-descr* ... = AuxType;
*current_constructor* ... [ *array-field-name* ":" ] (%Tuple aux_type *nat-ident*)

例如，10x10矩阵、向量和任意矩阵可以按如下方式定义：

matrix {X:Type} m:# n:# a:n*[ m*[ X ] ] = Matrix X;
matrix_10x10 a:10*[ 10*[ double ]] = Matrix_10x10;
vector {X:Type} # [ X ] = Vector X;

我们已经遇到过最后一个版本，它是“内置类型”的“定义” Vector。

当然，重复部分可以包含多个字段，其复杂程度可根据需要而定。此外，除了使用n作为重复计数器之外，还可以使用形如(n+const)和(const+n)的表达式，其中const是一个较小的非负常数，它们是S (S ( ... (S n) ... ))的简写：

repeat_np1 n:# a:(S n)*[ key:string value:string ] = Dictionary;

为了计算 CRC32 值，这些表达式会被转换为不带内部空格的表达式(const+X)。此外，*在这种情况下，表达式左右两侧也不用空格隔开。

依赖类型的序列化

序列化依赖类型和多态类型并非根本性的挑战：我们有具有非零元数和类型值的组合子。例如，类型Tuple double 10 : Type可以序列化为'Tuple' '%double' 10。需要注意的是，目前在实践中几乎没有必要序列化类型，无论它们是否依赖。

TL 中的可选组合器参数

TL 中的可选组合器参数必须具备以下属性：

• 可选参数必须恰好是组合器的前几个参数；

• 任何可选参数的值必须完全由组合器的结果类型决定。

例如，cons {X:Type} hd:X tl:(list X) = list X参数X可以设为可选，因为它位于参数列表的最开头，并且由list X结果类型明确决定。类似地，tcons {X:Type} {n:#} hd:X tl:(%Tuple X n) = Tuple X (S n)X 和 n 的值也完全取决于Tuple X (S n)结果类型，因此它们也可以设为可选参数。

通常情况下，将满足第二个条件的所有构造函数参数移到列表开头，并按照它们在结果类型参数中出现的顺序排列，然后将它们设为可选参数，这样是合理的。采用这种方法，构造函数的完整版本很少需要——只有当我们想将多态类型或依赖类型的值作为 Object 类型的值传递时才需要。在所有其他情况下，上下文中预期值的类型已经已知，这意味着所有可选参数都可以在分解过程中恢复。