静态类型和动态类型

静态类型在程序运行前检查类型，而动态类型在执行期间检查类型；渐进式类型旨在将两者结合在一种语言中。

Definition

静态类型在编译时验证类型约束，以便在执行前接受类型正确的程序；动态类型将类型检查推迟到运行时，当操作应用于不适当类型的值时会引发错误。

Scope

本主题涵盖了类型检查发生的时间和方式：在编译时拒绝类型不正确程序的静态检查，在运行时检测类型错误的动态检查，以及允许两者共存的渐进式或可选类型。它探讨了每种方法的保证、灵活性和性能影响，以及类型检查规范的健全性。

Core questions

• 静态检查可以防止哪些动态检查无法提前防止的错误类别？
• 动态类型提供了哪些灵活性，代价是什么？
• 渐进式类型如何能健全地混合类型化和非类型化代码？
• 如何确立静态类型规范的健全性？

Key theories

渐进式类型

Siek和Taha定义了一种类型系统，允许程序的一部分是静态类型，另一部分是动态类型，并通过一致性关系来管理边界处的安全交互。

静态类型健全性

Wright和Felleisen的进展与保持方法表明，健全的静态类型系统保证类型正确的程序永远不会达到停滞状态，从而形式化了静态检查的安全性。

Clinical relevance

静态与动态的选择决定了开发人员的工作流程、工具和可靠性。渐进式和可选类型系统，例如那些叠加在动态语言之上的系统，允许团队逐步向大型现有代码库添加静态保证。

History

早期语言分为静态类型（Algol、Pascal、ML）和动态类型（Lisp、Smalltalk）两大类。随着动态语言因其生产力而日益普及，研究人员试图调和这两种方法；Siek和Taha在2006年提出的渐进式类型以及同期关于可选类型的工作，促成了基于动态语言构建的广泛使用的渐进式类型系统。

Debates

渐进式类型的成本和健全性

研究人员争论健全的渐进式类型是否能避免在类型化/非类型化边界处产生过高的运行时检查成本，以及不健全的“可选”类型是否是更好的实际权衡。

Key figures

• Benjamin Pierce
• Jeremy Siek
• Walid Taha
• Matthias Felleisen

Seminal works

• pierce2002
• siek2006
• wright1994

Frequently asked questions

静态类型总是优于动态类型吗？

两者并非普遍优劣；静态类型能更早地捕获更多错误并有助于工具开发，而动态类型则提供灵活性和更快的原型开发，因此正确的选择取决于项目的可靠性和敏捷性需求。

什么是渐进式类型？

渐进式类型允许单个程序混合静态和动态类型部分，在边界处插入运行时检查，从而使类型化代码保持其保证，同时非类型化代码保持灵活性。