編譯原理 類型檢查

1、章類型檢查內(nèi)容m類型系統(tǒng)m類型表達(dá)式的等價m類型轉(zhuǎn)換m函數(shù)和運算符的重載m多態(tài)函數(shù)m一致化算法靜態(tài)檢查（static checking）m類型檢查（type check）q操作對象必須與操作符匹配：函數(shù)名相加m控制流檢查（flow-of-control check）qbreak必須退出while、for、switchm唯一性檢查（uniqueness check）q對象（變量、標(biāo)號）定義必須唯一m名字關(guān)聯(lián)檢查（name-related check）q相同名字在不同位置類型檢查m檢查語法結(jié)構(gòu)的類型與上下文匹配q簡單的類型檢查q兩個類型的匹配m代碼生成要利用類型信息m重載，多態(tài)6.1 類型系統(tǒng)m語

2、法結(jié)構(gòu)、類型、將類型賦予語法結(jié)構(gòu)q+, -, *的兩個運算數(shù)均為整數(shù)，結(jié)果為整數(shù)q&的結(jié)果為指向操作對象的指針，若操作對象類型為T，結(jié)果類型為“指向T的指針”m每個表達(dá)式都有一個相關(guān)聯(lián)的類型m類型是有結(jié)構(gòu)的！指針m基本類型：語言內(nèi)部支持類型m結(jié)構(gòu)類型：組合基本類型構(gòu)成新類型6.1.1 類型表達(dá)式mtype expression用以表示語言結(jié)構(gòu)的類型m基本類型或用類型構(gòu)造符組合基本類型q基本類型：boolean, char, integer, real, type_error, void1.類型名類型表達(dá)式（續(xù)）q類型構(gòu)造符 數(shù)組：T是類型表達(dá)式，I為索引集合（整數(shù)范圍），則array(I, T

3、)是一個類型表達(dá)式，表示元素為類型T的數(shù)組類型int A10;array(0, , 9, integer) 笛卡兒積：T1、T2為類型表達(dá)式，則T1T2為類型表達(dá)式類型表達(dá)式（續(xù)） 記錄：與笛卡兒積的不同之處僅在于記錄的域有名字。元組typedef struct int address;char lexeme15; row;row table101;類型表達(dá)式為：record(addressinteger)(lexemearray(0, , 15, char)類型表達(dá)式（續(xù)） 指針：T為類型表達(dá)式，則pointer(T)為類型表達(dá)式，表示“指向類型為T的對象的指針”類型row *p;point

4、er(row) 函數(shù)：數(shù)學(xué)上，一個集合“定義域”到另一個集合“值域”的映射。程序語言，定義域類型D到值域類型R的映射：DR。%運算符(intint)intint *f(char a, char b);(charchar)pointer(integer)不考慮函數(shù)返回數(shù)組、函數(shù)類型的情況(integerinteger)(integerinteger)q可使用類型表達(dá)式變量圖表示類型表達(dá)式m(charchar)pointer(integer)6.1.2 類型系統(tǒng)mtype system：規(guī)則的集合規(guī)則將類型表達(dá)式賦予程序的不同部分m類型檢查程序：實現(xiàn)一個類型系統(tǒng)m語法制導(dǎo)方式實現(xiàn)嵌入語義規(guī)則6.1

5、.2靜態(tài)/動態(tài)檢查m靜態(tài)編譯器進(jìn)行動態(tài)運行時進(jìn)行m可靠類型系統(tǒng)，強(qiáng)類型語言編譯器無type_error運行時無類型錯誤mint a10, i; b=ai;需動態(tài)檢查m安全領(lǐng)域也涉及類型檢查（緩沖溢出問題）6.1.4 錯誤恢復(fù)m最低要求：報告類型錯誤位置m錯誤處理應(yīng)融入規(guī)則中m錯誤修正比描述正確程序更困難q根據(jù)錯誤的程序、處理缺失信息，來推測正確類型在變量使用之前無需定義它q類型變量可用來處理這種問題6.2 一個簡單的類型檢查器6.2.1 一種簡單語言m用綜合屬性type保存類型表達(dá)式P D ; ED D ; D | id : TT char | integer | array num of T

6、 | TE literal | num | id | E mod E | E E | Em基本類型：char、integer、type_errorm例CODESome Types Expressionskey:integer; array256 of char array(1.256, char)key mod 1999 integer pointer(integer)翻譯模式P D ; E D D ; D D id : T addtype(id.entry, T.type) T charT.type = char T integer T.type = integer T array num

7、of TT.type=array(1.num.val,T.type)T T T.type = pointer(T.type) mDid:T的規(guī)則在符號表保存標(biāo)識符類型mT.type由后幾個產(chǎn)生式語義規(guī)則計算mPD;E，D在E之前，保證在檢查表達(dá)式類型之前類型已經(jīng)保存入符號表6.2.2 表達(dá)式類型檢查E literal E.type = char E numE.type = integer E id E.type = lookup(id.entry)E E1 mod E2E.type = if (E1.type = integer) and (E2.type = integer) then in

8、teger else type_error E E1 E2 E.type = if (E2.type = integer) and (E1.type = array(s,t) then t else type_error E E1E.type = if (E1.type = pointer(t)then t else type_error m可添加其他類型和運算6.2.3 語句的類型檢查m賦值、條件、whilem無錯誤，void；錯誤，type_errorS id := ES.type = if (lookup(id.entry)=E.type) then void else type_err

9、or S if E then S1S.type = if (E.type = boolean) then S1.type else type_error S while E do S1S.type = if (E.type = boolean) then S1.type else type_error S S1 ; S2S.type = if (S1.type = void) and (S2.type = void) then void else type_error 6.2.4 函數(shù)的類型檢查m函數(shù)定義T T1 T2 T.type = T1.typeT2.type m函數(shù)調(diào)用E E1(E2)

10、 E.type = if (E2.type=s)and (E1.type=st)then t else type_error m多參數(shù)：T1, , TnT1Tnm更復(fù)雜例子：root: (realreal)realrealfunction root(function f(real): real; x: real): real6.3 類型表達(dá)式的等價m兩個類型表達(dá)式等價的精確定義？m用類型表示方式可快速確定等價性m結(jié)構(gòu)等價和名字等價m類型表達(dá)式的圖表示不同葉結(jié)點為基本類型或類型名m遞歸定義類型會導(dǎo)致回路6.3.1 類型表達(dá)式的結(jié)構(gòu)等價m結(jié)構(gòu)等價（structural equivalence）q相

11、同的基本類型q對子表達(dá)式施加的類型構(gòu)造符相同q兩個類型表達(dá)式結(jié)構(gòu)等價dag中對應(yīng)相同結(jié)點m有時要放松條件數(shù)組參數(shù)忽略界限1.等價性檢查算法稍做修改等價性檢查算法bool sequiv(s, t)if (s和t為相同基本類型)return true;else if (s = array(s1, s2) and t = array(t1, t2)return sequiv(s1, t1) and sequiv(s2, t2);else if (s = s1s2 and t = t1t2)return sequiv(s1, t1) and sequiv(s2, t2);else if (s = po

12、inter(s1) and t = pointer(t1)return sequiv(s1, t1);else if (s = s1s2 and t = t1t2)return sequiv(s1, t1) and sequiv(s2, t2);else return false; 例6.1：編碼類型表達(dá)式m用二進(jìn)制碼表示類型和構(gòu)造符m節(jié)省內(nèi)存，加速檢測二進(jìn)制碼不同的類型表達(dá)式肯定不等價mD. M. Ritchie，C編譯器m忽略數(shù)組界限和函數(shù)參數(shù)charfreturns(char)pointer(freturns(char)array(pointer(freturns(char)例6.1（續(xù)

13、）m構(gòu)造符的編碼pointer01array10freturns11m基本類型編碼boolean0000char0001integer0010real0011例6.1（續(xù)）m編碼方法q最右端四位二進(jìn)制位表示基本類型q它前面兩位表示第一個構(gòu)造符q再前面兩位表示第二個構(gòu)造符類型表達(dá)式編碼char000000 0001freturns(char)000011 0001pointer(freturns(char)000111 0001array(pointer(freturns(char)100111 0001例6.1（續(xù)）m加速等價性檢查q不同二進(jìn)制串不可能表示相同類型q不同類型可能表示為相同二進(jìn)制

14、串?dāng)?shù)組界限、函數(shù)參數(shù)m記錄的編碼q在類型表達(dá)式中記錄作為基本類型q用另一個二進(jìn)制串編碼它的域6.3.2 名字等價type link = cell;var next : link; last : link; p : cell; q, r : cell; m5個變量類型是否都相同？依賴實現(xiàn)m允許類型表達(dá)式命名，但不允許回路m名字等價：完全相同m結(jié)構(gòu)等價：名字被替換后完全相同例6.2變量類型表達(dá)式nextlinklastlinkppointer(cell)qpointer(cell)rpointer(cell)m名字等價：next, last類型相同，p, q, r類型相同，p, next類型不同m

15、結(jié)構(gòu)等價：5個變量類型都相同例6.3m許多Pascal編譯器會隱含地為每條標(biāo)識符定義語句涉及到的類型關(guān)聯(lián)一個類型名type link = cell; np = cell; nqr = cell;var next : link; last : link; p : np; q, r : nqr;m名字等價：next, last類型相同，q, r類型相同，p, next, q類型不同例6.3（續(xù)）m實現(xiàn)方式構(gòu)造類型圖q對基本類型和類型構(gòu)造符創(chuàng)建新結(jié)點q對新類型名創(chuàng)建葉結(jié)點，保存與類型表達(dá)式的鏈接m名字等價相同結(jié)點6.3.3 回路問題m鏈表、樹：遞歸定義m實現(xiàn)：記錄數(shù)據(jù)、指向同一記錄類型的指針回路ty

16、pe link = cell; cell = recordinfo : integer;next : link; end;回路問題（續(xù)）m將遞歸定義的類型名替換為類型表達(dá)式，類型圖中會產(chǎn)生回路例6.4 C語言避免回路m對除記錄之外的類型使用結(jié)構(gòu)等價struct cell int info;struct cell *next;mC語言要求類型名在使用前聲明m例外：未定義記錄類型的指針m回路：只可能是記錄指針引起m結(jié)構(gòu)等價判定遇到記錄類型停止：只有名字相同的記錄才認(rèn)為類型相同6.4 類型轉(zhuǎn)換mx+i，x為實型，i為整型q不同保存格式，不同加法指令q轉(zhuǎn)換為相同類型進(jìn)行運算m語言定義指定轉(zhuǎn)換方法q賦值

17、：轉(zhuǎn)換為左部類型q表達(dá)式：intrealq類型檢查器完成轉(zhuǎn)換操作的生成qx i inttoreal real+m類型轉(zhuǎn)換與重載緊密相連強(qiáng)制類型轉(zhuǎn)換（coercion）m編譯器自動進(jìn)行的隱含的類型轉(zhuǎn)換m一般要求：不能丟失信息m顯式（explicit）類型轉(zhuǎn)換：程序員qC：(float)10qPascal：ord(a)字符型整型 chr(65)整型字符型m常量類型轉(zhuǎn)換編譯時進(jìn)行，提高性能qfor I := 1 to N do XI := 148.4N msqfor I := 1 to N do XI := 1.05.4N ms例6.5E num E.type = integer E num.num

18、E.type = real E id E.type = lookup(id.entry)E E1 op E2E.type = if (E1.type = integer) and (E2.type = integer) then integer else if (E1.type = integer) and (E2.type = real) then realelse if (E1.type = real) and (E2.type = integer) then realelse if (E1.type = real) and (E2.type = real) then realelse t

19、ype_errorlcc的類型typedef struct type *Type;struct type int op;Type type;int align;int size;union Symbol sym;struct unsigned oldstyle:1;Type *proto; f; u;Xtype x;類型構(gòu)造符（基本類型）子類型表達(dá)式（用鏈表保存類型表達(dá)式）類型構(gòu)造static Type type(int op, Type ty, int size, int align, void *sym) unsigned h = (op(unsigned long)ty3)&(NELEM

20、S(typetable)-1);struct entry *tn;if (op != FUNCTION & (op != ARRAY | size 0)for (tn = typetableh; tn; tn = tn-link)if (tn-type.op = op & tn-type.type = ty& tn-type.size = size & tn-type.align = align& tn-type.u.sym = sym)return &tn-type;函數(shù)類型和不完全數(shù)組類型無重復(fù)概念，總是創(chuàng)建新類型重復(fù)類型檢查類型構(gòu)造NEW0(tn, PERM);tn-type.op =

21、op;tn-type.type = ty;tn-type.size = size;tn-type.align = align;tn-type.u.sym = sym;tn-link = typetableh;typetableh = tn;return &tn-type;指針Type ptr(Type ty) return type(POINTER, ty, IR-ptrmetric.size,IR-ptrmetric.align, pointersym);Type deref(Type ty) if (isptr(ty)ty = ty-type;elseerror(type error: %

22、sn, pointer expected);return isenum(ty) ? unqual(ty)-type : ty;脫掉指針數(shù)組Type array(Type ty, int n, int a) assert(ty);if (isfunc(ty) error(illegal type array of %tn, ty);return array(inttype, n, 0);if (isarray(ty) & ty-size = 0)error(missing array sizen);if (ty-size = 0) if (unqual(ty) = voidtype)error(

23、illegal type array of %tn, ty);else if (Aflag = 2)warning(declaring type array of %t is undefinedn, ty);不允許函數(shù)數(shù)組數(shù)組的數(shù)組，低維必須大小已知數(shù)組 else if (n INT_MAX/ty-size) error(size of array of %t exceeds %d bytesn,ty, INT_MAX);n = 1;return type(ARRAY, ty, n*ty-size,a ? a : ty-align, NULL);結(jié)構(gòu)和聯(lián)合Type newstruct(int

24、op, char *tag) Symbol p;assert(tag);if (*tag = 0)tag = stringd(genlabel(1);elseif (p = lookup(tag, types) != NULL & (p-scope = level| p-scope = PARAM & level = PARAM+1) if (p-type-op = op & !p-defined)return p-type;error(redefinition of %s previously defined at %wn,p-name, &p-src);創(chuàng)建一個結(jié)構(gòu)類型，但只是一個空架子結(jié)

25、構(gòu)和聯(lián)合p = install(tag, &types, level, PERM);p-type = type(op, NULL, 0, 0, p);if (p-scope maxlevel)maxlevel = p-scope;p-src = src;return p-type;結(jié)構(gòu)和聯(lián)合Field newfield(char *name, Type ty, Type fty) Field p, *q = &ty-u.sym-u.s.flist;if (name = NULL)name = stringd(genlabel(1);for (p = *q; p; q = &p-link, p

26、= *q)if (p-name = name)error(duplicate field name %s in %tn,name, ty);NEW0(p, PERM);*q = p;p-name = name;p-type = fty;結(jié)構(gòu)和聯(lián)合if (xref) /* omit */if (ty-u.sym-u.s.ftab = NULL)/* omit */ ty-u.sym-u.s.ftab = table(NULL, level);/* omit */install(name, &ty-u.sym-u.s.ftab, 0, PERM)-src = src;/* omit */* omi

27、t */return p;結(jié)構(gòu)和聯(lián)合static Type structdcl(int op) ty = newstruct(op, tag);fields(ty);static void fields(Type ty) p = newfield(id, ty, fty);類型等價int eqtype(Type ty1, Type ty2, int ret) if (ty1 = ty2)return 1;if (ty1-op != ty2-op)return 0;switch (ty1-op) case ENUM: case UNION: case STRUCT:case UNSIGNED:

28、case INT: case FLOAT:return 0;case POINTER: return eqtype(ty1-type, ty2-type, 1);case VOLATILE: case CONST+VOLATILE:case CONST: return eqtype(ty1-type, ty2-type, 1);類型等價case ARRAY: if (eqtype(ty1-type, ty2-type, 1) if (ty1-size = ty2-size) return 1; if (ty1-size = 0 | ty2-size = 0) return ret; retur

29、n 0;類型等價case FUNCTION: if (eqtype(ty1-type, ty2-type, 1) Type *p1 = to, *p2 = to; if (p1 = p2) return 1; if (p1 & p2) for ( ; *p1 & *p2; p1+, p2+)if (eqtype(unqual(*p1), unqual(*p2), 1) = 0)return 0;if (*p1 = NULL & *p2 = NULL)return 1;類型等價 else if (variadic(p1 ? ty1 : ty2)retu

30、rn 0;if (p1 = NULL)p1 = p2;for ( ; *p1; p1+) Type ty = unqual(*p1);if (promote(ty) != (isenum(ty) ? ty-type : ty)return 0;return 1; return 0;assert(0); return 0;TinyC的類型檢查void typeCheck(TreeNode * syntaxTree) traverse(syntaxTree,nullProc,checkNode);static void traverse( TreeNode * t, void (* preProc

31、) (TreeNode *), void (* postProc) (TreeNode *) ) if (t != NULL) preProc(t); int i; for (i=0; i childi,preProc,postProc); postProc(t); traverse(t-sibling,preProc,postProc); TinyC的類型檢查static void checkNode(TreeNode * t) switch (t-nodekind) case ExpK: switch (t-kind.exp) case OpK: if (t-child0-type !=

32、Integer) | (t-child1-type != Integer) typeError(t,Op applied to non-integer); if (t-attr.op = EQ) | (t-attr.op = LT) t-type = Boolean; else t-type = Integer; break; case ConstK: case IdK: t-type = Integer; break;TinyC的類型檢查 default: break; break; case StmtK: switch (t-kind.stmt) case IfK: if (t-child

33、0-type = Integer) typeError(t-child0,if test is not Boolean); break; case AssignK: if (t-child0-type != Integer) typeError(t-child0,assignment of non-integer value); break;TinyC的類型檢查 case WriteK: if (t-child0-type != Integer) typeError(t-child0,write of non-integer value); break; case RepeatK: if (t

34、-child1-type = Integer) typeError(t-child1,repeat test is not Boolean); break; default: break; break; default: break; 6.5 函數(shù)和操作符重載m重載（overloaded）符號：根據(jù)上下文，具有不同的意義q+：整型加法，浮點型加法qA(I)：數(shù)組A的第I個元素，以參數(shù)I調(diào)用A，將I轉(zhuǎn)換為類型A的顯式類型轉(zhuǎn)換m重載的解析（resolved）：在某個特定上下文，確定符號的唯一意義q1+2：+為整型加法q運算符識別，operator identification6.5.1 子表達(dá)式可

35、能類型集合m例6.6mAda允許對乘法運算符“*”進(jìn)行重載qfunction “*” (i, j : integer) return complex;qfunction “*” (x, y : complex) return complex;m*具有三種可能類型qinteger integer integerqinteger integer complexqcomplex complex complexq2*(3*5)3*5類型1qz*(3*5)，z為復(fù)數(shù)類型3*5類型2可能類型集合情況的處理E id E.types = lookup(id.entry)E E1(E2) E.types = t

36、 | E2.types中 存在s使得st屬于 E1.types m單一類型運算類型集合運算例 確定唯一類型m完整表達(dá)式須有唯一類型確定每個子表達(dá)式的唯一類型，或type_errorm自頂向下mE.types中每個類型t均為可行（feasible）類型確定E中重載標(biāo)識符的類型，某種情況下，E的類型為tq對標(biāo)識符成立，id.types中類型均可行q歸納法：E為E1(E2)，s為E2可行類型，st為E1可行類型，因此t為E可行類型確定唯一類型的語義規(guī)則E EE.types = E.typesE.unique = if E.types=t then t else type_errorE

37、.code = E.codeE id E.types = lookup(id.entry)E.code = gen(id.lexeme : E.unique)E E1(E2) E.types = s | E2.types中存在s使得ss屬于E1.types t = E.uniqueS = s | sE2.types and stE1.types E2.unique = if S = s then s else type_errorE1.unique = if S = s then s t else type_errorE.code = E1.code | E2.code | gen(apply

38、 : E.unique)6.6 多態(tài)（polymorphic）函數(shù)m普通函數(shù)：參數(shù)類型固定m多態(tài)函數(shù)：不同調(diào)用參數(shù)可為不同類型m某些內(nèi)置操作符多態(tài)操作符q數(shù)組索引符，函數(shù)調(diào)用符()，指針操作符&q&：“若操作對象類型為，則操作結(jié)果的類型為指向的指針6.6.1 為什么使用多態(tài)函數(shù)？m實現(xiàn)算法處理數(shù)據(jù)結(jié)構(gòu)，而不必管其內(nèi)部元素的類型type link = cell; cell = recordinfo : integer;next : link end;function length(lptr : link) : integer;var len : integer;beginlen := 0;whi

39、le lptr nil do beginlen := len + 1;lptr := lptr.next;end;length := lenend;求任何類型列表長度的ML程序fun length(lptr) =if null(lptr) then 0else length(tl(lptr) + 1;m可應(yīng)用于任何類型的列表qlength(“sun”, “mon”, “tue”);qlength(10, 9, 8);遞歸函數(shù)遞歸函數(shù)列表為空？列表為空？列表剩余部分列表剩余部分6.6.2 類型變量ma, b, ，表示未知類型m重要應(yīng)用：不要求標(biāo)識符先聲明后使用的語言中，檢查標(biāo)識符使用的一致性m類

40、型變量表示未聲明標(biāo)識符的類型q若類型變量發(fā)生變化，不一致！q若一直未變化，一致！同時得到標(biāo)識符類型m類型推斷，type inferenceq根據(jù)語言結(jié)構(gòu)的使用方式判定其類型例6.8type link = cell;procedure mlist(lptr : link; procedure p);beginwhile lptr nil do beginp(lptr);lptr := lptr.nextendend;mp：參數(shù)情況未知，不完整的過程類型m由p(lptr)qp參數(shù)為link類型，p的類型為linkvoidq其他使用方式均會導(dǎo)致type_error例6.9function deref

41、(p);beginreturn p;end;m掃描第一行，p的類型未知，用b表示m第三行，應(yīng)作用于指針，因此p為某未知基本類型a的指針類型，b=pointer(a)m因此函數(shù)deref類型為：pointer(a)a6.6.3 包含多態(tài)函數(shù)的語言m用 表示“對所有類型”mderef類型的精確描述：mlength：qlist(integer)integerqlist(list(char)integerm ：全稱量詞（universal quantifier）它所施用的類型變量稱為由它約束（bound）aaa)(.pointerintegerlist)(.aa文法定義P D ; ED D ; D |

42、 id : QQ type_varible . Q | TT T T | T T | unary_constructor ( T ) | basic_type | type_varible | ( T )E E (E) | E , E | id程序例：deref : q : pointer(pointer(integer);deref(deref(q);)(.aaapointer多態(tài)函數(shù)類型檢查m每個結(jié)點兩個標(biāo)簽：子表達(dá)式和類型表達(dá)式m下標(biāo)o：外層deref，i：內(nèi)存deref類型檢查規(guī)則的特點m不同位置出現(xiàn)的同一多態(tài)函數(shù)可具有不同類型的參數(shù)。mderefo參數(shù)為二重指針，而derefi的參數(shù)

43、為一重指針。m關(guān)鍵在于 的解釋，對不同deref，約束的類型變量a所代表的意義是不同的。m對多態(tài)函數(shù)的每次出現(xiàn)，都賦予不同的類型變量，而不再使用 上例中用ao、ai分別對應(yīng)外層和內(nèi)層deref類型檢查規(guī)則的特點（二）m類型表達(dá)式中存在變量，因此要重新考慮類型等價的概念m類型為ss的函數(shù)E1施用于類型為t的E2，僅判定s和t是否等價是不夠的，要對它們進(jìn)行“一致化”（unify）m適當(dāng)替換類型變量，檢查是否有可能達(dá)到結(jié)構(gòu)等價m上例：將ai替換為pointer(integer)，則pointer(ai)與pointer(pointer( integer)等價類型檢查規(guī)則的特點（三）m需要某種機(jī)制記錄

44、一致化的影響m一個類型變量可出現(xiàn)在表達(dá)式的多個位置m若s和s的一致化使得變量a表示類型t，則在整個類型表達(dá)式中，它都應(yīng)表示tm上例： ai作用域為derefi(q)，因此可用來一致化derefi和qm而ao為不同類型變量，因此表示不同類型不違反本規(guī)則6.6.4 代換，實例和合一m變量表示實際類型的形式化定義q類型變量類型表達(dá)式的映射，稱為替換，substitutionsubst(t : type_expression) : type_expression/利用代換（映射）S將類型表達(dá)式t中變量代換if (t為基本類型) return t;else if (t為類型變量) return S(t)

45、;else if (t為t1t2) return subst(t1)subst(t2);mS(t)表示代換t的類型表達(dá)式，稱為t的實例，instancem若無法代換，S(a)=a，恒等映射例6.10mst表示s是t的一個實例qpointer(integer) pointer(a)qpointer(real) pointer(a)qinteger integer a aqpointer(a) bqa bm不是實例的情況qintegerrealqinteger reala aqinteger aa a合一方法m類型表達(dá)式t1和t2能合一的條件存在代換S，S(t1) = S(t2)m最一般的合一代換

46、，most general unifier最少變量約束的代換q類型表達(dá)式t1和t2的最一般的合一代換是一個代換S，它滿足以下條件qS(t1) = S(t2)1.對任何其他代換S，S(t1) = S(t2)，S是S的一個實例，即，對任意t，S(t)是S(t)的一個實例6.6.5 多態(tài)函數(shù)類型檢查m檢查規(guī)則由下列對類型圖的操作構(gòu)成qfresh(t)將類型表達(dá)式t中約束變量代換為新變量，返回代換后類型表達(dá)式結(jié)點指針消除qunify(m, n)將結(jié)點m、n表示的類型表達(dá)式合一，會修改、保存對應(yīng)的代換。若失敗，則整個類型檢查過程失敗m圖的創(chuàng)建仍可用mkleaf、mknode完成m每個類型變量創(chuàng)建不同結(jié)點

47、unify操作m合一、代換基于圖論的方法mm、n為類型圖結(jié)點，分別表示表達(dá)式e、f，若S(e)=S(f)，稱m、n在代換S下等價m求最一般的合一代換q轉(zhuǎn)化為在S下必須等價的結(jié)點的集合劃分問題q類型表達(dá)式等價根必須等價qm、n等價表示相同操作且孩子結(jié)點等價類型檢查規(guī)則E E1(E2) p = mkleaf(newtypevar);unify(E1.type, mknode(, E2.type, p);E.type = p; E E1 , E2 E.type = mknode(, E1.type, E2.type); E id E.type = fresh(id.type); mE1.type=a

48、，E2.type=b，都是類型變量m前者是函數(shù)，尋求兩者等價，必有類型變量g，使得a=bg例表達(dá)式類型代換qpointer(pointer(integer)derefipointer(ai) aiderefi(q)pointer(integer) ai=pointer(integer)derefopointer(ao) aoderefo(derefi(q)integer ao=integer例6.11例6.11（續(xù)）mderefi的合一過程例6.12 ML語言多態(tài)函數(shù)檢查fun id0 ( id1, , idk ) = E;mid0：函數(shù)名， id1, , idk：參數(shù)，E遵從前面定義的用于多

49、態(tài)函數(shù)類型檢查的文法，其中的標(biāo)識符只可能是函數(shù)名、參數(shù)或內(nèi)置函數(shù)m方法：例6.9方法的形式化q為函數(shù)名和參數(shù)創(chuàng)建新類型變量q多態(tài)函數(shù)的類型變量由 約束q檢查id0 ( id1, , idk )和E類型是否匹配q若成功，則推斷出函數(shù)類型例6.12（續(xù)）fun length(lptr) =if null(lptr) then 0else length(tl(lptr) + 1;m類型變量：lengthb，lptrgm為匹配函數(shù)體：b=m按多態(tài)函數(shù)類型檢查語言重寫程序length : b;lptr : g;if : integerlist)(.aa;.aaaaboolean例6.12（續(xù)）null

50、: tl : 0 : integer;1 : integer;+ :match :match (length(lptr),if ( null(lptr), 0, length(tl(lptr) + 1) ;)(.booleanlistaa);()(.aaalistlist;integerintegerinteger;.aaaa檢查length(lptr)與函數(shù)體匹配例6.12（續(xù)）表達(dá)式：lptr :length :length(lptr) :lptr :null :null(lptr) :0 :lptr :tl :tl(lptr) :類型gbdglist(an)booleanbooleani

51、ntegerlist(an)list(at)list(at)list(an)替換b=gdg=list(an)at=anlength參數(shù)為參數(shù)為lptrg g返回類型為返回類型為d dnull參數(shù)類型為參數(shù)類型為list(a an)lptr類型類型g g=list(a an) length類型為類型為list(a an)d d例6.12（續(xù)）表達(dá)式：length :length(tl(lptr) :1 :+ :length(tl(lptr) + 1:if :if () :match :match() :類型list(an)ddintegerintegerinteger integerintege

52、rbooleanaiaiaiintegeramam aminteger替換d=integerai=integeram=integerlength的返的返回類型，因回類型，因此此d d=integera an最終未被替代，最終未被替代，length類型為類型為integerlistnn )(.a aa a6.7 合一算法m合一：類型表達(dá)式e、f通過變量代換，是否可達(dá)到類型等價q特殊情況：等價性檢查，無變量q本節(jié)算法適用類型圖有回路情況q算法尋找最一般的合一代換S例6.13me、f：m兩個合一代換S, S：xS(x)S(x)a1 a3 a1a2 a2 a1a3 a3 a1a4 a2 a1a5list(a2) list(a1)m代換結(jié)果：53432321)()()()()(aaaaaaaalistlistlist)()()()( )( )()()()()(11112323aaaaaaaalistlistfSeSlistlistfSeS=最一般的合一代換最一般的合一代換S(e)是是S