Nathan Linger：Ontology，一套面向语言的权限系统

Ontology 是我们在 Jane Street 为权限管理和其他共享配置设计的系统。它在两个层面面向语言：内部使用类型理论中的依赖类型语言；外部隐藏这套语法，用英语呈现信息。

内部语言描述类型和声明，但大多数用户并不想阅读类型理论的语法。因此，我们在界面中隐藏它，改用熟悉的英语呈现，同时保留这门语言作为整个系统的共同基础。

系统询问某个领域中有哪些实体、它们之间存在什么关系、人们想作哪些更改，以及需要谁批准。有些配置存放在 Ontology 中，供其他系统获取；另一些相关信息则从它无法控制的外部系统导入。

用户可以查看现有权限，并提出更改请求，例如申请自己尚未拥有的访问权限或创建用户组。Ontology 查询负责审批的人，向他们发送邮件；必要人员批准后应用更改，也允许他们拒绝请求。

为解释数据，我区分名词和命题：前者是讨论的事物，后者是关于这些事物的陈述。我还区分数据的定义方式：通过表枚举、通过逻辑规则，或者作为系统内置的原语。

表与规则的区别在于信息的定义方式。表枚举实例，规则描述实例如何构造或推导；原语则由实现本身提供。

由表定义的名词可以是用户、Mercurial 仓库或用户组列表。演讲中的例子有意使用了一个很小的虚构世界。这类数据有很多来自 Ontology 之外的系统。

表也可以定义命题。用户组成员关系表中的每一行，都断言某个用户属于某个组。表枚举了这一关系成立的实例。

另一张表授予某个用户集合访问仓库的权限。用户集合是更有意思的名词：规则可以从组的所有成员构造它，也可以从一个用户构造单元素集合。两种方式都很有用，因为权限可以授予组或个人。

这两个用户集合构造器回应了实际需求：向组授权和向个人授权，都应适用于同一种权限关系。它们的内部表示不同，但都是用户集合类型的值。

接下来可以用相应规则定义用户集合的成员关系。用户属于自己的单元素集合；属于某个组的用户，也属于由该组全部用户组成的集合。

个人的仓库访问权限可由这些定义推导。如果用户属于某个获准访问仓库的用户集合，该用户就可以访问仓库。规则展开这一关系，无需另建一张表列出每个人推导得到的权限。

子集类型也是有用的模式。先定义一个命题说明用户何时可以交易——在这个例子中是属于 traders 组。再把 trader 定义为用户以及该用户可以交易的证据，使其他数据能够专门引用 trader。

把 trader 定义为用户的子集后，另一张表就可以将条目限制为 trader，而不是任意用户。规则和证据让这个更窄的范围变得明确。

这些类别并不是严格的单向层级。表定义的事实可以包含由规则构造的用户集合；像 trader 这样的名词也可以依赖命题。这些定义可以以有用的方式相互依赖。

通常命题用名词定义，规则建立在表数据之上，但这些例子有意跨越了边界：表可以提到规则定义的对象，规则定义的名词也可以包含命题。

原语是系统提供的类型和命题，不通过表或规则定义。原语名词的例子包括端口号和 IP 地址范围，在配置防火墙规则或网络带宽时很有用。

表加原语类型大致相当于关系数据库；仅有规则则类似 Prolog 的一个变体。将表、规则和原语结合，就得到我所说的演绎数据库。它支持子集和递归定义关系等模式。

例如，邮件列表可以订阅其他邮件列表。要找出用户所属的所有列表，我们可能需要反复沿这些链接查找。递归规则可以自然地表达这种传递闭包。

在介绍内部表示之前，先看 OCaml 或 Haskell 中的变体类型。布尔值有 true 和 false 两个构造器；退出码可以是 success，或携带整数的 error。递归树可以是包含字符的叶子，或包含子树和整数的节点。

退出码构造器展示了携带额外数据的选项，树的例子则通过递归引用构造任意更大的树。演讲重点是构造这些值，而不是对它们进行模式匹配。

这些构造器创建相应类型的值。Ontology 的语言通过常量及其类型的声明表达类似思想，语法受到 S-表达式启发。error 构造器接收一个整数，然后产生退出码；嵌套构造器可以建立树。

在内部语言中，冒号连接声明名称及其类型。类型及其构造器都作为常量引入；把构造器应用于参数就能建立项，与变体例子类似。

用户表可以表示为一个类型和有限的用户常量声明列表。Ontology 在这种表示中区分两种类型：名词和命题。注解还区分外延性的表式定义与通过规则给出的内涵性定义。

用户组成员关系命题以组和用户为参数。表中的每一行都变成一个声明，其类型表达特定的成员事实。系统为常量生成名称，关系的重要信息则包含在它的类型中。

例如，一个用户属于人力资源组的成员行，其命题以这个具体的组和用户为参数。生成的标识符为这个命题类型的项命名，因此可以作为该事实的证明重复使用。

这个生成名称之后可以作为事实证据：系统查找它，并验证其类型是否为预期命题。这些声明类似广义代数数据类型，因为构造器针对不同参数可以产生相关但不完全相同的类型。

规则定义的用户集合变成具有构造器的内涵名词类型。一个构造器把组包装为全体成员的集合，另一个把用户包装为单元素集合。两者都返回相同的用户集合类型，类似普通变体构造器。

这两个用户集合构造器是返回相同类型的普通选项。这比成员事实简单，因为成员事实的命题类型会随每一行中的值变化。

仓库访问表现在可以引用这些构造出的用户集合。每一行仍然是带生成名称的命题，但其参数包含全组成员集合或单元素集合。类型检查器确保仓库和用户集合参数具有预期类型。

由于构造器与其类型位于同一作用域，系统可以推断构造器路径的一部分。这让表示省去部分重复限定，同时仍能检查所选名称是否具有所需类型。

接下来，用内涵性命题表示用户集合成员关系。每条英语规则变成一个构造器：一条说明用户属于自己的单元素集合，另一条利用组成员事实建立用户属于该组派生集合的结论。

单元素成员关系的构造器接收一个具体用户，产生关于同一用户的命题。它的结果类型依赖参数值。这就是新特性：把构造器应用于不同用户，会得到不同的命题类型。

依赖函数类型为参数命名，使类型后面的部分可以引用它。这让单元素规则不只是说某人属于某个单元素集合，而是说这个特定用户属于自己的单元素集合。

组规则同样表示：对于一个组和一个用户，用户属于该组的证据可以建立其属于组派生用户集合的结论。其他规则也用同一模式，从用户集合的权限推导个人仓库权限。

表示 trader 的子集将用户与该用户可以交易的命题证据打包在一起。构造一个类型为命题的项，实际上就是构造证明，因此证据成为数据的一部分，而不是非正式假设。

所有这些信息都是类型语言中的一系列声明。类型检查器可以验证声明是否格式良好，我们希望数据变化时这一性质始终保持不变。

一个简单的失败情况是声明引用了已不存在的常量。因此，删除用户组需要清理指向它的引用：组成员事实、基于该组的用户集合，以及依赖这些集合的仓库权限。

级联清理可以防止无意义数据积累，但删除也可能代价高昂。所介绍的实现会将删除项目保留一段时间，约两周，而不是立即永久丢弃。

读取权限也沿依赖关系传播，方向则相反。展示一个常量之前，系统检查读者是否有权查看它所引用的内容。我把结果描述为个性化视图：不可访问的数据及其依赖项就像已被移除一样。

这个过滤视图是对读者能够观察到的数据所作的保证。传递检查依赖关系很重要，因为一个看似无害的声明可能泄露它所引用的实体。

一个查询可以寻找用户、用户集合和仓库，要求用户属于该集合，且该集合有权访问仓库。用英语表达时，这些是受命题约束的名词；返回的行展示匹配组合。

在内部，查询是一个逻辑公式，断言所需类型的值存在并满足指定关系。为建立这一点，系统寻找值和命题证据。展开后的结果包含证明对象，而面向用户的结果只展示名词数据。

对于一行结果，一个有名称的表事实可以证明仓库访问权限，单元素构造器则可以证明用户属于该单元素集合。每份证据都以相应命题为类型，从而将结果与声明联系起来。

更改方式取决于数据类型。对于由 Ontology 管理的外延数据，用户可以提交请求，进入审批流程；由其他系统控制的外延数据则按计划导入。

更改获得批准后，其他系统可以与 Ontology 同步。创建组、更改关系或授予仓库权限便能影响外部世界；例如，权限同步后，仓库克隆可能就能成功。

普通用户不能直接更改由规则定义的非外延数据。修改这些定义需要引入新版本、迁移旧数据并切换可见性，同时考虑哪些客户端仍依赖旧表示。

英语渲染刻意保持简单。每个构造器都有一个字符串模板，递归渲染后的参数填入其中的空位。系统只了解完成任务所需的少量英语语法，因此有些表达不够完美；更复杂的自然语言生成器可以改进它们。

渲染过程是递归的：系统得到构造器参数的英语短语后，将它们插入该构造器的模板。我把这看作简单的工程选择，而非对自然语言语法的完整处理。

为了演示，我使用一个只包含上述例子的小型私有 Ontology 副本。命令行环境经过设置，便于调用查询命令。我想找出 developers 组成员能够访问的仓库。

交互式查询构建器提供以英语呈现的模板。我选择仓库访问，再添加组成员条件。起初两个条件彼此独立，工具警告它们尚未连接成一个查询。

我将两个条件中的用户变量连接起来。界面依据类型提供兼容选项，然后我把组限定为 developers。得到的查询寻找该组的用户、包含该用户的用户集合，以及通过该集合可访问的仓库。

初始结果显示，这个小例子里的 developers 无法访问代码仓库。我通过网页界面请求让 developers 用户集合访问 OCaml 代码仓库。

请求指出需要哪位所有者批准。我在另一个所有者会话中批准它。查询构建器还生成了可重复使用的内部查询，因此无需重建所有条件就能再次运行；新结果显示 developers 获得了代码仓库访问权限。

网站还允许用户浏览一个组，以及提到它的规则或事实。例子中，我查看 traders 组、定义谁可以交易的规则、其成员和相关仓库权限。底层声明始终以英语呈现。

这种面向语言的设计带来了什么？演绎数据库支持包括传递闭包在内的表达力丰富的查询。数据驱动的界面可以为用户呈现同一组声明，尽管简单的英语模板仍有粗糙之处。

构建请求和查询时，界面会提供有效选项：需要用户组时列出用户组，需要用户集合时列出可构造它的构造器。由于界面受类型系统驱动，它生成格式良好的结构，而不要求用户编写内部语言。

上传声明就能增加新的权限和配置类型，无需改动核心系统。通用结构还支持适用于多类请求的测试，而不必为每种请求单独编写测试。

例如，用户应能放弃自己的权限，而不需要其他人批准。我们可以编写一项通用测试：为每个权限移除请求代入请求者，并检查它能否在没有额外批准的情况下继续。这个测试曾发现 bug。

一个主要缺点是 DSL 核心类似 Prolog 的搜索具有图灵完备性。用来确定审批人的查询理论上可能永远运行下去。我们施加抽象的执行预算，防止查询消耗无限工作量。

这个限制让人安心，却也可能仅因为一个有效查询比以前的例子需要更多工作，就拒绝它。一种可能的改进是把预算更集中地用于递归类型和有问题的递归，而不是像现在这样广泛施加细粒度限制。

自定义 DSL 还需要实现和维护。Ontology 结合了数据库与编程语言的特性，因此我们不得不重新实现两者的一部分。好在底层方法——常量构成的依赖类型语言，加上 Prolog 风格的回溯——是人们熟知的方法，而不是全新的发明。

我们有意将所表示的数据保持为一阶，而更激进的学术系统探索高阶数据。这种克制有助于控制实现的复杂度。最终结果是数据、查询、更改请求和普通语言界面共享的类型化基础。