Dependent Type

释义 Definition

依赖类型：一种类型系统中的类型，其定义可以依赖于某个值（term）。也就是说，类型不仅取决于其他类型，还能取决于具体数据，从而更精确地表达程序性质与约束（常用于定理证明与形式化验证）。（在不同语境下也可能指“依赖于……的类型/从属类型”，但在编程语言与类型论里通常指上述含义。）

发音 Pronunciation

/dɪˈpɛndənt taɪp/

例句 Examples

A dependent type can encode the length of a list in its type.
依赖类型可以把列表的长度编码到它的类型里。

In a proof assistant, dependent types let you express specifications and programs in one language, so a function’s type can state and enforce a theorem about its behavior.
在证明助手中，依赖类型让你用同一种语言表达“规格说明”和“程序”，因此函数的类型可以陈述并约束一个关于其行为的定理。

词源 Etymology

dependent 来自 depend（依赖）+ 形容词后缀 -ent（表示“处于某种状态/具有某种性质”）；type 源自希腊语 typos（印记、模型、范式）。合起来表示“会随某些值而变化（依赖）的类型”。

相关词 Related Words

• Dependent
• Type
• Type System
• Dependent Typing
• Polymorphism
• Generics
• Proof Assistant
• Curry–Howard Correspondence

文学与著作 Notable Works

• Homotopy Type Theory: Univalent Foundations of Mathematics（HoTT Book）：在现代类型论语境下大量讨论依赖类型及其数学化表达。
• Types and Programming Languages（Benjamin C. Pierce）：在类型系统框架中涉及相关思想，并为理解依赖类型打基础。
• Practical Foundations for Programming Languages（Robert Harper）：从语言理论角度讲解类型系统，包含与依赖类型紧密相关的核心概念。
• Type Theory and Formal Proof（Rob Nederpelt & Herman Geuvers）：以形式化证明为主线介绍类型论，依赖类型是关键主题之一。
• Software Foundations（Pierce 等）：在 Coq 语境下频繁出现与依赖类型直接相关的概念与用法。