PFPL 笔记 - VII Subtyping · Zero Calorie Drink Shop

笔记 8 子类型

Subtyping ¶

子类型是大家用的很多的东西，简单来说，~~里氏替换原则~~ 如果 τ₁ <: τ 则任何需要 τ 类型的地方都可能在任何时候被 provide 一个 τ₁ 的值

子类型是一个 pre-order. 显然不是一个 total order. 但是为什么不是一个 partial order?

（可能是因为存在 class T1 < T {} 这种东西，在 norminal type 的情况下二者不等但是理论上可以互相替换吧，我们这章节似乎没有对 eq 做一个很好的定义）

比如 int <: rat <: real

Prod and Sum type ¶

这里看上去 prod type 是“逆变”的而 sum type 是“协变” 的，为什么？（虽然我不觉得在这里下标集合算逆变/协变性）

因为 sum type 是只有其中的某一个，那么大的下标集合会包含小的那个下标集合的所有可能取值，所以小的 I 产生的是大的 J 产生的子类型

prod type 是包含所有的，那么大的集合会包含小的那个集合的所有信息，所以大的集合是小集合的子类型

（很难不吐槽一下子类型是十分复杂的东西）

这是当类型的分量是子类型的时候的子类型关系，可以看出这显然是协变的，很符合直觉

Function Type ¶

函数类型的子类型的两条基本规则比较显然，我们以 Nat 和 Int 为例子

假如有 f : Int -> Int ，考虑将定义域缩小， f': Nat -> Int ，注意到 f'(-1) 没有定义，所以 f' 并不 <: f

考虑将定义域扩大， f': Real -> Int ，注意到 f' 对所有 f 可接受的输入产生合适的输出，所以 f' <: f

Int <: Real，同时 Real -> Int <: Int -> Int

同理，将值域扩大和缩小也能推出类似的规则，综上所述， function type 在定义域上逆变，在值域上协变。

Quantified Type ¶

这两条规则都比较直白，很好看懂

这两条关系要抽象很多，而且 23.11 作者还写错了呃呃，第二个 $\tau'$ 应该是 $\tau$

总而言之，首先让我们看看 universal type 的 contravariant 性质，让我们写一坨 ts 代码方便理解：

type A = { a: number };
type B = { b: string };

// 注意 typescript 是 structural type，可以认为这里自带一个 forall
// ∀ t : A, t -> A | undefined
function id_a(a: A): A | undefined {
  return a;
}

// ∀ t : A | B, t -> A | undefined
function id_a_or_b(a: A | B): A | undefined {
  return undefined;
}

// ∀ t : A & B, t -> A | undefined
function id_a_and_b(a: A & B): A | undefined {
  return a;
}

// A is a subtype of A | B
// A & B is a subtype of A
// so id_a_or_b is a subtype of id_a
// and id_a is a subtype of id_a_and_b

// universal quantification is contravariant
function test(fn: typeof id_a) {}

test(id_a); // ok
test(id_a_or_b); // ok
test(id_a_and_b); // error
// 类型“(a: A & B) => A | undefined”的参数不能赋给类型“(a: A) => A | undefined”的参数。
//   参数“a”和“a” 的类型不兼容。
//     不能将类型“A”分配给类型“A & B”。
//       类型 "A" 中缺少属性 "b"，但类型 "B" 中需要该属性。ts(2345)

存在类型的协变性质可以用它的 universal type 表示法解释，

因为 ∃ t . τ == ∀ u . (∀ t . τ → u) → u

所以两次逆变（ ∀ t . τ → u 的 t 逆变一次，它作为 → 的定义域逆变一次），我们可以知道 extensial type 是协变的

Singleton Kinds ¶

其实我没很明白这里的 Singleton 和 design patterns 的 singleton 有什么关系。或许它的意义是一个集合中只有一个元素吧。

Singleton Kind：我们可以把所有和 $\tau$ 相等的东西记做 $S(\tau)$

Subkinding: $\kappa_1 :<: \kappa_2$

我们现在在这里就给 type 配备了一个相等性 $\equiv$

$\dfrac{\Delta \vdash c :: S(d)} {\Delta \vdash c \equiv d :: \text{Type}}$

详细规则见

Dependent Kinds ¶

higher kinds 可以表达一个 $T \to S(int)$ 这样的东西，接受一个类型返回一个类型的构造子

但没法非常 exactly 地表达 $id: T \to T$ 或者 $HP: T \to T \times T$

（应该说）

id : a -> a

这样的东西的准确的性质，因为没法表达出这些 T 相同。你确实能构造出一个 id 来但没法表达出它是 id 的那个相等的性质。

（也就是说，直接用 universal type 的表达力不够）

引入 dependent kinds，

为什么要用 $\sum$ 表示 prod，用 $\prod$ 表示 arrow 呢？这确实有点呃抽象。但写都这么写了也就这样吧。

或许我们能从信息论的角度去理解， $(a, b)$ 的信息实际上是两个东西信息的和 $a + b$ 而 $a \to b$ 的信息量实际上是 $a \times b$ （列表就知道）

（同学观点：实际上是 dependent sum 和 dependent prod：）

考虑一个 $\sum$ 它实际上给定了第一个参数第二个就被确定了这实际上是 sum 的性质，虽然有很多种可能性但是给定了第一个只能唯一的是第二个

有了这个 dependent kinds 我们就能表达出像上面这样的函数的类型，它接受一个 pair 返回它们的交换（和下面这个差不多）

swap_pair : a × b → b × a

Higher Singletons ¶

我们 require c :: T 来构造 $S(c)$ 所以现在我们引入 higher kinds 来让 $S(c::\kappa)$ 也能 equivalent to $c$

24.13b 和 24.13c 是两条分配律

dependent kind 的一个实际应用可以用 TypeScript 举例子：

type Shape = "circle" | "square";
type CircleConfig = { radius: number };
type SquareConfig = { sideLength: number };
type Config<S extends Shape> = S extends "circle"
  ? CircleConfig
  : S extends "square"
  ? SquareConfig
  : never;

function createShape<S extends Shape>(shapeType: S, config: Config<S>): void {
  // ....
}

createShape("circle", { radius: 10 });
createShape("square", { sideLength: 5 });
createShape("circle", { sideLength: 5 }); // fail~~~~