“静态”（static）指不运行程序就能知道的东西，“动态”（dynamic）指运行时才能看到的东西。按类型检查发生在什么时候，程序语言大致分成两类：

• 静态类型语言（statically typed）：在运行之前检查类型，通常在编译阶段完成；不通过检查的程序被拒绝。Rust、Haskell、OCaml、Java、C 都属于这一类。 [定义] 类型与类型判断 的类型系统也是：$𝑡:𝑇$ 只看项的形状，不执行 [定义] 一步归约 的 $⟶$ 归约。
• 动态类型语言（dynamically typed）：程序先运行，每次真正做运算时再检查参与运算的值是不是合适的种类，不合适就抛出错误。Python、JavaScript、Ruby 属于这一类。

用 [定义] 项的集合 的布尔值／自然数语言作类比，一种动态检查的设计是不预先构造 $𝑡:𝑇$ 的推导，而是在 $⟶$ 里给不合适的运行时操作补上报错规则（ [附注] 显式错误规则与 Kotlin 的底类型 ），把受阻换成可预期的异常。另一种操作可以采用转换规则（ [例] JavaScript 隐式转换与相等三角图 ）。真实语言往往同时有这两类处理；JavaScript 的条件还会采用真假值转换，不要求参数字面上就是布尔值。

对这门小语言的运算，类型规则、 [引理] 典范形式（canonical forms） 与 [定理] 保型 合起来保证：参数若被要求为 $\text{Nat}$，求值为值时就一定是数值，所以不必再检查它是否为布尔值。这不等于真实静态类型语言可以省掉所有运行时检查；例如 Kotlin 仍会抛出数组越界异常，Rust 的数组索引也可能需要边界检查。两者的取舍是：静态检查更早排除它所覆盖的错误，但会拒绝一些实际运行不会出错的程序（ [附注] 类型系统是保守的 ）；动态检查更灵活，但错误通常要等到运行到那一行才暴露。

另外，“静态 / 动态”和“强 / 弱”是两个不同的维度。C 是静态类型，但允许随意强制转换指针，类型系统不可靠；Python 是动态类型，但不会把字符串当整数用。 [推论] 类型安全 证明的“类型安全”，指的是这套静态类型系统对受阻错误的可靠性，不是由“强／弱”这一称呼作出的保证。

对这个话题感兴趣的可以看看帝球的类型 vs. 类型检查