7.1引言 ·三种多态性之间的简单区别 1、直谓式多态性 -Id(nat→nat)=入x:nat→nat.x 2.非直谓式多态性 -IdΠt:T.t>t)=入x:Πt:T.t->t).x 3、ype:pe IdT=入x:T.x (Id T):T->T
7.1 引 言 • 三种多态性之间的简单区别 1、直谓式多态性 – Id (nat → nat) = x : nat → nat. x 2. 非直谓式多态性 – Id (t: T. t → t) = x : (t: T. t → t). x 3、type : type Id T = x:T. x (Id T): T → T
7.1引 言 参数多态性和特定多态性 1、参数化多态性 一个多态函数对任何类型都使用“本质上一样的 算法” 2、特定多态性 -可以测试类型变元的值， 根据它的类型类型选择 某个分支 ad hoc compose 入：T.入s:T.入t:T.入f:S→t.入g:r→S.入x:r if Eg?st thenf(f(g x))else f(g x)
7.1 引 言 • 参数多态性和特定多态性 1、参数化多态性 – 一个多态函数对任何类型都使用“本质上一样的 算法” 2、特定多态性 – 可以测试类型变元的值，根据它的类型类型选择 某个分支 ad_hoc_compose r: T. s: T. t: T.f : s → t. g: r → s. x: r. if Eq? s t then f (f (g x)) else f (g x)
7.2直谓式多态演算 7.2.1类型和项的语法 ·入，Ⅱ的类型分成两类 入类型 全域U “小”全域 一用Ⅱ构造的多态类型 全域U, “大”全域 各类表达式（上下文、类型表达式、项）的 语法各由一个断言证明系统给出 在入，中将使用形式为TA:B的断言 一厂是上下文，指出每个变量的类型或全域 -A是类型表达式，则B是U1,U2 -A是项，则B是类型表达式
7.2 直谓式多态演算 7.2.1 类型和项的语法 • → 的类型分成两类 – →类型 全域 U1 “小”全域 – 用构造的多态类型 全域 U2 “大”全域 • 各类表达式（上下文、类型表达式、项）的 语法各由一个断言证明系统给出 • 在→ 中将使用形式为 A: B的断言 – 是上下文，指出每个变量的类型或全域 – A是类型表达式，则B是U1，U2 – A是项，则B是类型表达式
7.2直谓式多态演算 良形上下文的公理和推理规则 一上下文是一个有序序列，它给变量以类型或全域 =1:A1),Vk:A 每个A必须仅在假设y:A1,,1:A1下就可证 明为良形的 可以使用公理和推理规则来将它形式化 例：t:U入x:t→t.入y:t. 确定xy类型时的上下文：t:U,x:t→t,J:t
7.2 直谓式多态演算 • 良形上下文的公理和推理规则 – 上下文是一个有序序列，它给变量以类型或全域 = v1 : A1 , …, vk : Ak – 每个Ai必须仅在假设v1 : A1 , …, vi -1 : Ai–1下就可证 明为良形的 – 可以使用公理和推理规则来将它形式化 – 例：t : U1 .x : t → t.y: t. xy 确定xy类型时的上下文：t : U1 , x : t → t, y: t
7.2直谓式多态演算 ·良形上下文的公理和推理规则 ☑ context (empty context） I context t不在T中 (U context) T,t:U context o:Ui x不在T中 T,x:o context (U;type context)
7.2 直谓式多态演算 • 良形上下文的公理和推理规则 context (empty context) t不在中 (U1 context) x不在中 (Ui type context) context , t : U1 context : Ui , x : context