【正文】 把 subst函數(shù) 用于 t后所得的類(lèi)型表達(dá)式是 t的一個(gè)實(shí)例，用 S (t)表示。 例子（ s t 表示 s是 t 的實(shí)例 ） pointer ( integer ) pointer (? ) pointer ( real ) pointer (? ) integer ? integer ? ?? pointer (? ) ? ? ? 多 態(tài) 函 數(shù) 下面左邊的類(lèi)型表達(dá)式不是右邊的實(shí)例 integer real 代換不能用于基本類(lèi)型 integer ? real ? ? ? ? 的代換不一致 integer ? ? ? ?? ? 的所有出現(xiàn)都應(yīng)該代換 多 態(tài) 函 數(shù) 合一 如果存在某個(gè)代換 S使得 S (t1) = S (t2)， 那么這兩個(gè)表達(dá)式 t1和 t2能夠 合一 最一般的合一代換 ? S(t1) = S(t2)； ? 對(duì)任何其它滿足 S?(t1) = S?(t2)的代換 S?， 代換S?(t1)是 S (t1)的實(shí)例 多 態(tài) 函 數(shù) 多態(tài)函數(shù)的類(lèi)型檢查 多態(tài)函數(shù)和普通函數(shù)在類(lèi)型檢查上的區(qū)別 (1)同一多態(tài)函數(shù)的不同出現(xiàn)無(wú)須變?cè)邢嗤?lèi)型 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)必須把類(lèi)型相同的概念推廣到類(lèi)型合一 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)必須把類(lèi)型相同的概念推廣到類(lèi)型合一 (3)要記錄表達(dá)式合一的結(jié)果 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ù) 檢查多態(tài)函數(shù)的翻譯方案 E?E1 (E2 ) {p := mkleaf (newtypevar)。 unify (E1. type, mknode ( ??‘, , p) )。 E. type := p} E ? E1, E2 {E. type := mknode ( ??‘, , )} E ? id {E. type := fresh (lookup())} 多 態(tài) 函 數(shù) apply: ?o derefo:pointer(?o) ? ?o apply : ?i derefi : pointer(?i) ? ?i q: pointer(pointer(integer)) 表 達(dá) 式 ： 類(lèi) 型 代 換 q : pointer(pointer(integer)) derefi : pointer(?i) ? ?i derefi(q) : pointer(integer) ? i= pointer(integer) derefo : pointer(?o) ? ?o derefo(derefi (q)) : integer ?o = integer 多 態(tài) 函 數(shù) 確定表長(zhǎng)度的 ML函數(shù) fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1。 多 態(tài) 函 數(shù) length : ? 。 lptr : ? 。 if : ?? . boolean ?? ?? ?? 。 null : ?? . list (?) ? boolean 。 tl : ?? . list (?) ? list (?) 。 0 : integer 。 1 : integer 。 + : integer ? integer ? integer 。 match : ?? . ? ?? ? ? 。 match ( length (lptr), if (null (lptr), 0, length (t1(lptr)) +1) ) 多 態(tài) 函 數(shù) 行 定 型 斷 言 代 換 規(guī) 則 (1) lptr : ? (Exp Id) (2) length : ? (Exp Id) (3) length(lptr) : ? ? = ? ? ? (Exp FunCall) (4) lptr : ? 從 (1)可得 (5) null : list(?n) ? boolean (Exp Id)和(Type Fresh) (6) null(lptr) : boolean ? = list (?n) (Exp FunCall) (7) 0 : integer (Exp Num) (8) lptr : list(?n) 從 (1)可得 多 態(tài) 函 數(shù) 行 定 型 斷 言 代 換 規(guī) 則 (9) tl : list(?t) ? list(?t) (Exp Id)和(Type Fresh) (10) t1(lptr) : list(?n) ?t = ?n (Exp FunCall) (11) length : list(?n) ? ? 從 (2)可得 (12) length(t1(lptr)) : ? (Exp FunCall) (13) 1 : integer (Exp Num) (14) + : integer ? integer ? integer (Exp Id) 多 態(tài) 函 數(shù) 行 定 型 斷 言 代 換 規(guī) 則 (15) length (t1(lptr)) +1 : integer ? = integer (Exp FunCall) (16) if : boolean ??i ??i ??i (Exp Id)和(Type Fresh) (17) if ( ... ) : integer ?i = integer (Exp FunCall) (18) match : ?m ? ?m ??m (Exp Id)和(Type Fresh) (19) match ( … ) : integer ?m=integer (Exp FunCall) 多 態(tài) 函 數(shù) fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1。 length函數(shù)的類(lèi)型是 ??. list (?) ? integer 函數(shù)和運(yùn)算符的重載 重載符號(hào) 有多個(gè)含義，但在引用點(diǎn) 的含義都是唯一的 例如 加法算符 +可用于不同類(lèi)型，是不同的函數(shù) 在 Ada中， ( ) 是重載的， A( I ) 有不同含義 子表達(dá)式的可能類(lèi)型集合 例 Ada語(yǔ)言 聲明： function ―? ‖ (i, j : integer ) return plex。 function ―? ‖ (x, y : plex ) return plex。 使得算符 ?重載， 可能的類(lèi)型包括： integer ? integer ? integer integer ? integer ? plex plex ? plex ? plex 子表達(dá)式的可能類(lèi)型集合 例 Ada語(yǔ)言 聲明： function ―? ‖ (i, j : integer ) return plex。 function ―? ‖ (x, y : plex ) return plex。 使得算符 ?重載， 可能的類(lèi)型包括： integer ? integer ? integer 2 ? (3 ? 5) integer ? integer ? plex plex ? plex ? plex 子表達(dá)式的可能類(lèi)型集合 例 Ada語(yǔ)言 聲明： function ―? ‖ (i, j : integer ) return plex。 function ―? ‖ (x, y : plex ) return plex。 使得算符 ?重載， 可能的類(lèi)型包括： integer ? integer ? integer 2 ? (3 ? 5) integer ? integer ? plex (3 ? 5) ? z plex ? plex ? plex z是復(fù)型 以 函數(shù)作用為例，考慮類(lèi)型檢查 在每個(gè)表達(dá)式都有唯一的類(lèi)型 時(shí)，函數(shù)作用 的類(lèi)型檢查是： E?E1 (E2 ) {E. type := if E2. type = s and E1. type = s ? t then t else type_ error } 確定表達(dá)式可能類(lèi)型的集合 產(chǎn) 生 式 語(yǔ) 義 規(guī) 則 E? ? E E?.types := E. types E ? id E. types := lookup(id. entry) E ? E1 (E2) E. types := {t | E2. types中存在一個(gè) s， 使得 s ? t屬于 } 注意 : 重載的函數(shù)和符號(hào)的引入使得程序員可以用一個(gè)名字或符號(hào)表示多個(gè)不同類(lèi)型的函數(shù)或運(yùn)算，它也不像引入類(lèi)型構(gòu)造器或類(lèi)型變量那樣能豐富我們所能表達(dá)的類(lèi)型。 例 題 1 C語(yǔ)言 ? 稱(chēng) amp。為地址運(yùn)算符， amp。a為變量 a的地址。 ? 數(shù)組名代表數(shù)組的首地址。 問(wèn)題： 如果 a是一個(gè)數(shù)組名，那么表達(dá)式 a和 amp。a的值都是數(shù)組 a的首地址，它們的使用是否有區(qū)別的？ 例 題 1 C語(yǔ)言 ? 稱(chēng) amp。為地址運(yùn)算符， amp。a為變量 a的地址。 ? 數(shù)組名代表數(shù)組的首地址。 問(wèn)題： 如果 a是一個(gè)數(shù)組名，那么表達(dá)式 a和 amp。a的值都是數(shù)組 a的首地址，它們的使用是否有區(qū)別的？ 用四個(gè) C文件的編譯報(bào)錯(cuò)或運(yùn)行結(jié)果來(lái)提示。 例 題 1 typedef int A[10][20]。 A a。 A *fun() { return(a)。 } 該函數(shù)在 Linux上用 gcc編譯時(shí) ， 報(bào)告的錯(cuò)誤如下： 第 6行： warning: return from inpatible pointer type 例 題 1 typedef int A[10][20]。 A a。 A *fun() { return(amp。a)。 } 該函數(shù)在 Linux上用 gcc編譯時(shí) ， 沒(méi)有錯(cuò)誤 。 例 題 1 typedef int A[10][20]。 typedef int B[20]。 A a。 B *fun() { return(a)。 } 該函數(shù)在 Linux上用 gcc編譯時(shí) ， 沒(méi)有錯(cuò)誤 。 例 題 1 typedef int A[10][20]。 A a。 fun() { printf(―%d,%d,%d\n‖, a, a+1, amp。a+1)。} main() { fun()。 } 該程序的運(yùn)行結(jié)果是： 134518112, 134518192, 134518912 例 題 1 結(jié)論 對(duì)一個(gè) t 類(lèi)型的數(shù)組 a[ i1 ][ i2 ]… [ in ]來(lái)說(shuō) ， 表達(dá)式 a的類(lèi)型是： pointer(array(0.. i2 –1, … array(0.. in –1, t)… )) 表達(dá)式 amp。a的類(lèi)型是： pointer(array(0.. i1 –1, … array(0.. in –1, t)… )) 例 題 2 在 X86/Linux機(jī)器上 ， 編譯器報(bào)告最后一行有錯(cuò)誤： inpati