Skip to content

Chapter 1-2: Introduction

什么是类型系统

A type system is a tractable syntactic method for proving the absence of certain (bad) program behaviors by classifying phrases according to the kinds of values they compute.

What are type systems good for?

  • Detecting Errors
  • Many programming errors can be detected early, fixed intermediately and easily.
    • i.e. all possible errors would better be compile-time errors
  • Abstraction
  • type systems form the backbone of the module languages: an interface itself can be viewed as “the type of a module.”
  • Documentation
  • The type declarations in procedure headers and module interfaces constitute a form of (checkable) documentation.
  • Language Safety
  • A safe language is one that protects its own abstractions.
  • Efficiency
  • Removal of dynamic checking; smart code-generation

Type System and Language Design

Language design should go hand-in-hand with type system design.

  • Languages without type systems tend to offer features that make type checking difficult or infeasible.

  • i.e. type system makes type checking easy

  • Concrete syntax of typed languages tends to be more complicated than that of untyped languages, since type annotations must be taken into account.

  • i.e. well-typed language is usually more complicated

In typed languages, the type system itself is often taken as the foundation of the design and the organizing principle in light of which every other aspect of the design is considered

Math Preliminaries (Excerpt)

image-20240223150223687

重点：

  1. \(R\) 的 domain 就是 \(s\) 有对应的 \(t\)，codomain 就是 \(t\) 有对应的 \(s\)
  2. 如果 \(s\) 只对应至多一个 \(t\)，那么 \(R\) 就是从 \(S\) 到 \(T\) 的一个偏函数
  3. 显然，如果 \(dom(R) = S\)，那么所有的 \(s\) 都对应某个（唯一的） \(t\)，因此就是（全）函数。
  4. 如果 \(s \notin dom(S)\)，那么，我们记 \(f(s) = \uparrow\)
  5. 注意：\(fail\) 和 \(\uparrow\) 是不一样的，详见 2.1.9 的补充

image-20240223151911340

重点：

  1. 预序就是自反+传递
  2. e.g. 我们在实数上定义一个预序： 给定函数 \(f : \mathbb R \to \mathbb R\)，我们定义，如果 \(f(x) \leq f(y)\)，那么，\(x \sqsubseteq y\)。
    • 如果 \(f\) 是单射，那么就是偏序（自反+传递+反对称）
    • 如果 \(f\) 不是单射，那么就只是预序而不是偏序
  3. e.g. 给定 \(\mathbb R\) 上的所有线段，通过长度定义序关系。那么，这显然是预序而不是偏序。

image-20240223152918077

重点：

  1. 自反闭包 \(R'\)
  2. 传递闭包 \(R^+\)
  3. 自反+传递（预序）闭包 \(R^*\)

另外，不难证明，如果 \(P\) is preserved by \(R\)，i.e. \(\forall s R s': P(s) \implies P(s')\)。

那么，\(\forall s: P(s) \implies P(s)\) ，而且 \(\forall s R s', s' R s'', \cdots: P(s) \implies P(s''^{\cdots})\)，从而 \(P\) is also preserved by \(R^*\)。

image-20240223153438489

注：\((m', n') < (m, n)\) i.f.f. \(m' < m \lor (m' = m \land n' < n)\)。