【文章內(nèi)容簡(jiǎn)介】 { = if == boolean then S1. type else type_error } S ? S1。 S2 {S. type = if S1. type == void and S2. type == void then void else type_error } 簡(jiǎn)單類型檢查器的說(shuō)明 類型檢查 ——程序 P ? D。 S {P. type = if S. type == void then void else type_error } 簡(jiǎn)單類型檢查器的說(shuō)明 類型轉(zhuǎn)換 E ? E1 op E2 { = if == integer and == integer then integer else if == integer and == real then real else if == real and == integer then real else if == real and == real then real else type_error } 多 態(tài) 函 數(shù) 為什么要使用多態(tài)函數(shù) 例：用 Pascal語(yǔ)言寫(xiě)不出求表長(zhǎng)度的通用程序 若有下面的類型 type link = ?cell 。 cell = record info : integer。 next : link end。 針對(duì)這個(gè)類型，可以寫(xiě)出下頁(yè)的表長(zhǎng)函數(shù) 多 態(tài) 函 數(shù) function length(lptr : link) : integer。 var len : integer。 begin len := 0。 while lptr nil do begin len := len + 1。 lptr := lptr?. next end。 length := len end。 計(jì)算過(guò)程并不涉及 表元的數(shù)據(jù)類型 但語(yǔ)言的類型系統(tǒng) 使得該函數(shù)不能通用 多 態(tài) 函 數(shù) 例：用 ML語(yǔ)言很容易寫(xiě)出求表長(zhǎng)度的程序而不必管表元的類型 fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1。 多 態(tài) 函 數(shù) 例：用 ML語(yǔ)言很容易寫(xiě)出求表長(zhǎng)度的程序而不必管表元的類型 fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1。 length ( [―sun‖, ―mon‖, ―tue‖] ) length ( [10, 9, 8 ] ) 都等于 3 多 態(tài) 函 數(shù) ? 多態(tài)函數(shù) – 允許變?cè)念愋陀卸喾N不同的情況 – 函數(shù)體中的語(yǔ)句的執(zhí)行能適應(yīng)變?cè)愋陀卸喾N不同的情況（區(qū)別于重載的特征） ? 多態(tài)算符 – 例如： 數(shù)組索引 、 函數(shù)應(yīng)用、通過(guò)指針間接訪問(wèn) – 相應(yīng)操作的代碼段接受不同類型的數(shù)組、函數(shù)等 – C語(yǔ)言手冊(cè)中關(guān)于取地址算符 amp。的論述是： 如果運(yùn)算對(duì)象的類型是 ‘ … ’ ，那么結(jié)果類型是指向 ‘ … ’ 的指針 ” 多 態(tài) 函 數(shù) 類型變量 length的類型可以寫(xiě)成 ??.list(?) ? integer 允許使用類型變量，還便于討論未知類型 – 在不要求標(biāo)識(shí)符的聲明先于使用的語(yǔ)言中，通過(guò)類型變量的使用去確定程序變量的類型 多 態(tài) 函 數(shù) ? 例 function deref (p)。 begin return p? end。 多 態(tài) 函 數(shù) ? 例 function deref (p)。 對(duì) p的類型一無(wú)所知： ? begin return p? end。 多 態(tài) 函 數(shù) ? 例 function deref (p)。 對(duì) p的類型一無(wú)所知： ? begin return p? ? = pointer(? ) end。 多 態(tài) 函 數(shù) ? 例 function deref (p)。 對(duì) p的類型一無(wú)所知： ? begin return p? ? = pointer(? ) end。 deref的類型是 ??. pointer(? ) ? ? 多 態(tài) 函 數(shù) 一個(gè)含多態(tài)函數(shù)的語(yǔ)言 P ? D。 E 引入類型變量、笛卡 D ? D。 D | id : Q 兒積類型、多態(tài)函數(shù) Q ? ?typevariable. Q | T T ? T ??‘T | T ? T | unaryconstructor ( T ) | basictype | typevariable | ( T ) E ? E (E ) | E, E | id 多 態(tài) 函 數(shù) 一個(gè)含多態(tài)函數(shù)的語(yǔ)言 P ? D。 E 引入類型變量、笛卡 D ? D。 D | id : Q 兒積類型、多態(tài)函數(shù) Q ? ?typevariable. Q | T T ? T ??‘T | T ? T 這是一個(gè)抽象語(yǔ)言 , | unaryconstructor ( T ) 忽略了函數(shù)定義的 | basictype 函數(shù)體 | typevariable | ( T ) E ? E (E ) | E, E | id 多 態(tài) 函 數(shù) 一個(gè)含多態(tài)函數(shù)的語(yǔ)言 P ? D。 E D ? D。 D | id : Q Q ? ?typevariable. Q | T T ? T ??‘T | T ? T | unaryconstructor ( T ) 一個(gè)程序： | basictype deref : ??. pointer(? ) ?? 。 | typevariable q : pointer (pointer (integer))。 | ( T ) deref (deref (q)) E ? E (E ) | E, E | id 多 態(tài) 函 數(shù) 類型系統(tǒng)中增加的推理規(guī)則 ? 環(huán)境規(guī)則 (Env Var) ? 語(yǔ)法規(guī)則 (Type Var) (Type Product) ? |? ?, ? ? dom (?) ?, ? |? ? ?1, ? , ?2 |? ? ?1, ? , ?2 |? ? ? |? T1, ? |? T2 ? |? T1 ? T2 多 態(tài) 函 數(shù) 類型系統(tǒng)中增加的推理規(guī)則 ? 語(yǔ)法規(guī)則 (Type Parenthesis) (Type Forall) (Type Fresh) ? |? T ? |? (T ) ?, ? |? T ? |? ??.T ? |? ??.T , ?, ?i |? ? ?, ?i |? [?i /?] T 多 態(tài) 函 數(shù) 類型系統(tǒng)中增加的推理規(guī)則 ? 定型規(guī)則 (Exp Pair) (Exp FunCall) (其中 S是 T1和 T3的最一般的合一代換 ) ? |? E1: T1， ? |? E2: T2 ? |? E1, E2: T1 ? T2 ? |? E1: T1 ? T2, ? |? E2: T3 ? |? E1 (E2) : S(T2) 多 態(tài) 函 數(shù) 代換、實(shí)例和合一 代換 : 類型表達(dá)式中的類型變量用其所代表的類型表達(dá)式去替換 多 態(tài) 函 數(shù) 代換、實(shí)例和合一 代換 : 類型表達(dá)式中的類型變量用其所代表的類型表達(dá)式去替換 function subst (t : type_expression ) : type_expression。 begin if t是基本類型 then return t else if t是類型變量 then return S(t) else if t 是 t1? t2 then return subst(t1) ? subst(t2) end 多 態(tài) 函 數(shù) 實(shí)例 把 subst函數(shù) 用于 t后所得的類型表達(dá)式是 t的一個(gè)實(shí)例，用 S (t)表示。 例子（ s t 表示 s是 t 的實(shí)例 ） pointer( integer ) pointer(? ) pointer( real ) pointer(? ) integer ? integer ? ?? pointer(? ) ? ? ? 多 態(tài) 函 數(shù) 下面左邊的類型表達(dá)式不是右邊的實(shí)例 integer real 代換不能用于基本類型 integer ? real ? ? ? ? 的代換不一致 integer ? ? ? ? ? ? 的所有出現(xiàn)都應(yīng)該代換 多 態(tài) 函 數(shù) 合一 如果存在某個(gè)代換 S使得 S(t1) = S(t2)， 那么這兩個(gè)表達(dá)式 t1和 t2能夠 合一 最一般的合一代換 S ? S(t1) = S(t2)； ? 對(duì)任何其它滿足 S?(t1) = S?(t2)的代換 S?， 代換S?(t1)是 S(t1)的實(shí)例 多 態(tài) 函 數(shù) 多態(tài)函數(shù)的類型檢查 多態(tài)函數(shù)和普通函數(shù)在類型檢查上的區(qū)別 (1)同一多態(tài)函數(shù)的不同出現(xiàn)無(wú)須變?cè)邢嗤愋? apply: ?o derefo:pointer(?o) ? ?o apply : ?i derefi : pointer(?i)? ?i q: pointer(pointer(integer)) deref(deref (q ))的帶標(biāo)記的語(yǔ)法樹(shù) 多 態(tài) 函 數(shù) (2)必須把類型相同的概念推廣到類型合一 apply: ?o derefo:pointer(?o) ? ?o apply : ?i derefi : pointer(?i)? ?i q: pointer(pointer(integer)) deref(deref (q ))的帶標(biāo)記的語(yǔ)法樹(shù) 多 態(tài) 函 數(shù) (2)必須把類型相同的概念推廣到類型合一 (3)要記錄類型表達(dá)式合一的結(jié)果 apply: ?o derefo:pointer(?o) ? ?o apply : ?i derefi : pointer(?i