MTProto 移动协议 TL组合子的正式描述

主条目：TL 的正式描述。另见TL 语言。

TL 中的组合子声明如下：

combinator-decl ::= full-combinator-id { opt-args } { args } = result-type  ;
full-combinator-id ::= lc-ident-full | _
combinator-id ::= lc-ident-ns | _
opt-args ::= { var-ident { var-ident } : [ excl-mark ] type-expr  }
args ::= var-ident-opt : [ conditional-arg-def ] [ !] type-term 
args ::= [ var-ident-opt : ] [ multiplicity * ] [{ args } ]
args ::= ( var-ident-opt { var-ident-opt } :[ !] type-term  )
args ::= [ !] type-term 
multiplicity ::= nat-term 
var-ident-opt ::= var-ident | _
conditional-arg-def ::= var-ident [ . nat-const ] ?
result-type ::= boxed-type-ident { subexpr } 
result-type ::= boxed-type-ident  < subexpr { , subexpr }>

我们将阐明这一切意味着什么。

• 组合子标识符要么是以小写拉丁字母开头的标识符（lc-ident），要么是以命名空间标识符（也是lc-ident）开头，后跟一个句点和另一个lc-ident。因此，cons和lists.get都是有效的组合子标识符。

• 组合器有一个名称，也称为数字（不要与名称混淆）——一个 32 位数字，用于唯一确定组合器。该名称可以自动计算（见下文），也可以在声明中显式指定。为此，需要#在所定义组合器的标识符后添加一个井号 (#) 和 8 位十六进制数字（即组合器的名称）。

• 组合器的声明以它的标识符开头，其名称（用井号分隔）可以添加到标识符之后。

• 在组合器标识符之后是声明的主要部分，它由字段（或变量）的声明组成，包括对其类型的指示。

• 首先是可选字段的声明（可以有多个可选字段，也可以没有可选字段）。然后是必需字段的声明（也可以没有必需字段）。

• 任何以大写或小写字母开头且不包含命名空间引用的标识符都可以是字段（变量）标识符。对于变量类型，使用大写字母作为标识符，对于其他变量，使用小写字母作为标识符是一种良好的实践。

• 接下来，组合器声明包含等号 ( =) 和结果类型（可以是复合类型，也可以是首次出现）。结果类型可以是多态的和/或依赖的；已定义构造函数的任何类型字段Type（#作为子表达式）都可以返回。

• 组合器声明以分号结尾。

在下文中，构造函数的字段、变量和参数都指同一事物。

可选字段声明

• 这些字段的形式为{ field_1 ... field_k : type-expr }，其中field_i是组合器声明范围内唯一的变量（字段）标识符，而type-expr是所有字段共享的类型。

• 如果k>1，则此条目在功能上等同于{ field_1 : type-expr } ... { field_k : type-expr }。

• 所有可选字段必须明确命名（不允许使用field_i_代替）。

• 此外，目前所有可选字段的名称必须与组合器的结果类型相同（可能不止一次），并且它们本身必须是类型#（即nat）或Type。因此，如果确切的结果类型已知，则可以确定组合器所有隐式参数的值（2=3这样做可能会得到形如的矛盾，这意味着组合器在上下文中是不允许的）。

必填字段声明

• ( 这些字段可能采用field_1 ... field_k : type-expr 的形式)，类似于可选字段声明，但带有括号。此条目等效于( field_1 : type-expr ) ... ( field_k : type-expr )，其中字段逐个定义。

• 下划线符号 ( _) 可以用作一个或多个字段 ( field_i ) 的名称，表示该字段是匿名的（确切的名称并不重要）。

• 字段可以像这样声明，而无需外层括号：field_id : type-expr。但是，如果type-expr是复杂类型，则可能需要在type-expr周围加上括号（这在 BNF 中有所体现）。

• 此外，可以使用type-expr条目声明一个匿名字段，其功能与_ : type-expr等效。

• 必填字段声明一个接一个地出现，用空格分隔（更准确地说，是用任意数量的空白符号分隔）。

• 已声明字段的类型（类型表达式）可以使用已声明组合器先前定义的变量（字段）作为子表达式（即参数值）。例如：

  nil {X:Type} = List X; cons {X:Type} hd:X tl:(list X) = List X; typed_list (X:Type) (l : list X) = TypedList;

重复

• 这些参数只能存在于必需参数中。它们的形式为 [字段 ID : ] [多重性 *] [ args ]，其中args的格式与组合器声明的（多个）必需字段的格式相同，只是封闭组合器先前声明的所有字段都可以在参数类型中使用。

• 可以指定接收重复值作为值的封闭组合器的字段名称（字段 ID），也可以绕过该字段，这相当于使用下划线符号作为字段 ID。

• 多重性字段是一个类型为#( nat) 的表达式，它可以是实数常量、前面类型为 的字段的名称，或者形如c v#的表达式，其中c是实数常量，v是类型为 的字段的名称。多重性字段的作用是提供（重复）向量的长度，该向量的每个元素都由args中枚举的类型值组成。( + )#

• 可以绕过重数字段。在这种情况下，#将使用封闭组合器中最后一个前导参数（必须如此）。

• 从功能上看，重复字段 ID : 多重性 * [ 参数等价于单字段 字段 ID多重性]的声明，其中是一个辅助类型，其新名称定义为。如果封闭类型的任何字段在参数中使用，则它们将作为第一个（可选）参数添加到辅助构造函数及其结果类型中。( : %Tuple %AuxType )aux_typeaux_type *args* = AuxTypeaux_typeAuxType

• 如果args由一个类型为some-type的匿名字段组成，则可以直接使用some-type代替%AuxType。

• 如果在实现过程中按照上述方式重写重复项，那么使用 `and` 而不是aux_type`and`是合乎逻辑的AuxType，`and` 是一些标识符，其中包含正在定义的外部组合器的名称和重复项在其定义中的索引号。

例子：

matrix {m n : #} a : m* [ n* [ double ] ] = Matrix m n;

在功能上等同于

aux_type {n : #} (_ : %Tuple double n) = AuxType n; matrix {m : #} {n : #} (a : %Tuple %(AuxType n) m) = Matrix m n; 

此外，内置类型Tuple可以Vector定义为：

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; 

实际上，以下等效条目被认为是定义Vector（即，正是此条目用于计算vector构造函数及其偏函数的名称）：

vector {t : Type} # [ t ] = Vector t;

如果我们用展开它Tuple，就能得到前面的定义。

条件字段

施工

	args ::= var-ident-opt : [ conditional-arg-def ] [ !] type-term 
conditional-arg-def ::= var-ident [ . nat-const ]?

允许分配仅当前面类型为 `T` 的必填或可选字段的值不为空（或者，如果应用了#特殊的二进制位选择运算符，则其所选位不为零）时才存在的字段。示例：.

	用户 {fields:#} id:int first_name:(fields.0?string) last_name:(fields.1?string) friends:(fields.2?%(Vector int)) = User fields; 
get_users req_fields:# ids:%(Vector int) = Vector %(User req_fields)