笔记 7
Girard’s System F ¶
之前我们讨论的语言都非常地单态,每个表达式都有独立的一个类型,不支持多态。
这一章讲了通过 System F i.e. polymorphic typed lambda calculus 如何实现多态的。
引入一种全称类型,∀ t . τ
Λ t . e
是一个泛型函数,它的类型是一个 ∀ t . τ
比如
Λ t . λ (x : t) ↦ x
是一个 polymorphic identity function 具有类型
∀ t . t ↦ t
我们自然的可以把它叫作 unit, 而上面那个函数其实就是 ⟨ ⟩
它完全就是 null tuple 因为它是这个类型的唯一个元素
二元组也能被很好的定义,和 Chapter 17 untyped lambda calculus 一样:
τ₁ × τ₂ ≝ ∀ r . (τ₁ → τ₂ → r) → r
⟨e₁, e₂⟩ ≝ Λ r . λ (x : τ₁ → τ₂ → r) ↦ x e₁ e₂
e.l ≝ e[τ₁] λ (x : τ₁) (y: τ₂) ↦ x
e.l ≝ e[τ₂] λ (x : τ₁) (y: τ₂) ↦ y
容易看出这就是 17 章定义的 pair 加上了泛型类型。
sum type 也是容易定义的,只需要看出来 sum type 可以看作一个函数链,其中只有一个函数是能被调的
还有自然数。容易把自然数看成对于泛型 t 的
t -> (t -> t) -> t
比如
zero :: t -> (t -> t) -> t
zero z s = z
succ :: nat -> nat
succ e z s = s(e z s)
由此可知, 至少具有和 一样的表达力。事实上,它的表达力更强。
注意到,多态性仅靠类型就能一定程度上推断出行为。例如对于类型 因为我们没有任何关于 t 的信息,为了总是能成立,它只能是 identity function
参数化理论意味着,我们能够仅凭程序类型推导出关于程序行为的定理。这类定理有时被称为自由定理,因为它们是类型推导的“免费”结果,无需程序分析或验证即可推导。这些定理支撑了多态语言的卓越体验,即类型良好的程序在执行时往往能按预期运行。也就是说,满足类型检查器是正确性的充分条件。参数化对程序行为的限制非常严格,以至于只有相对较少的同类型程序会表现出非预期的行为,从而排除了编写代码时经常出现的一大类错误
Abstract Types ¶
Existential Types ¶
有了 forall 类型当然就有 exist 类型对吧。
据说 existential type 在 rust 里的对应是 dyn Trait
—— 你不知道具体是什么类型 但是保证了这里存在一个类型 T 满足 Trait. 或者说,存在类型对应一个 trait 而它的一个实例对应一个 impl
所以
其实 pack 就是构造了一个存在类型
// todo