渐进类型（Gradual Typing）

定义

渐进类型（gradual typing）是一种让静态类型检查与动态类型代码在同一语言中共存的类型系统设计，由 Jeremy Siek 与 Walid Taha 于 2006 年系统提出。核心是引入特殊的动态类型（常记作 ? 或 any/dynamic），带标注的部分接受静态检查，未标注部分保持动态语义。

设计要点

理论上，渐进类型系统应满足「渐进保证」：给正确程序增删类型标注不应改变其行为。静态与动态代码的边界可插入运行时契约检查，以便在类型被违反时准确归责（blame）。

工业实践

TypeScript（JavaScript）、mypy 与 Python 的类型注解体系、Sorbet（Ruby）、Hack（PHP）、C# 的 dynamic 都是渐进类型思想的大规模应用，使巨型动态语言代码库得以逐文件迁移到静态检查。

意义

渐进类型是过去二十年动态语言生态最重要的演进方向之一。