TL中的多态性

需要注意的是，在绝大多数 API 调用的 TL 架构中，多态类型的使用仅限于 Vector 类型。尽管如此，了解整体架构仍然很有帮助。

普通归纳类型

例如，我们考虑如下定义的 IntList： 

int_cons hd:int tl:IntList = IntList; int_nil = IntList;

“int_cons”和“int_nil”构造函数以及“IntList”类型本身都是以下类型的表达式（写成 A : X 表示 A 是类型为 X 的表达式）： 

IntList : Type; int_cons : int -> IntList -> IntList; int_nil : IntList;

关键字 ` Type`用于表示所有类型的类型。请注意，`Type` 不是 `Object`（`Object` 是所有项的类型）。以下是其他一些函数式编程语言（但不是 TL）中可以使用的替代语法： 

NewType IntList := | int_cons hd:int tl:IntList | int_nil EndType

多态型

TL 支持以下版本（花括号表示可选字段，详见下文）： 

cons {X:Type} hd:X tl:(List X) = List X; nil {X:Type} = List X

以下是其他具有依赖类型的函数式语言的另一种表述方式： 

NewType List {X:Type} := | cons {X:Type} hd:X tl:(List X) | nil {X:Type} EndType

总之，从类型形式理论的角度来看，这些变体彼此等价，并可由此定义以下术语： 

List : Type -> Type; cons : forall (X:Type), X -> List X -> List X; nil : forall (X:Type), X -> List X;

在每种情况下，请记住，“A -> B”是“forall (x : A), B”的简写形式，其中 x 不属于 A 和 B 中的任何变量。例如，“cons”类型可以写成如下形式： 

cons : forall (X:Type), forall (hd : X), forall (tl : List X), List X

或者更简洁地说： 

cons : forall (X : Type) (hd : X) (tl : List X), List X

参见构造演算。支持类似构造的依赖类型函数式语言的例子有Coq和Agda。

在这种情况下，全称量词后的条目比箭头后的条目更与内容相关，因为量词绑定的变量名被用来传递构造函数中相应字段的名称，即使该变量在量词下的表达式中没有被使用。从结构上看，所有这些“cons”类型的条目都是等价的。

类型序列化（类型为 Type 的值）

如我们所见，要序列化通过应用组合器“cons X:Type hd:X tl:(List X) = List X”获得的 List X 类型的值，我们需要：

  1. 将“cons”组合器的名称序列化为32位数字；
  2. 如果 X 是必需参数，则将 X 序列化为类型（即类型为 Type 的值）；
  3. 将列表的头部（hd）序列化为 X 类型的值；
  4. 将列表的尾部序列化为多态类型 List X 的值。

第一步，自然而然的问题是，究竟要用哪个字符串来计算 CRC32。建议采用cons X:Type hd:X tl:List X = List X不带终止分号和任何括号的“ ”（封闭类型表达式会根据其构造前缀明确地重建）。

最后一步，我们递归地解决了序列化类型为 List X 的值的相同问题；我们将基于被序列化值构造过程中的归纳假设，认为该问题已解决。同样，我们将认为第三步也是可以理解的（被序列化值构造过程中的归纳）。

我们仍然需要描述如何传输（序列化）类型，例如类型为 Type 的值。TL模式中的类型目前仅作为构造函数的可选参数出现，因此永远不会被显式序列化。相反，它们的值是从先前已知的待序列化值的类型推断出来的。

为了完整起见，我们将描述如何序列化类型（类型为 Type 的值）。但是请注意，目前这些信息尚无实际用处。请参阅类型序列化。

多态构造函数中的可选参数

前面提到，任何构造函数的（前几个）参数都可以被标识为可选参数（通过用花括号括起来），但这种说法并不完全准确。首先，这些可选参数只能是 `int`Type或#`int`（自然数）类型。其次，可选参数必须与返回值类型相同，否则无法确定它们的值。

请注意，`@'''constr-id'''` 表示构造函数的“完整形式”（其中所有可选参数都变为必需参数），而 `'''constr-id''` 表示其简写形式（不包含可选参数）。如果没有可选参数，则这两种形式相同。目前构造函数的完整形式从未被使用。

裸多态类型

这里有个小问题：如果我们想要序列化裸类型 '%pair string int' 或 '%pair string Y' 的值（在 TL 中通常简称为“pair”，但 '%Pair' 的形式更佳），我们不能同时使用完整的构造函数 @pair 和部分构造函数 pair，因为构造函数的名称不会被序列化。因此，我们必须区分裸类型 %@pair（序列化类型 X、类型 Y、值 x:X 和值 y:Y）和 %pair（仅序列化 x:X 和 y:Y；类型 X 和 Y 从上下文中可知）。实际上，我们几乎总是需要裸类型 %pair，而这正是 TL 中“pair”在类型上下文中的含义。因此， 

record name:string map:(List (pair int string)) = Record;

序列化结果将大致符合我们的预期（列表元素的序列化将由整数序列化和字符串序列化组成，不包含任何额外的头部、类型或组合器名称）。顺便一提，在计算上述示例中组合器“record”的名称时，会计算其 CRC32值record name:string map:List pair int string = Record。

另请注意，这种类型的更精确描述应该是： 

record name:string map:(List %(Pair int string)) = Record