TL类型语言的二进制序列化和抽象TL类型

TL 语言以通用类型理论（更准确地说，是 Martin-Löf 的依赖直觉类型理论）的精神定义了抽象数据类型，但并未规定这些类型的值在内存中、保存到磁盘时或通过网络传输时应如何表示。与之相反，关于二进制序列化的文章讨论了抽象类型值的有效序列化问题。为此，具体类型或序列化类型被定义为对应抽象类型所有可能值的序列化集合。在这种情况下，序列化值取自字母表A中的单词集合 A* ，该字母表由 2^32 个字符（即 32 位整数）组成。

为了在 TL 语言中使用 TL 模式（例如“程序”）来描述抽象类型的值的序列化，我们应该解释具体类型[T]（A^* 的子集[T] ）如何与抽象类型T （在 TL 中定义）关联，以及抽象类型T的值如何对应于具体类型[T]的值（即[T]的元素）。

序列化是指根据抽象类型T的值构造[T]的元素的过程。反序列化是相反的过程。

抽象类型T的值可以用不同的方式表示。通常，内存中会使用某种树或图，或者，如果需要，可以使用一组节点，每个节点包含一个特定的标签（“节点类型”）以及指向其他节点和/或内置基本类型（例如 `T`）值的多个指针。然而，为了便于讨论，将抽象类型Tint的值写成字符串（更具体地说，是 S 表达式）会更方便。回想一下，S 表达式可以是原子（基本类型的值，例如用引号括起来的整数或字符串常量；或者对应于内置函数或自定义函数的标识符），也可以是以空格分隔并以括号结尾的 S 表达式列表。在我们的例子中，我们使用 S 表达式，其第一个元素是组合器标识符，而其余元素（数量取决于组合器的元数）是表示所选组合器字段（或参数）元素的 S 表达式。此外，参数的 S 表达式的类型和结果的 S 表达式的类型（例如关联表达式）必须匹配。

例如，对于该模式 

pair x:int y:int = Pair;
pnil = PairList;
pcons hd:Pair tl:PairList = PairList;

以下是抽象类型的示例PairList，以 S 表达式的形式编写： 

(pnil)
(pcons (pair 2 3) (pcons (pair 9 4) (pnil)))

我们通常写成E : T（读作“类型为T的E ”）来表示E是类型为T的值。我们假设存在一个内置类型Type，它的值也是类型。因此，写成T : Type表示T是一个类型。

例如，我们可以这样写： 

PairList : Type;
(pcons (pair 2 3) (pcons (pair 9 4) (pnil))) : PairList;

一般来说，将抽象值转换为序列化值很简单（如果需要，可以通过归纳法定义）：

如果我们用[T]表示与抽象类型T对应的具体类型，用[E]表示[T]中对应于类型T的值E的元素，那么最后一条规则可以写成：

内置的带颜色类型的值会像使用 `&` 和 `&` 定义一样进行序列化，Int也就是说，整数常量或字符串的序列化前面会加上 `&`或`& ` 组合子（构造函数）的编号。在 S 表达式中，这可以写成 `&`或 `&` 。Stringint x:int = Int;string s:string = String;intstring(int 5)(string "Test")

然而，上述描述并未涵盖某些细微之处，例如裸类型的存在，以及函数（可归约的主动组合器，例如计算型组合器）和构造函数（无归约规则的被动组合器）之间的区别。此外，我们也没有解释如何处理多态类型和可选的组合器参数。现在我们将尝试解释这些问题。

常数、表面值和函数值

通过将组合子分为构造函数和函数，我们可以引入以下抽象类型T的表达式（值）类别：

在实践中，我们最常需要的是常量值（用于存储和传递任何数据结构，特别是 RPC 查询的响应）和表面表达式（例如，作为 RPC 查询：外层函数组合器是我们想要调用的 RPC 函数的名称，而它的参数是调用该函数的实参，这些实参是常量值）。在某些情况下，任意函数表达式也很有用（例如，当我们想要将一个 RPC 查询的结果远程传递给另一个 RPC 查询时）。

我们将使用c(T)来表示抽象类型T的子类型，其值为类型为T的常量表达式。显然，c(T)拥有与T本身大致相同的构造函数（所有参数Ti的类型都被c(Ti)替换） ，但它没有函数组合子。

类似地，我们将用f(T)表示T的一个子类型，其值是T类型的表面表达式。显然， f(T)的组合子本质上是T类型的函数组合子，但c()适用于这些组合子参数的类型：组合子A : T1->...->Tr->T变为A' : c(T1)->...->c(Tr)->f(T)。（参见下文对此规则的解释。）

因此，我们定义了两个“函数” c : Type -> Type和f : Type -> Type，使得对于所有 T : Type，c(T) :- T且对于所有 T : Type，f(T) :- T （写成T :- T'表示T包含在T'中，或者T是T'的子类型）。

我们将假设c和f是幂等的。

裸露类型

从抽象类型理论的角度来看，裸类型（与内置的原始类型如 `int`int和 `int`相对string）是不必要的。然而，它们在实践中却非常有用。

因此，TL 引入了（部分定义的）幂等一元运算符，它将一个标准泛函（例如类型为...->Type或简称为Type%的表达式）转换为相同类型的另一个标准泛函。如果T是一个类型，那么从抽象的理论角度来看，它等价于c(T)。换句话说，的值是T的常量值。如果T是一个k元标准表达式，那么T : S1 -> ... -> Sk -> Type，其中每个Si=Type或#，那么根据定义，它也是一个具有相同元数的k元标准表达式，由等式(%T) a1 ... ak = % (T a1 ... ak)定义。%T%T%T

当序列化一个类型为 `T` 的常量值时，它首先被序列化为类型为`T`%T的值（假设`T`本身不是裸类型）。然后，序列化结果的第一个字符会被丢弃（例如，封闭组合子的名称）。因此， `T: S1 -> ... -> Sk -> Type`仅当 `T` 只有一个构造函数时才是一个有效的类型表达式。表达式` T: S1 -> ... -> Sk -> Type`是有效的，当且仅当对于任意参数组合`a1 : S1, ... , ak : Sk` ，类型`T a1 ... ak`只有一个构造函数。在其他情况下使用`T: S1 -> ... -> Sk -> Type`是不正确的。%T%T%T%

如果对于参数a1 : S1, ..., ak : Sk的每个值，都存在唯一构造函数C来表示T a1 ... ak，那么 TL 允许使用`T a1 ... ak`C a1 ... ak代替 ` T a1 ... %T a1 ... akak`或 `T a1 ... ak` %(T a1 .. ak)。换句话说，在某些情况下，标识符 `T a1 ... ak`C是 `T a1 ... ak` 的同义词%T。这仅在类型上下文中允许（在指定组合器字段或结果的类型时）。

此外，假设%Int = int和%String = string。

!修饰符

在 TL 中，幂等运算符!可以修改任何类型，实际上允许在其常量值序列化时使用表面值。但是，如果T是一个标准函数，例如S1->..->Sr->Type，则!T使用等式定义(!T) a1 ... ar = !(T a1 ... ar)，对于任何a1:S1 , ..., ar:Sr。

该!运算符仅允许用于函数组合子字段类型的定义中。它通常用作类型前缀，例如： 

set_timeout {X:Type} timeout:int f:!X = X;

在这种情况下，set_timeout“包装器”已定义。它接受两个显式参数：整数timeout和类型为 `.X:Type` 的表面表达式X。`X :Type`本身是一个隐式参数（它没有显式声明，而是从其他参数的值及其类型推断得出）。类似的包装器可能有助于修改 RPC 查询（各种类型的表面表达式）的操作。例如，假设我们有以下函数： 

factorial n:int = int;

然后我们可以将 RPC 查询包装(factorial 100)如下：(set_timeout 200 (factorial 100))。此表达式仍然是类型为的表面值int，这意味着它可以作为 RPC 查询传递。

连续两次计算是另一个例子： 

pair {X Y : Type} x:X y:Y = Pair X Y;  // constructor
seq_pair {X Y : Type} x:!X y:!Y = Pair X Y; // functional wrapper for sequential computation
par_pair {X Y : Type} x:!X y:!Y = Pair X Y; // functional wrapper for parallel computation

现在，RPC 查询(seq_pair (factorial 2) (factorial 3)) : Pair int int首先计算 2 的阶乘，然后计算 3 的阶乘，并返回结果对(pair 2 6)。在这种情况下，操作顺序并不重要，因为它们没有副作用。使用 `________` 也完全可以(par_pair (factorial 2) (factorial 3))。然而，情况并非总是如此。

我们还可以将其类比为“逗号”操作： 

comma {X Y : Type} x:!X y:!Y = Y;

例如，此操作可以先计算x，然后忘记结果，再计算y，然后返回y。

seq_pair请注意，`\t` 、` \t`par_pair和`\t` 包装器的语义comma确实是在它们实现的地方定义的（就像所有其他函数组合器的语义一样），而不是通过它们的 TL 声明定义的。

原则上，类似这样的多态包装器set_timeout也可以用于例如“注释”RPC响应的常量值。例如，服务器可能会返回查询响应以及计算时间。但是，类型为!X的值必须是常量，因为这是封闭表达式期望的值。换句话说，当且仅当E本身是类型为X的常量/表面值时， !Xset_timeout 239 E才是常量/表面值。

$修饰符

幂等修饰符$允许在通常只允许使用常量或表面值的上下文中使用任意适当类型的函数值。它会递归地转换所有涉及类型的所有组合子，取消原有操作%，并将$所有组合子的参数类型和结果附加到原有类型（$也会添加到转换后的组合子的前面）。此外，内置类型也会被转换（在最后阶段）：$int = Int和$string = String。

这可能有助于创建 RPC 查询，该查询对传递给它的表达式执行“深度计算”： 

compute {X:Type} expr:$X = X;

例如，现在我们可以将以下内容作为 RPC 查询发送： 

(compute ($factorial ($factorial (int 3)))) : int

（注意，这三个元素都穿上了衣服；组合子 $factorial 的类型为 $int -> $int）。

这是一个非常强大的工具。它不需要在非常简单的TL版本中实现。$目前使用的TL模式中还没有遇到它。

关于修饰语的更多信息

事实上，至少就序列化应用而言，TL 语言默认会在所有组合器的参数类型和结果周围添加 ` c()! ` 修饰符，而 `\cdot`和`\ddot`$则会取消它（更准确地说，!它们只会取消，并且在某种意义上$反转其含义）。这就是为什么 TL 中没有显式的 `\cdot`c()修饰符，以及为什么除非另有说明，否则假定所有函数都只接受常量值并返回常量结果。

你可能会认为某些函数组合器可能具有诸如 `T` 之类的类型partial_factorial n:int = $int;，并且 RPC 查询(partial_factorial 3)可能会意外地返回($product (int 3) ($product (int 2) ($product (int 1) (int 1)))) : $int……

!或许更准确的说法是，可以这样理解修饰符。所有类型最初都只包含常量值（以及构造函数）。!修饰符会从每个类型创建一个新类型（与其对应的类型）。这个新类型没有固有的构造函数。函数式组合器与构造函数的区别在于，它!会在其结果类型的前面隐式地添加一个修饰符。之后，表达式的计算过程（无论是局部的还是远程的）都可以使用多态函数来表示eval : !X -> X。

可选组合器参数及其值

请参阅可选组合器参数及其值。