依赖类型理论：知识图谱的下一个里程碑

当今的知识图谱通常依赖本体论（如OWL）来定义类和关系，并利用SHACL等约束语言验证数据结构。这种分层方法虽然有效，但在表达能力和集成方面存在众所周知的局限性。而依赖类型理论（Dependent Type Theory，DTT）则提供了一种替代方案：一个统一的类型系统，其功能强大到足以同时充当本体、数据模式和逻辑。可以把DTT想象成一个功能极度强化的编程语言类型系统——它能将复杂的规则（例如“出生日期必须早于死亡日期”）直接编码到数据类型中。对于AI和知识图谱从业者而言，这意味着数据不一致性可在“编译时”（即数据录入阶段）被及时发现并纠正，而无需依赖单独的验证步骤。本文将以通俗易懂的方式介绍DTT，并探讨它如何增强甚至取代传统的OWL本体论和SHACL验证机制。

什么是依赖类型理论（DTT）？

依赖类型理论的核心是一种类型系统，其中类型可以依赖于值。换言之，程序的类型定义可以包含实际数据或条件。这在Coq、Agda、Idris或Lean等证明助手语言中是常见的。例如，在支持依赖类型的语言中，你可能会有一个Vector(n)类型，它表示“一个长度为n的数组”。这里的数字n是一个存在于类型内部的值——因此Vector(3)和Vector(4)是不同的类型。这使得类型系统能够自动强制执行数组长度一致性等属性。

对于知识表示，我们可以这样类比：将知识图谱中的实体和关系视为编程语言中的“值”，同时其类型系统能够确保本体论规则的有效性。依赖类型具有极高的表达能力——它们可以将子集约束、关系条件以及其他复杂规则纳入类型定义中。在实践中，依赖类型可以被视为一种内含逻辑的类或模式。

为了具体说明，我们来看一个包含DTT特性的伪代码简化示例：

// Pseudocode for a Person type with a dependent constraint
type Person(name: String, birthDate: Date, deathDate: Date?)
// If deathDate is provided, enforce birthDate < deathDate
requires (deathDate == null) or (birthDate < deathDate)

在这个例子中，Person是一个类型，包含name、birthDate和可选的deathDate字段。有趣的部分是requires子句：它是一个逻辑条件，它成为了类型定义的一部分。任何被声明为Person类型的数据都必须满足“出生日期早于死亡日期”的规则（如果存在死亡日期）。在DTT中，这类条件在类型检查阶段由编译器或解释器进行验证——就像程序中违反类型会引发编译错误一样。对于知识图谱开发者而言，这意味着“出生日期早于死亡日期”这一约束不再是外部验证的内容，而是Person类型的内置属性。

OWL的逻辑基础与局限性

网络本体语言（OWL）是定义本体论的常用标准。其底层基于描述逻辑（Description Logics），而描述逻辑本身是谓词逻辑（first-order logic）的片段（OWL的某些方面，如关于类的推理，可以被视为二阶逻辑）。这种设计以牺牲表达能力来换取可判定性：OWL推理机可以高效地计算子类关系、检测逻辑不一致性等，但仅限于在特定逻辑范围内定义的本体。因此，OWL无法捕捉到开发者在数据中经常关注的某些类型的约束。

例如，OWL（即使是OWL 2版本）也无法表达对同一实体中两个数据值进行比较的约束。你可以声明一个Person具有出生日期和死亡日期作为日期属性，但你无法在OWL中正式声明“出生日期早于死亡日期”——这种限制超出了OWL的表达范围。类似地，OWL在声明全局约束方面的能力也有限，例如“每个人必须恰好有两个父母”或“每个员工的工资必须高于其奖金”。这些规则在OWL中要么无法表达，要么实现起来十分复杂且不直观。它们通常需要变通方案（例如使用额外的规则，或将约束不强制执行，并在应用程序代码中处理）。

为什么存在这些局限性？本质上，OWL的描述逻辑框架避免了复杂的约束，以确保推理计算上的可行性。它坚持特定的语句模板（关于类成员资格、子类关系、属性域/值域等），并避免使用谓词逻辑或二阶逻辑的全部能力。如果尝试强制OWL表达日期排序或数学关系等内容，则会面临限制。OWL 2标准增加了一些特性（例如限定基数约束和像自反性这样的属性特征，这些是旧版OWL所缺乏的），但仍然无法表示属性值之间的任意约束。例如，OWL可以声明“一辆自行车至少有2个轮子”或“至多2个轮子”，但在早期的OWL DL中，不通过扩展是无法表示“恰好2个类型为Wheel的轮子”的。而且，没有OWL公理可以声明一个属性是满射的（即该属性值域中的每个对象都与某个主体相关联）——这类约束超出了OWL的开放世界、单调逻辑的范畴。

为了弥补这些不足，语义网社区引入了SHACL（Shapes Constraint Language）等工具。例如，SHACL可以定义RDF数据的形状或结构规则，如“一个Person节点必须有一个出生日期，如果它有一个死亡日期，那么出生日期必须早于死亡日期。” SHACL规则通常作为单独的验证步骤应用于数据图谱。与OWL的推理（开放世界，不假设数据是完整的）不同，SHACL在封闭世界、严格验证模式下运行。在实践中，许多项目使用OWL进行语义建模，如定义类、构建子类层次结构以及执行推理；同时使用SHACL进行数据完整性检查，例如验证基数、值范围以及属性的共现关系。这种分离意味着“本体论”和“数据验证”存在于系统的不同层面——你可以从OWL获得逻辑一致性检查，但需要运行SHACL引擎（或类似工具）来强制执行更具程序性的业务规则。

依赖类型理论提供了一种解决方案。通过DTT，我们可以将OWL和SHACL的功能整合到一个统一的框架中。其理念是类型系统可以直接表达所有这些约束。依赖类型知识表示不再需要一个OWL本体加上一个单独的SHACL模式，而是将本体和完整性约束编码在一个连贯的框架中。

DTT如何增强知识建模

将依赖类型理论用于知识图谱意味着类型变得“富有逻辑”：你的实体、关系和约束都整合于一个单一的正式系统中。事实上，在基于DTT的模型中，一切都是类型或依赖结构，包括我们通常认为是数据实例的。TypeDB（前身为Grakn）是这种方法的一个典型示例，它将依赖类型原理应用于其模式设计。正如TypeDB的设计者所描述的：实体可被视为类型，关系则为依赖类型（引用其他实体的类型），而属性则可视为指向字面值的依赖类型。在这样的系统中，像Marriage(Person, Person)这样的关系可以是一个依赖类型，它本身依赖于两个Person类型——有效地将关系视为具有自身约束的一等公民。这比传统的图建模更具表达性，在传统图建模中，边只是一个没有内部结构的链接。

至关重要的是，由于DTT植根于形式逻辑，这些“富类型”内含必须满足的证明义务或约束。如果你定义了一个Person类型，并规定出生日期必须早于死亡日期，那么任何Person实例都需要证明或证据来满足该规则。在实践中，这个证据可能就是两个日期的实际比较——类型检查器仅在验证比较成立后才会接受该实例。我们实际上获得了SHACL所提供的强制性校验功能，但它被“烘焙”进了数据创建的动作本身。

我们来探讨几个DTT比OWL/SHACL提供更多表达能力或精确度的具体场景：

• • 值依赖约束（例如出生日期早于死亡日期）： 如前所述，OWL无法原生强制执行两个日期属性之间的顺序比较。SHACL可以强制执行，但只能通过运行单独的验证器。在基于DTT的模型中，我们只需将日期顺序作为Person类型的一部分。例如，在像Idris/Agda这样的依赖类型语言中，可以编写如下类型：

  record Person where
  constructor MkPerson
  name : String
  birthDate : Date
  deathDate : Optional Date
  proof : case deathDate of
  Just d => birthDate < d
  Nothing => True

  在这个类似Idris的伪代码中，proof字段确保如果提供了deathDate（Just d），则birthDate < d必须成立（proof值概念上会携带该事实的证明，但如果编译器能够推断出来，则可以省略）。如果有人试图创建一个死亡日期早于出生日期的人，类型检查器就会拒绝——这类似于编译错误。这意味着一致性在数据构建时就得到了保证，而不是事后才检查。依赖类型有效地取代了SHACL的形状定义。
• • 函数属性和单射/满射映射： 在OWL中，你可以声明一个属性是函数式（Functional）或逆函数式（InverseFunctional），这涵盖了简单的唯一性情况（每个人最多有一个出生日期，或每个社会安全号最多标识一个人）。但如何指定一个真正的双射（bijective）或满射（surjective）关系呢？例如，假设在大学知识图谱中，我们想说每个学生ID对于一个学生是唯一的（单射），并且每个学生都有一个学生ID（一个方向是函数式，另一个方向是全函数）。OWL无法完全强制执行“每个学生恰好有一个ID，并且每个ID恰好指代一个学生”——它可以断言逆函数式（ID唯一）和函数式（每个学生至多一个ID），但它不能强制要求每个学生都必须有一个ID（这是一种封闭世界假设）。通过依赖类型，我们可以在类型理论中将ID分配建模为一个函数，并证明其属性。例如，我们可能有：

  constant studentID : Student → ID. // 每个学生都有一个ID（全函数）
  axiom id_injective : ∀ s1 s2, studentID s1 = studentID s2 → s1 = s2

  这个Lean代码片段声明studentID是一个全函数（这意味着每个Student都会产生一个ID——你可以通过构建或定义学生的方式来确保这一点），以及一个公理，声明如果两个学生共享相同的ID，他们必须是同一个学生（单射性）。在依赖类型环境中，这个公理可以是你根据类型设置方式证明的一个定理。例如，你可以将ID设为包含学生作为证据的依赖类型，这样通过构造方式，一个ID总是绑定到一个唯一的学生。关键点是，单射性或满射性等属性可以在类型系统内部编码和验证，这远超OWL的原生能力范围。
• • 构建时的一致性证明： 在当今的知识图谱开发中，一致性检查通常通过运行推理机（查看OWL本体和数据是否存在不可满足的类或矛盾）或运行SHACL验证来完成。这些是运行时或部署时的步骤。通过DTT，一致性通常可以在数据被“加载”之前由类型检查器确保。由于任何约束违反都会导致潜在的实例类型错误，你根本无法构建一个不一致的知识图谱——类型理论不允许它。在Coq或Agda等证明助手的上下文中，需要将整个知识图谱作为一个复杂类型的项（term）来构建一个“证明实例”（witness），该类型代表了所有的本体约束。如果构建成功，你实质上就拥有了一个证明，证明该知识图谱满足所有声明的约束。事实上，研究人员已经演示了在Coq的依赖类型系统内构建和查询知识图谱，这意味着该知识图谱通过构造方式获得了机器可检查的一致性证明。
• • 类型即模式（形状和基数）： 依赖类型模糊了模式和数据之间的界限。在DTT方法中，你不会编写一个SHACL形状来声明“Person必须具有属性X、Y、Z”；相反，你的Person类型被定义为恰好具有这些属性。OWL或SHACL会表达的基数（例如某个属性的1个或2个值）就变成了字段的数量或你类型的结构。需要建模一个具有恰好两个父母和任意数量孩子的“家庭”实体？你可以定义一个类型Family(parent1: Person, parent2: Person, children: List Person)——现在，根据定义，一个Family就只有两个父母。或者，如果一篇学术论文应该至少有一个作者，你可能会将其定义为Paper(authors: NonEmptyList Person, ...)，使用一个非空列表类型。这些技巧在高级类型系统编程中很常见，但同样的思想也适用于知识建模：形状约束由类型构造器强制执行。不需要单独的验证阶段来检查“是否有人不小心提供了0个父母？”，因为这样的状态在类型中是字面上无法表示的。这种方法可以简化技术栈：你不再需要维护并行的本体文件和形状文件，而只有一个依赖类型的规范，同时服务于这两种目的。

所有这些例子都说明了核心主题：DTT让我们能够无缝地混合数据和逻辑。你不再需要对外部规则进行单独检查的“静态数据”；相反，数据本身通过类型系统携带规则。依赖类型系统可以被视为一种表达力极强的本体语言，其中“本体”不仅仅是一个被动模式，而是数据模型中主动防止错误的一部分。

统一框架：实体、关系和约束作为类型

依赖类型方法最强大的方面之一是它统一了语义网栈中原本分离的层级。在DTT中，我们不必将“本体与数据”或“TBox（术语盒）与ABox（断言盒）”分开——类型涵盖了两者。举例来说，考虑一个依赖类型知识库如何表示两个人之间的婚姻关系。在OWL中，你可能有一个对象属性spouse和一些公理，并且你可能使用SWRL或SHACL来强制spouse是互惠的且每人一个等等。在DTT系统中，你可以引入一个类型（或参数化类型）Marriage(p1: Person, p2: Person)，它直接编码了p1和p2互为配偶（可能还有一个证明p1 ≠ p2以禁止自婚等）。现在，一个特定的婚姻实例将是Marriage(alice, bob)类型的值。该值只有在alice和bob都是Person且所有婚姻约束都满足的情况下才能存在。这样，我们就将关系及其约束捕获在一个构造中。

在这样的框架中，实体可能对应于类型，而关系则对应于链接这些实体的依赖类型或函数。属性（字面值）也可以被视为依赖类型（例如，一个始终与Person的出生日期保持一致的“Person年龄”类型）。知识图谱的所有部分都受相同的类型理论规则约束。这不仅提供了表达能力，还提供了一种内置的文档功能：类型签名能精确地告知你在图谱中允许或不允许哪些内容。

因为DTT也是一种逻辑（具体来说，是构造性（constructive）、高阶逻辑的一种形式），我们甚至可以在这个统一框架中进行推理。类型本身可以被视为关于它们所描述数据的逻辑命题。一个类型正确的知识库，就好比一个已被证明的定理，它声明“存在一个满足所有这些约束的模型”。此外，查询或规则也可以用相同的语言进行表述。事实上，在TypeDB方法中，查询语言和模式语言紧密相连，以至于查询本身可以被视为必须满足特定约束的类型。这意味着当你查询数据时，查询可以以一种非常精确的方式根据模式规则进行检查（甚至从模式规则中推断出来），所有这些都在一个系统内完成。这与传统的技术栈形成对比：你可能用SPARQL进行查询，它独立于用OWL定义的本体，又独立于用SHACL进行的验证——这些层之间的集成是有限且通常是非正式的。DTT承诺提供一个单一的、连贯的框架。

使用证明助手和依赖类型语言

从业者今天如何实践这些思想呢？现在已经有几种成熟的依赖类型语言和证明助手可以用于知识建模：

• • Coq / Agda / Lean (证明助手)： 这些是基于依赖类型理论的交互式定理证明环境。它们并非为数据库而设计，但可以将本体论编码为归纳类型和命题的集合。例如，Coq曾被用于构建一个原型“依赖类型知识图谱”，它在Coq的类型理论中重现了RDF和SPARQL的功能。在Coq或Lean中，你可以为核心实体和关系定义类型，然后声明引理（系统会要求你证明它们），这些引理对应于一致性或推理规则。优点是坚如磐石的保证——如果在Coq/Lean中被证明，那它在数学上是确定的。缺点是这些工具的学习曲线陡峭，并且“知识库”存在于证明助手内部，而非典型的数据库。然而，它们非常适合进行实验以及以绝对严谨的方式建模领域。特别是Lean，其社区日益壮大，并拥有大量教程（Lean基于一种DTT变体，用于形式化数学，但这些概念也适用于本体建模）。
• • Idris / F* / 带有GADTs的Haskell (编程语言)： Idris是一种通用编程语言，拥有完整的依赖类型，这意味着你可以编写直接操作依赖类型数据的程序。例如，你可以在Idris中实现一个小型知识库，每次插入都是一个函数，只有当插入保持一致性时，该函数才会返回一个新的知识状态（否则函数将无法通过类型检查）。F*是另一个有趣的语言（来自微软研究院），旨在进行程序验证，但也支持依赖类型；它有可能编码复杂的关系，然后编译成可运行的形式。Haskell在严格意义上并非依赖类型语言，但通过GADTs和类型家族等扩展，Haskell可以实现一些类似依赖类型的建模。这些编程语言可能为与现有软件系统集成提供更实用的途径，但代价是与证明助手相比，表达能力或便利性有所牺牲。
• • 专用知识库系统： 如前所述，TypeDB是一个将依赖类型思想融入其模式设计的数据库示例。它提供了一个查询接口和数据存储，因此更接近知识图谱从业者习惯的工具，但其底层以类型理论的方式处理模式。创建者解释说，依赖类型理论为他们提供了“知识表示的数学上健全的基础”，从而实现了复杂关系建模乃至超关系（hyper-relational，即超图）数据结构。虽然在使用这类系统时，你可能不会直接与lambda项或证明进行交互，但了解这些原理正在影响新的知识图谱技术是有启发性的。这意味着DTT的思想不仅仅是学术层面的；它们正在进入实际工具。

为了说明使用依赖类型理论进行建模是什么样子，这里有一个Lean 4风格的微型示例（Lean 4是Lean的更新版本，它在保留定理证明能力的同时，感觉更像一种编程语言）：

// 定义一个基本的Person类型，其中包含一个基于年龄的依赖约束
structure Person where
name : String
birthYear : Nat
deathYear : Option Nat
// 依赖字段：如果deathYear存在，则证明其大于birthYear
validYears : match deathYear with
| some d => birthYear < d
| none => True
// 示例用法：构建一个Person实例
def alice : Person :=
{ name := "Alice"
birthYear := 1980
deathYear := some 2070
validYears := Nat.lt.base 1980 2070 // 证明1980 < 2070（微不足道）
}

在这个片段中，如果我们试图创建一个死亡年份为1970年而出生年份为1980年的人，Lean会拒绝编译，并提示我们未能提供validYears的有效证明。根据设计，我们无法表示具有不可能日期序列的Person。类型系统在编译阶段就捕获了错误。与RDF/OWL相比：你可以在RDF中描述Alice的出生和死亡年份，但OWL中没有什么能自动标记出不一致性，除非你运行自定义规则或查询。在Lean（或其他基于DTT的环境）中，不一致性就是类型错误。

此外，一旦你在Lean/Coq/Agda中有了数据，你就可以要求系统证明关于它的事物。例如，你可以证明一个引理，即“我们知识库中的所有人都是在出生后才去世的”，这个证明会自动解决，因为它已经由Person类型本身保证了。这种形式化的知识表示方式为数据质量和逻辑蕴涵的机器可检查证明打开了大门，超越了OWL推理机通常所做的工作（OWL推理机侧重于类包含、实例分类等，但它们不生成可以逐步检查的证明——而证明助手可以做到）。

超图与高阶关系

值得注意的是，依赖类型天然地支持超图，即涉及两个以上实体的关系。标准基于RDF的知识图谱仅限于二元关系（主语-谓语-宾语三元组）。如果你有三或四项之间的关系（例如一个事件连接着一个人、一个地点、一个时间和原因），你通常需要进行实体化（reify）处理，或将其拆分为更小的部分。在依赖类型框架中，你可以直接将一个n元关系建模为一个类型或一个n元函数/谓词。例如，你可以将Event(person: Person, location: Place, time: Time, reason: Reason)定义为一个单一的构造。这就像有一个连接所有相关节点的超边。TypeDB系统强调了这一能力：“与边仅连接两个节点的简单图不同，超图允许边同时连接多个节点”，通过使用依赖类型，可以建模与多个实体有复杂依赖关系的关系。原生处理超关系的能力对于表示复杂知识（如生化通路、多方交易等）越来越重要，而DTT提供了一种清晰的方式来实现这一点。每个超关系也可以携带自己的约束（例如，一个单一的Event类型可以强制要求参与者通过某种调度子逻辑，确实在给定时间出现在给定地点，如果需要达到那种程度的严谨性）。

在范畴论术语中，依赖类型理论的语义与高阶结构相关联（在范畴论中常被称为局部笛卡尔闭范畴（locally cartesian closed categories）），这意味着它能够很好地处理“由其他事物索引的事物族”——这本质上就是超边的概念（一个由多个节点参数索引的连接族）。对于从业者来说，这意味着：你不必扭曲你的模型以适应二元关系；更丰富的类型系统可以直接表达多实体关系。

结论

依赖类型理论为知识表示带来了新的严谨性和表达能力水平。通过使类型能够表达逻辑，我们获得了一个统一的系统，其中本体论、数据和约束都编码在一个连贯的框架中。这带来了一种“活的本体论”——它不仅描述了世界，还主动强制执行了这种描述的规则。对于AI和知识图谱开发者而言，这可能意味着更少的无效数据录入、更强大的自动化推理，并最终带来更值得信赖的知识库。

当然，将DTT应用于知识图谱也伴随着挑战。其理论和工具比传统的模式语言更为复杂，理解证明和依赖类型需要一定的学习曲线。然而，随着工具的不断改进，并逐渐隐藏这些复杂性（正如TypeDB等新系统所展示的，它们将DTT思想融入了更友好的用户界面），DTT的优势将变得难以忽视。我们本质上是将过去在运行时（或作为单独步骤）进行的验证和推理，转移到数据结构本身的设计中。这类似于软件工程中从无类型脚本语言向强类型编程的转变——许多人最初抵制，但最终，提前捕获错误和拥有自文档化接口的优势胜出。

在未来几年，我们可以期待类型理论与知识图谱交叉领域出现更多的研究和发展。已经有关于使用证明助手来管理知识以及将依赖类型规范编译成高效运行时系统的工作。随着知识密集型AI系统（如用于科学研究、法律推理或复杂规划的系统）对一致性和正确性提出更高的保证要求，基于DTT的方法显得越来越有吸引力。它提供了一个坚实的基础，其中每条数据都受其类型所代表的逻辑契约约束。通过拥抱依赖类型，我们很可能正在见证下一代知识图谱的出现——它们不仅在所表示的连接中表现出智能，而且在维护完整性和推断新知识方面也具有形式上的智能。

如果您有兴趣尝试，可以从在Agda或Lean等语言中建模一个简单的本体开始，或者查阅有关依赖类型知识图谱的相关文献。即使DTT不能在一夜之间取代OWL/SHACL，它也能极大地启发我们思考数据模型的新方式。对于AI从业者来说，了解依赖类型可以激发设计“通过构建实现正确性”的系统的想法。编程语言理论与知识图谱工程的融合有可能减少数据与规则之间的“阻抗不匹配”，从而产生既高度表达又稳健可靠的系统。这是一个重新构想语义AI基础的激动人心时刻，而依赖类型理论可能正是实现下一个飞跃的关键。