【正文】 算 ? 良形上下文的公理和推理規(guī)則 (var) (add var) 這兩條規(guī)則可用于多個類型系統(tǒng) 第二條規(guī)則可用于推導 x:A, y:B ? x:A這樣的斷言 ?, x : A context ?, x : A ? x : A ? ? A : B ?, x : C context ?, x : C ? A : B 直謂式多態(tài)演算 ? U1和 U2類型表達式的語法規(guī)則 – U1的類型表達式由三個公理和推理規(guī)則給出 ? ? b: U1 (cst U1) （限制到 U1的變量） (var) (? U1) ? ? ? : U1, ? ? ?? : U1 ? ? ? ? ?? : U1 ?, x : A context ?, x : A ? x : A 直謂式多態(tài)演算 – 第二 個全域 U2包含類型 U1和多態(tài)函數類型 (U1?U2) (?U2) – 雖然有 屬于 U2的類型表達式，但是沒有 U2的變量 – 如果 加了變量和 ?抽象到 U2上，它就會導致形式是 ?t:U2.?的類型，它將屬于第三個全域 U3 ?, t : U1 ? ? : U2 ? ? (? t : U1. ?) : U2 ? ? ? : U1 ? ? ? : U2 直謂式多態(tài)演算 ? 例 證明 ?t: ? t是屬于 U2的良形的類型表達式 ? context 由 (empty context) t: U1 context 由 (U1 context) t: U1 ? t: U1 (var) t: U1 ? t ? t: U1 (?U1) t: U1 ? t ? t: U2 (U1?U2) ? ? ( ?t: ? t) : U2 (?U2) 直謂式多態(tài)演算 ? 項的語法 （先給 ??, ? 預備 項的文法 ） M ::= b | x | ?x:?. M | MM | ?t: | M? ? 定型規(guī)則用來判斷項是否為良類型的 (var) (add var) ?, x : A context ?, x : A ? x : A ? ? A : B ?, x : C context ?, x : C ? A : B 直謂式多態(tài)演算 ? ? c: ? (cst) (?Intro) (?Elim) 任何 ??項（可能包括了用類型變量取代類型常量）都是 ??,?的項 ?, x :? ? M : ?? ? ? ? : U1 ? ? ?? : U1 ? ? (?x : ?. M) : ? ? ?? ? ? M : ? ? ?? ? ? N : ? ? ? MN : ?? 直謂式多態(tài)演算 (? Intro) (? Elim) (type eq) 在類型 ?t: U1.?中將省略 t所屬的全域 U1， 寫成 ?t.? ?, t : U1 ? M : ? ? ? (?t : U1. M) : (?t: U1.? ) ? ? M : (?t: U1.? ) ? ? ? : U1 ? ? M ? : [?/t ]? ? ? M : ?1 ? ? ?1 = ?2 : Ui ? ? M : ?2 直謂式多態(tài)演算 (? Intro) (? Elim) (type eq) 若 ? ? M??是從公理和 ??, ?定型規(guī)則可推導，則 說， M在上下文 ?中是類型為 ?的 ??, ?項 ?, t : U1 ? M : ? ? ? (?t : U1. M) : (?t: U1.? ) ? ? M : (?t: U1.? ) ? ? ? : U1 ? ? M ? : [?/t ]? ? ? M : ?1 ? ? ?1 = ?2 : Ui ? ? M : ?2 直謂式多態(tài)演算 ? 規(guī)則 U1 ?U2 和規(guī)則 U1 :U2 規(guī)則 U1 ?U2 – 可以只用一個 ?形成規(guī)則 – U1 ?U2沒有在該語言上設置任何額外的語義限制 規(guī)則 U1 :U2 – 因為 ????在任意 U2類型上無任何有意義的運算，因此看起來沒有任何理由取 U1 :U2 – 在 ????的非直謂式拓展中，加入 U1 :U2規(guī)則將是一個合理的語言設計 直謂式多態(tài)演算 和其它形式多態(tài)性的比較 ? 其它兩種演算都可看成直謂式多態(tài)演算的特殊情況 – 非直謂 式類型化 ?演算 強加“全域等式” U1 = U2 – “ type: type” 演算 強加了等式 U1 = U2和條件 U1:U2 直謂式多態(tài)演算 ? 非直謂式演算 – 在 ??, ?中已經有 U1 ?U2, – 加入逆向包含 U2 ?U1來獲得 U1 = U2 (U2?U1) ? ? ? : U2 ? ? ? : U1 直謂式多態(tài)演算 ? 例 – 證明語法 斷言 ? ? (I (??t))I: ? ?t， 其中 I ? ?t:U1.?x: ? 由（ ??, ?的定型規(guī)則 ） ? ? I: (??t)， 其中 (??t):U2 ? (??t):U1 由 (U2 ?U1) ? I (??t) : (??t) ? (??t) 由 (? Elim) ? I (??t) I : (??t) 由 (? Elim) 直謂式多態(tài)演算 ? type : type 加上 U2 = U1和 U1:U2 – 對前者加語法規(guī)則（ U2 ?U1） – 對后者加公理 ? ? U1:U2 (U1:U2) – 可以寫出非常復雜的類型函數 – 一個有效的 編譯時的類型檢查算法是不可能的 直謂式多態(tài)演算 ? ??? ?的簡化語法 – 第一個約定是使用兩類變量 項變量 x, y, z, … 類型變量 r, t, s, … 代表 U1的類型 – 第二個 約定 對 U1的類型表達式使用 ?, ??, ?1, … 對 U2的類型表達式使用 ?, ??, ?1, … – U1和 U2的類型表達式的語法 ? ::= t | b | ? ? ? ? ::= ? | ?t.? 直謂式多態(tài)演算 – 上下文 ? = {x1: ?1, … , xk: ?k} －－不再需要類型變量 – 語法簡化后的規(guī)則 {x: ?} ? x: ? (var) ? ? c:? (cst) (add var) (?Intro) ? ? M : ? ?, x : ? ? M : ? ?, x :? ? M : ??