本文整理自 Luca Cardelli, Type Systems 的第四章内容。欢迎 star 和 follow。

命令式语言中的一阶类型系统 (First-order Type Systems for Imperative Languages)

命令式语言在类型系统方面和函数式语言略有区别，主要是因为它们明确区分了命令（不返回值）和表达式（返回值）。通过给命令赋予类型，可以将命令简化为表达式，但我们在这里更倾向于保留两者的区别。

作为命令式语言类型系统的示例，我们在表20 中总结了无类型命令式语言的语法。这种语言让我们有了学习声明(declarations)的类型规则的机会，这是我们尚未讨论过的。在这种语言中，过程和数据类型的处理非常基础，可以轻松地根据第3章中所描述的规则进行调整。

表20. 命令式语言的语法

我们将命令式语言的断言列在表21中。断言和对应于 F1 的同一个断言，因为我们现在区分了命令和表达式。断言将签名(signature) 分配给声明(declaration) ；签名本质上是声明的类型。在这种简单的语言中，签名仅有一个组成部分。例如，相应的声明可以是。通常情况下，一组签名将由类似于此的组件的列表组成，从表面看起来和环境非常相似。