类型系统

类型系统是形式化规程，通过对程序表达式所计算的值的种类进行分类，在程序运行前排除大量错误。

Definition

类型系统是一种易于处理的句法方法，通过根据表达式所计算的值的种类对其进行分类，来证明某些程序行为不存在。

Scope

该领域涵盖类型系统的理论与设计：静态与动态类型、参数化和特定多态性、子类型、类型推断以及依赖类型和子结构类型等高级系统。它探讨类型健全性、通过Curry-Howard对应关系连接类型与逻辑，以及类型规程如何在表达能力、保证和可判定性之间进行权衡。

Sub-topics

• dependent and substructural types
• polymorphism and generics
• static and dynamic typing
• type inference

Core questions

• 类型系统提供哪些保证？类型健全性是什么？
• 多态性和子类型如何在不牺牲安全性的情况下增加表达能力？
• 类型能否自动推断？推断何时是可判定的？
• 类型能在多大程度上编码丰富的程序属性，直至完整的规范？

Key theories

通过进展和保持实现类型健全性

Wright和Felleisen的句法方法通过确立类型良好的程序不会陷入停滞来证明类型系统是健全的：类型在求值过程中得以保持，并且类型良好的项总是能取得进展。

多态性和抽象的类型学

Cardelli和Wegner在一个统一的框架内组织了类型概念空间，区分了参数化和特定多态性、包含（子类型）和数据抽象。

作为编程语言基础的类型理论

Harper开发了一种统一的静态和动态方法论，其中语言特性通过类型和求值规则定义，将类型理论视为语言设计的组织基础。

Clinical relevance

类型系统是应用最广泛的形式化方法之一：它们在编译时捕获错误、文档化接口、实现安全重构并驱动编辑器工具。泛型、渐进式类型和所有权类型等进展已直接进入主流工业语言。

History

类型化语言随着Algol和简单类型lambda演算等早期系统而出现。Milner的多态类型推断（1978）奠定了ML的基础；Girard和Reynolds独立设计了用于参数多态性的System F。Cardelli和Wegner于1985年发表的综述使该领域系统化，而进展与保持方法（1994）成为标准的健全性技术，后来由Pierce和Harper在教科书中确立。

Debates

静态与动态类型

一场长期争论权衡了静态类型的早期错误检测和文档化与动态类型的灵活性和快速迭代，渐进式类型被视为一种和解方案。

Key figures

• Benjamin Pierce
• Robert Harper
• Luca Cardelli
• Robin Milner
• Matthias Felleisen

Seminal works

• pierce2002
• harper2016
• cardelli1985
• wright1994

Frequently asked questions

类型系统健全意味着什么？

健全性意味着类型良好的程序不会出现类型系统旨在预防的错误，通常通过证明类型在求值过程中得以保持且类型良好的程序永远不会陷入停滞来证明。

动态类型语言有类型系统吗？

它们有类型并执行运行时类型检查，但它们缺乏在执行前拒绝错误类型程序的静态类型系统；类型错误反而表现为运行时故障。