Extending the Theory and Practice of Gradual Typing

编程语言通常分为静态类型和动态类型。Java等静态类型语言使用类型来确保程序在运行之前满足基本的行为保证。类型检查捕获编程错误，并支持优化，使程序运行更快，使用更少的内存。但是，程序员必须添加额外的类型注释，并且类型检查通常会拒绝本来可以正常运行的程序。动态类型语言（如Javascript和PHP）使用运行时检查来捕获错误，因此它们支持灵活且快节奏的编程，这些编程被大量用于开发网站和移动应用程序。但在交易中，它们往往运行得更慢，占用更多内存和电力，这对移动应用来说尤其糟糕，而且已部署的程序往往存在代价高昂的错误，而这些错误本可以被类型检查器立即发现。

Programming languages are typically categorized as either statically or dynamically typed. Statically typed languages such as Java use types to ensure that a program satisfies basic behavioural guarantees before running it. Type checking catches programming errors and supports optimizations that make programs run faster and use less memory. However, programmers must add extra type annotations, and type checking often rejects programs that would otherwise run correctly. Dynamically typed languages such as Javascript and PHP use runtime checks to catch errors, so they enable flexible and fast-paced programming that is heavily used to develop web sites and mobile applications. But in trade they tend to run slower and use more memory and power, which is particularly bad for mobile apps, and deployed programs often harbour costly bugs that could have been detected right away by a type checker.