5.2.2 依赖类型基础

文档摘要

5.2.2 依赖类型基础在类型系统的演进长河中，依赖类型（Dependent Types）不是一次温和的改良，而是一场静默却彻底的范式地震。它撕开了“类型”与“值”之间那道被默认为不可逾越的帷幕——从此，一个类型的定义，可以合法地、精确地、可计算地依赖于某个具体运行时值；一个函数的返回类型，不再由输入参数的种类决定，而是由输入参数的具体内容决定；一段程序的正确性，不再靠测试用例去碰运气，而是被编译器在类型检查阶段就强制验证为逻辑必然。这不是语法糖，不是元编程的花招，更不是类型推导的延伸；这是将证明论（Proof Theory）的骨架，直接嵌入到程序语言的语法与语义之中。