如今的知识图通常依赖于本体（例如OWL）来定义类和关系，并使用约束语言如SHACL来验证数据形状。但是这种方法在表达力和集成方面有一些已知的局限性。依赖类型理论（DTT）提供了一个统一的类型系统，这个系统足够强大，可以同时处理本体、数据模式和逻辑。DTT就像一个升级版的编程语言类型系统，可以直接在其类型中编码复杂的规则，比如“出生日期必须早于死亡日期”。对于AI和知识图谱的从业者来说，这意味着他们可以在数据录入阶段就发现不一致之处，而不是在单独的验证步骤中。本文将以简单易懂的方式介绍DTT，并探讨它如何增强甚至取代传统的OWL本体和SHACL验证。

从根本上说，依赖类型理论是一种类型系统，其中类型可以依赖于值或条件。换句话说，程序的类型定义可以包含实际的数据条件。这在像 Coq、Agda、Idris 或 Lean 这样的证明辅助语言中很常见。例如，在依赖类型的语言中，可以有一个类型 Vector(n)，表示“长度为 n 的向量”。这里的 n 是类型中的值，因此 Vector(3) 和 Vector(4) 是不同的类型。这让类型系统能够自动确保数组长度的一致性。

对于知识的表达方式，我们可以做一个类比：想象将你的知识图谱实体和关系视为编程语言中的变量值，并采用类型系统来保证你的本体规则。依赖类型具有极强的表达能力——可以表达子集规则、关系或任何规则作为类型定义的一部分。从实际应用的角度来看，依赖类型可以理解为一种自带逻辑的类或框架。

具体来看，考虑一个简单的例子（如下伪代码所示，使用一种具有 DTT 特性的语言）：如下

    // 伪代码定义了一个Person类型，该类型具有依赖约束
    type Person(name: String, birthDate: Date, deathDate: Date?)
    . // 如果提供了deathDate参数，则要求birthDate必须早于deathDate
    . requires (deathDate == null) 或 (birthDate < deathDate).

在这里，Person 是一个包含 name、birthDate 和可选 deathDate 字段的类型。有趣的是 requires 子句：它是一个逻辑条件，成为类型的一部分。任何声明为 Person 的数据必须满足这条 birthDate 早于 deathDate 的规则（如果存在死亡日期）。在 DTT 中，这样的条件作为类型检查的一部分由编译器或解释器来检查——就像违反类型规则会导致编译错误一样。对于 KG 构建者而言，这意味着“出生日期早于死亡日期”的约束不再是外部检查，而是 Person 类型自身的一个内置属性。

注：OWL是指特定术语或首字母缩略词，可能需要根据上下文添加解释或说明。

Web本体语言（OWL）是一种定义本体的常用标准。在技术上，OWL基于描述逻辑，而描述逻辑本质上是一阶逻辑的一种形式（例如，关于类的推理可以被视为二阶逻辑的一部分）。这种设计在表达力和可判定性之间进行了权衡：OWL推理器可以高效地计算子类关系，检测逻辑矛盾等，但仅适用于保持在一定逻辑限制内的本体。因此，OWL无法涵盖开发者在处理数据时常关心的一些约束条件。

例如，即使在OWL 2规范中，OWL也无法表达同一个实体上的两个数据值之间的约束条件。例如，你可以声明一个人有一个出生日期和一个死亡日期作为日期属性，但你不能在OWL中正式声明出生日期必须早于死亡日期——这样的限制超出了OWL的表达范围。同样地，OWL对于声明全局约束（如“每个人必须恰好有两个父母”或“每个员工的工资必须高于他们的奖金”）的能力也很有限。这些规则要么无法在OWL中表达，要么表达起来非常不自然。通常需要一些变通的方法，例如使用额外的规则或逻辑，或者选择不强制约束并在应用程序代码中进行处理。

这些限制为什么存在？本质上，OWL的描述逻辑框架避免使用复杂的约束，以确保推理在计算上是可行的。它坚持使用某种陈述模板（关于类成员、子类关系、属性域/范围等），并避免使用一阶或二阶逻辑的全部力量。如果我们试图让OWL表达排序日期或数学关系这样的逻辑，我们就会遇到障碍。OWL 2标准增加了一些功能（例如，具备资格的数量限制和属性特性如自反性，这些是早期的OWL版本所没有的功能），但仍然无法表达属性值之间的任意约束。例如，OWL可以声明“自行车至少有2个轮子”或“至多有2个轮子”，但在早期的OWL DL中，无法直接表达“恰好有2个Wheel类型的轮子”，除非进行扩展。而且没有OWL公理可以直接声明一个属性是满射的，也就是说，每个对象都至少与某个主体相关联。这种约束超出了OWL开放世界的单调逻辑范围。

为了填补这些缺口，语义网社区引入了诸如SHACL（形状约束语言）之类的工具。例如，SHACL用于定义RDF数据的形状或结构规则，如“Person节点必须有一个出生日期，如果有死亡日期，则出生日期需早于死亡日期。” SHACL规则通常作为数据图的独立验证步骤来应用。与OWL的开放世界推理不同，后者不假设数据完整，SHACL在封闭世界中进行严格的验证工作。实践中，许多项目使用OWL进行语义建模（如类、子类层次结构和推理），并使用SHACL进行数据完整性检查（如基数、值范围和属性共存）。这种分离使“本体”和“数据验证”分属系统的不同层次。你可以通过OWL获得逻辑一致性检查，但需要运行SHACL引擎（或其他类似工具）来强制执行更多的业务规则。

依赖类型就来了。"DTT" 的意思是“依赖类型理论”，这使得我们有可能将OWL和SHACL分别做的事情统一起来。简单来说，类型系统可以直接表达所有这些约束。不再需要单独的OWL本体和SHACL模式，而是通过依赖类型的知识表示，将本体和完整性约束编码在一起，形成一个整体的框架。

使用依赖类型理论构建知识图谱意味着类型变得“逻辑丰富”：你的实体、关系和约束都存在于同一个形式系统中。实际上，在基于DTT的模型中，一切都是类型或依赖类型，包括我们通常认为的数据。最近的一个例子是TypeDB（以前称为Grakn），它将其模式设计应用了依赖类型原则。正如TypeDB的设计者所描述的那样：实体被视为类型，关系作为依赖类型（引用其他实体），属性作为指向具体值的依赖类型。在这种系统里，像Marriage(Person, Person)这样的关系就是一个依赖类型，它依赖于两个Person类型——实际上将关系视为具有自己约束的一等实体。这比传统的图模型更具表现力，在传统图模型中，边只是没有内部结构的链接。

至关重要的是，由于DTT基于形式逻辑，这些丰富的类型带有必须满足的证明义务或约束。例如，如果你定义了一个Person类型，并且规定出生日期必须早于死亡日期，那么，任何Person类型的实例都需要提供该规则的证明或证据。在实际操作中，这种证据就是对这两个日期的实际比较，类型检查器只会在验证比较有效的情况下接受该实例。这样一来，我们实际上在创建数据的过程中就获得了像SHACL那样的强制性。

让我们来看看几个具体的例子，在这些例子中，DTT比OWL/SHACL更具有表达力或精确度。

• 值依赖的约束（例如出生日期应在死亡日期之前）：如前所述，OWL 本身无法原生在两个日期属性之间执行顺序比较。SHACL 可以实现这个条件，但需要运行一个单独的验证器。在依赖类型理论（DTT）模型中，我们只需将日期顺序作为 Person 类型的属性。例如，在像 Idris/Agda 这样的依赖类型理论语言中，可以定义如下类型：

    定义 Person 为  
    . 构造器 MkPerson  
    . 名字 : String  
    . 出生日期 : Date  
    . 死亡日期 : Optional Date  
    . 验证条件：根据死亡日期情况  
    . 如果死亡日期存在且为 d，则出生日期应在 d 之前  
    . 如果死亡日期不存在，则验证结果为真

在这一类似Idris的伪代码中，证明字段确保当提供死亡日期（Just d）时，出生日期必须早于d。证明会携带这一事实，但如果编译器能够推断出来，可以省略证明。如果有人尝试用早于出生日期的死亡日期构建Person，类型检查器会拒绝这种构建方式，就像编译器遇到错误一样。这意味着数据构建时的一致性得到了保证，而不是在之后才进行检查。这个依赖类型实际上替代了SHACL形状的功能。

• 功能属性和单射/满射映射：在OWL中，你可以声明一个属性为功能型或反功能，这涵盖了简单情况下的唯一性（每个人都最多有一个生日，或每个社会保障号最多对应一个人）。但如何指定一个真正的双射或满射关系呢？例如，在一个大学知识图谱中，我们想说每个学生ID都是唯一的（单射），并且每个学生都有一个学生ID（在一个方向上是单射，在另一个方向上是满射）。OWL无法确保“每个学生有且只有一个ID，每个ID对应唯一一个学生”——你可以断言反功能（唯一ID）和功能型（每个学生最多一个ID），但不能确保每个学生都一定有ID（这是假设所有学生都有一个已知的ID）。利用依赖类型，我们可以将ID分配建模为类型理论中的一个映射，并证明其属性。例如，我们可能有：

    定义 studentID : Student → ID。- 每个学生都有一个 ID  
    公理 id_injective : 对于任意的学生 s1 和 s2，如果 studentID(s1) 等于 studentID(s2)，则 s1 等于 s2

这个 Lean 代码片段将 studentID 声明为一个全函数（意味着每个学生都会产生一个 ID — 你可以通过如何构造或定义学生的方式来确保这一点），并声明了一个公理，即如果两个学生拥有相同的 ID，那么这两个学生必须是同一个学生（一对一）。在依赖类型设置中，这个公理可以被证明为一个定理，从你设置的类型系统来证明。例如，你可以将 ID 设为一个包含学生作为证据的依赖类型，这样通过构造，一个 ID 总是与一个唯一的、特定的学生相关联。关键点在于像一对一或多对一这样的性质可以在类型系统中编码和验证，这超出了 OWL 的原生能力范围。

• 构建时的一致性验证：在当今的知识图谱开发中，一致性检查通常通过运行推理器（检查您的OWL本体加上数据是否有不可满足的类或矛盾）或运行SHACL验证来完成。这些步骤通常在运行时或部署时进行。通过DTT，一致性通常可以在数据被加载之前通过类型检查器来确保。由于任何违反约束的情况都会使一个潜在的实例成为非法类型，因此您根本无法组装一个不一致的知识图谱——类型理论不允许这样做。在使用Coq或Agda等证明助手的背景下，您会构造整个知识图谱作为表示所有本体约束的复杂类型的实例。如果构建成功，您实际上就得到了一个该知识图谱满足所有声明约束的证明。事实上，研究人员已经在Coq的依赖类型系统中构建并查询了一个知识图谱，这意味着知识图谱自带了构建时的一致性机器可验证的证明。

• 类型作为模式（形状和基数）：依赖类型模糊了模式和数据之间的区别。在 DTT 方法中，你的 Person 类型被定义为恰好具有这些属性，而不是通过 SHACL 形状来规定。你需要建模一个“家庭”实体，它恰好拥有两名父母和任意数量的孩子吗？你可以定义一个类型 Family(parent1: Person, parent2: Person, children: List Person)，通过这种定义，家庭现在被定义为恰好只有两名父母。或者，如果学术论文应该至少有一名作者，你可以将其定义为 Paper(authors: NonEmptyList Person, …)，使用一个非空列表类型。这些技巧在使用高级类型系统的编程中很常见，但同样的概念也适用于知识建模。形状约束通过类型构造器来强制执行。不需要单独的验证阶段来检查“有人错误地提供了 0 名父母”这样的情况，因为这种状态在类型上是不可表示的，即这种状态无法用类型来表示。这种方法可以简化技术堆栈：你不再需要维护并行的本体文件和形状文件，这样的规范同时满足了两个方面的需求。

所有这些例子都说明了核心主题：DTT 让数据和逻辑能够无缝地结合。我们不再有需要外部规则来检查的“死数据”；相反，数据通过类型自带规则。一个依赖类型系统可以被视为这种高度表达性的本体语言，在这种语言中，“本体”不再是被动的模式，而是一个积极的部分，能够主动预防错误。

统一框架：实体、关系以及约束条件作为类型的概念

依赖类型方法的一个最强大的特性是它将语义网堆栈中的各个独立层统一起来。在依赖类型理论中，我们不需要区分“本体和数据”或“TBox和ABox”——类型涵盖了这些方面。以婚姻关系为例，如何用依赖类型知识库表示两个人之间的婚姻更合适。在OWL中，你可以定义一个对象属性spouse，并附上一些公理，同时可能使用SWRL或SHACL来确保spouse是互惠的，且每人只有一个配偶等。而在依赖类型理论系统中，你可以定义一个类型（或参数化类型）Marriage(p1: Person, p2: Person)，它直接表示了p1和p2是彼此的配偶这一关系。现在，一个特定的婚姻实例将是一个Marriage(alice, bob)类型的值。只有当alice和bob都是Person，并且所有婚姻约束都得到满足时，这个值才存在。我们因此在一个构造中同时捕获了关系及其约束。

在这种框架下，实体可能表示类型，而关系则可以看作是连接这些实体的依赖类型或函数。属性（即文字值）也可以被看作是依赖类型（例如，“人的年龄”这种类型总是与其出生日期相关联）。知识图的所有部分都遵循相同的类型理论规则。这不仅提供了强大的表达能力，还提供了一种内置的文档：类型签名明确告诉你在图中允许或不允许什么操作。

因为DTT（数据类型图，DTT）也是一种逻辑（具体来说，是一种构造性高阶逻辑），我们甚至可以在这种统一的框架中进行推理。类型本身可以被视为描述数据的逻辑命题。一个良好的类型化的知识库类似于一个证明了“存在一个满足所有这些约束条件的模型”的定理。此外，查询或规则可以用相同的语言来表达。事实上，在TypeDB方法中，查询语言和模式语言紧密相连，查询可以被视为必须满足特定约束的类型。这意味着当你查询数据时，查询可以被检查是否符合模式规则，甚至可以从中推断出来，所有这些都在系统内精确完成。相比之下，传统的技术堆栈：你可能有SPARQL用于查询，与用于本体的OWL分开，与用于验证的SHACL分开——这些工具之间集成有限且往往非正式。DTT承诺一个单一且连贯的框架。

今天，人们如何实践这些想法？目前已经有一些成熟的依赖类型语言和证明工具，可用于知识建模：

• Coq / Agda / Lean（证明助手）：这些是交互式定理证明工具，基于依赖类型理论。它们不是设计成数据库，然而你可以将本体论作为归纳类型和命题的集合来编码。例如，Coq 被用来构建一个原型“依赖类型知识图”，在 Coq 的类型理论中重新创建了 RDF 和 SPARQL 的功能。在 Coq 或 Lean 中，你可以为你的核心实体和关系定义类型，然后声明对应的引理（系统会要求你证明这些引理），这些引理对应于一致性和推理规则。最大的优点是：一旦在 Coq/Lean 中证明了某个命题，就可以得到数学上的确证。缺点是这些工具的学习难度较大，并且“知识库”存在于证明助手内部，而不是存在于传统数据库中。然而，它们非常适合实验，并且可以用绝对严谨的方式建模领域。特别是 Lean，有一个不断壮大的社区和很多教程（Lean 基于依赖类型理论的一种变体，并用于形式化数学，但这些概念也适用于本体论建模）。

• Idris / F / Haskell 带 GADTs（编程语言）：Idris 是一种通用编程语言，具有全依赖类型，这意味着你可以编写直接操作依赖类型数据的程序。例如，你可以在 Idris 中实现一个小型知识库，每个插入操作都是一个函数，该函数仅在插入操作保持一致时返回新的知识状态信息（否则函数无法通过类型检查）。F 是另一种有趣的语言（来自微软研究院），其目标是程序验证，但支持依赖类型；它可能编码复杂的关联性，然后编译为可运行的形式。Haskell 本身不是严格意义上的依赖类型语言，但通过 GADTs 和类型族等扩展，Haskell 可以实现类似依赖类型的一些建模功能。这些编程语言可能为与现有软件系统的集成提供更实际的途径，但与证明助手相比，它们在表达力或方便性上可能会有所欠缺。

• 专门的知识库系统：如前所述，TypeDB 是一个将依赖类型的理念融入其模式中的数据库示例。它提供查询接口并存储数据，因此与知识图谱从业者熟悉的工具更接近，但在底层架构中，它以类型理论的方式处理模式，使其更接近于数据库而非简单的知识图谱工具。开发团队解释说，依赖类型理论为他们提供了“知识表示的数学严谨的基础”，从而能够支持复杂的关系建模，甚至超关系（超图）数据结构。尽管使用时您可能不会直接看到 lambda 表达式或证明，但了解这些原则正在影响新的知识图谱技术是很有启发性的。这表明 DTT 的理念不仅停留在理论层面，而是正在被实际工具所采纳。

为了展示用依赖类型理论建模的样子，这里有一个用Lean 4风格的小示范（Lean 4是Lean的较新版本，感觉更像一种编程语言，同时保留了定理证明的功能）。

    - 定义一个 Person 类型，包含以下字段  
    . name : String.  
    . birthYear : Nat.  
    . deathYear : Option Nat.  
    . - 依赖字段：如果 deathYear 存在，则它应大于 birthYear 的证明  
    . validYears : 根据 deathYear 的值，  
    . | some d => birthYear < d.  
    . | none => True.  
    - 示例用法：构造一个名为 alice 的 Person 实例  
    定义一个 alice 的 Person 实例为  
    . { name := "Alice".  
    . birthYear := 1980.  
    . deathYear := some 2070.  
    . validYears := Nat.lt.base 1980 2070. - 证明 1980 < 2070.  
    . }

在这个代码片段中，如果我们尝试创建一个人，其死亡年份为1970年，而出生年份为1980年，Lean将会拒绝编译，因为它认为我们没有提供有效的 validYears 证明。设计上，我们不能表示具有不现实日期序列的人。类型系统在编译时静态地捕获了这个错误。相比之下，在 RDF/OWL 中，你可以用 RDF 描述 Alice 的出生和死亡年份，但在没有运行自定义规则或查询的情况下，OWL 不会自动标记这种不一致。在 Lean（或其他基于 DTT 的环境中），这种不一致会被视为一个类型错误。

此外，一旦你在Lean/Coq/Agda中有数据，你可以要求系统证明关于这些数据的事情。例如，你可以证明一个命题，即“我们知识库中的所有Person都在出生后死亡”，并且这个证明会自动解决，因为它是由Person本身的类型保证的。这种形式的知识表示开启了机器检查的数据质量和逻辑推导的大门，超越了OWL推理器通常能做的事情（OWL推理器侧重于类的子类关系、实例分类等，但它们不会生成你可以逐步验证的证明——证明助手则可以）。

值得注意的是，依赖类型自然地适应超图，即涉及两个以上实体的关系。基于标准RDF的知识图局限于二元关系（即主体-谓词-客体三元组）。如果你有一个关系涉及到三个或四个事物（例如，一个事件链接了人物、地点、时间和原因），你通常需要将其实体化或分解成更小的部分。在依赖类型框架中，你可以直接将n元关系建模为类型或n元函数/谓词的形式。例如，你可以定义一个类型Event(person: Person, location: Place, time: Time, reason: Reason)作为一个单一的构造。这就像一条超边连接所有相关的节点。TypeDB系统强调了这一点：“不同于简单的图，其中边只连接两个节点，超图允许边同时连接多个节点”，并且通过使用依赖类型，可以对具有复杂多实体依赖关系的关系进行建模。能够原生处理超关系对于表示复杂知识（如生化途径、多方交易等）越来越重要，这一点也越来越突出。每个超关系也可以有自己的约束（例如，一个单一的Event类型可以通过一些调度子逻辑来强制执行，在给定时间人物实际存在于该地点的约束，如果需要的话）。

从范畴理论的角度，依赖类型论的语义与高阶结构（通常在范畴理论中讨论为局部笛卡尔闭范畴）相关联，这意味着它可以自然地描述“由其他事物索引的类型族”——本质上就是超边（由多个节点参数索引的连接集）。对于实践者来说，这意味着：你不必为了适应二元关系而扭曲你的模型；更丰富的类型系统可以直接表达多实体间的关系。

或

依赖类型理论为知识表示带来了新的严谨性和表现力。通过使类型能够表达逻辑，我们获得了一个将本体、数据和约束整合为一体的连贯框架。这形成了一种“实时本体模型”——不仅描述了世界及其规则，还积极地执行这些规则。对于AI和知识图谱开发者而言，这可能意味着更少的无效数据条目、更强的自动化推理能力，以及最终形成更为可靠的知识库。

当然，为知识图谱采用依赖类型理论（DTT）也伴随着挑战。其理论和工具比传统的模式语言系统更复杂。理解证明和依赖类型的理论也存在学习曲线。然而，随着工具的改进并简化了一些复杂性（就像我们看到的新系统如TypeDB，它在更用户友好的界面下嵌入了这些理念），好处变得难以忽视。我们基本上将我们以前在运行时（或作为一个单独的步骤）进行的验证和推理，融入到数据结构的设计过程中。这与软件工程中从无类型脚本到强类型编程的转变类似——许多人最初抵制它，但最终，这些好处赢得了人们的认可，因为它们能够尽早捕捉错误并提供具有自解释性的接口。

在未来几年里，我们可以期待在类型理论和知识图谱的交叉领域有更多的研究和发展。目前已经有人利用证明助手来整理和验证知识，并将依赖类型规格编译成高效的运行时环境。随着知识密集型AI系统（如用于科学研究、法律推理或复杂规划的系统）对一致性和正确性的保证需求越来越高，基于依赖类型理论的方法正变得越来越有吸引力。它提供了一个坚实的基础，在这个基础上，每条数据都被逻辑契约（即其类型）所约束。通过接纳依赖类型，我们或许正见证下一代知识图谱的诞生——这些知识图谱不仅在它们所表示的连接上智慧，而且在维护完整性和推导新知识方面也具备形式上的智慧。

准备好实验了吗？你可以从用像Agda或Lean这样的语言建模一个玩具本体开始，或者研究一下依赖类型知识图谱的相关文献。虽然DTT可能不会马上取代OWL/SHACL，但它可以极大地启发我们对数据模型的新思考。对于AI从业者来说，学习依赖类型可以激发设计时就能保证正确的系统的思路。编程语言理论与知识图谱工程的融合有可能减少我们数据和规则之间的不兼容性，从而打造出既高度表达又稳健可靠的系统。这是一个重新思考语义AI基础的激动人心的时代，依赖类型理论或许是推动下一步飞跃的关键。

在你走之前，提醒一下:

• 记得👏️给作者鼓掌并关注👏️
• 关注我们：X | LinkedIn | YouTube | 通讯简报 | 播客 | Differ | Twitch
• 试试 CoFeed，智能掌握最新科技动态 🧪
• 在 Differ 上创建您自己的免费 AI 博客 🚀
• 加入我们的创作者 Discord 社区 🧑‍💻
• 更多内容，请访问 plainenglish.io 和 stackademic.com