PFPL 笔记 - IV Finite Data Types · Zero Calorie Drink Shop

Practical Foundations for Programming Languages 是 Robert Harper 的一本书，而这是我写的笔记 4

Chapter 11 Product Types ¶

可以参照 C++ 的 sturct 类型

定义 $\tau_1 \times \tau_2$ 为两个类型的 product，这个新类型包含两个类型。e = <e_1, e_2> 可以用 e.l e.r 取出 e 的 left 和 right projection

定义了 pair (binary product) 以后，一个 finite product (tuple) 也就很容易了。

在 product 上，我们可以简化第 9 章中定义的原始递归构造，以便只有前一个结果而不是前一个本身的结果被传递给后继分支。将其写为

同时在 product 上我们还能定义两个相互引用的递归函数，这是之前做不到的

\tau_EO :: <even :: nat -> nat, odd :: nat -> nat>

fix this: \tau_EO is <even = e_E, odd = e_O>

where e_E = \lambda (x: nat) ifz x { z => s(z) | s(y) => this.odd(y) },
      e_O = \lambda (x: nat) ifz x { z => z | s(y) => this.even(y) }

Chapter 12 Sum Types ¶

可以类比为 Typescript 的 | 类型，或者说 Rust 的 union 类型

(更正：typescript 的 | 类型并不是sum type，考虑 i32 + i32 ，应该有 33 的信息熵，但 Ts 的 i32 | i32 只有32 )

从 Sum Types 中我们很容易得到一个 bool 类型：

当然，从 sum types 中我们显然能得到 Option<T> 类型

Chapter 13 Pattern Matching ¶

模式匹配是乘积和和类型的消去形式的自然而方便的推广。例如，与其写

let x be e in x.l + x.r

来将 pair 的两对加起来，有了 pattern matching 我们可以写出

match e { <x_1, x_2> => x_1 + x_2 }

同样的，pattern matching 可以在 sum type 上，比如

$\text{match} \{ <l \cdot <>, x> \Rightarrow x + x | <r \cdot <>, y> \Rightarrow y * y \}$

Chapter 14 Generic Programing ¶

TODO