PFPL 笔记 - VI Dynamic Types

笔记 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)

由此可知, L\mathcal{L}{\rightarrow \forall} 至少具有和 Lnat \mathcal{L}{\text{nat }\rightarrow} 一样的表达力。事实上,它的表达力更强。

System F 可以表达 Godel’s T 的 evaluate function,但是 Godel’s T 没法表达自己的。当然二者都不是完备的,无法表达自己

注意到,多态性仅靠类型就能一定程度上推断出行为。例如对于类型 (t.tt)\forall (t. t \to t) 因为我们没有任何关于 t 的信息,为了总是能成立,它只能是 identity function Λ(t.λ(x:t)x)\Lambda (t. \lambda (x:t) x)

(题外话:上面的东西很直观,但我没理解如何证明的,但从我之前在知乎上看的东西看,似乎在范畴论里可以证出来 ∀ t → t 只有 ident function?)

参数化理论意味着,我们能够仅凭程序类型推导出关于程序行为的定理。这类定理有时被称为自由定理,因为它们是类型推导的“免费”结果,无需程序分析或验证即可推导。这些定理支撑了多态语言的卓越体验,即类型良好的程序在执行时往往能按预期运行。也就是说,满足类型检查器是正确性的充分条件。参数化对程序行为的限制非常严格,以至于只有相对较少的同类型程序会表现出非预期的行为,从而排除了编写代码时经常出现的一大类错误

Abstract Types

Existential Types

有了 forall 类型当然就有 exist 类型对吧。

据说 existential type 在 rust 里的对应是 dyn Trait —— 你不知道具体是什么类型 但是保证了这里存在一个类型 T 满足 Trait. 或者说,存在类型对应一个 trait 而它的一个实例对应一个 impl

比如

fn get_animal() -> impl Animal;

你不知道具体返回的是哪个 animal,可能是 Cat 或者 Dog,但是它保证了会返回一个 Animal,它其实是

get_animal : () → ∃ (t . ⟨ Animal ⟩ )

所以

其实 pack 就是构造了一个存在类型

ρ\rho 是 e2 的类型其实

Main idea of data abstracton is to introduce a interface

抽象类型一个重大的动力是实现一个抽象的接口,客户端不需要关注具体实现,只要二者都满足相同的接口和一个(后面我们会讲得性质(?))

Existential type 可以用 System F 表示:

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

这意味着如果给定了 (∀ t. τ → u ),也就是存在类型最后的那个 client 我们都当然能构造出 u ,这也是 ∃ 类型用 ∀ 类型 的解释

Bisimilar

// todo

Constructors and Kinds

注意到 nat → nat 和 nat list 可以被思考为

  • (→) 构造子作用在 nat 和 nat 上
  • list 作用在 nat 上

(就像函数那样)

我们是否要支持 type 上的计算?

比如考虑 ⟨ t₁ , t₂ ⟩ . l 似乎它等价于 t₁ 那么 ⟨ t₁ , t₂ ⟩ . l 的表达式也应该具有 t₁ 类型?

需要引入 definational equality of constructor 的概念,并且要求我们设计一个算法看它是否等价(甚至对于太强的类型系统可能遇到图灵完备问题?)

另一种方案:禁止这种 constructors 这样等价就只有完全长得一模一样的概念了
这个方案的问题是会让 substitution 的定义变得困难

这里新书选择了第一种方案,旧书选择了第二种

目前已经有了许多检查 type equality 的方式

Previous  Next

Loading...