【導(dǎo)讀】類型系統(tǒng)、類型檢查、多態(tài)函數(shù)、重載。檢查、關(guān)聯(lián)名字檢查。只能是布爾值，not總有意義。類型系統(tǒng)的根本目的是防止程序運(yùn)行時(shí)出現(xiàn)執(zhí)行錯(cuò)。顯式類型化的語(yǔ)言。不會(huì)被捕獲的錯(cuò)誤。類型化語(yǔ)言的目標(biāo)是在排除禁止錯(cuò)誤

　　

【正文】 y(s1, s2) and t = array(t1, t2) then return sequiv(s1, t1) and sequiv(s2, t2) else if s = s1 ? s2 and t = t1? t2 then return sequiv(s1, t1) and sequiv(s2, t2) else if s = pointer (s1) and t = pointer(t1) then return sequiv(s1, t1) else if s = s1 ? s2 and t = t1 ? t2 then return squiv(s1, t1) and sequiv(s2, t2) else return false 類型表達(dá)式的等價(jià) 類型表達(dá)式的名字等價(jià) ? 把每個(gè)類型名看成是一個(gè)可區(qū)別的類型 type link = ?cell。 var next : link。 last : link。 p : ?cell。 q, r : ?cell。 類型表達(dá)式的等價(jià) 類型表達(dá)式的名字等價(jià) ? 把每個(gè)類型名看成是一個(gè)可區(qū)別的類型 ? 兩個(gè)類型表達(dá)式名字等價(jià)當(dāng)且僅當(dāng)這兩個(gè)類型表達(dá)式不做名字代換就結(jié)構(gòu)等價(jià) type link = ?cell。 var next : link。 last : link。 p : ?cell。 q, r : ?cell。 類型表達(dá)式的等價(jià) Pascal的許多實(shí)現(xiàn)用隱含的類型名和每個(gè)聲明的標(biāo)識(shí)符聯(lián)系起來(lái) type link = ?cell。 type link = ?cell。 var next : link。 np = ?cell。 last : link。 nqr = ?cell。 p : ?cell。 var next : link。 q, r : ?cell。 last : link。 p : np。 q : nqr。 r : nqr。 類型表達(dá)式的等價(jià) 注意 : 類型名字的引入只是類型表達(dá)式的一個(gè)語(yǔ)法約定問(wèn)題，它并不像引入類型構(gòu)造器或類型變量那樣能豐富我們所能表達(dá)的類型。 類型表達(dá)式的等價(jià) 記錄類型 (Type Record) (li是有區(qū)別的 ) ? |? T1,… ,? |? Tn ?? |? record(l1:T1,… ,ln:Tn) (Val Record) (li是有區(qū)別的 ) ? |? M1:T1,… , ? |? Mn: Tn ? ? |? record (l1=M1, … , ln=Mn) : record (l1:T1, … , ln:Tn) (Val Record Select) ? |? M : record(l1:T1, … , ln:Tn) ? ? |? : Tj (j? 1..n) 類型表達(dá)式的等價(jià) 類型表示中的環(huán) type link = ? cell 。 cell = record info : integer 。 next : link end。 cell = record ? : : info pointer next integer cell 類型表達(dá)式的等價(jià) 類型表示中的環(huán) type link = ? cell 。 cell = record info : integer 。 next : link end。 cell = record ? : : info pointer next integer 類型表達(dá)式的等價(jià) C語(yǔ)言對(duì)除記錄（結(jié)構(gòu)）以外的所有類型使用結(jié)構(gòu)等價(jià)，而記錄類型用的是名字等價(jià)，以避免類型圖中的環(huán)。 cell = record ? : : info pointer next integer cell 函數(shù)和算符的重載 重載符號(hào) 有多個(gè)含義，但在引用點(diǎn) 的含義都是唯一的 例如 加法算符 +可用于不同類型，是不同的函數(shù) 在 Ada中， ( ) 是重載的， A( I ) 有不同含義 函數(shù)和算符的重載 重載符號(hào) 有多個(gè)含義，但在引用點(diǎn) 的含義都是唯一的 例如 加法算符 +可用于不同類型，是不同的函數(shù) 在 Ada中， ( ) 是重載的， A( I ) 有不同含義 重載的消除 在重載符號(hào)的引用點(diǎn)，其含義能確定到唯一 函數(shù)和算符的重載 子表達(dá)式的可能類型集合 例 Ada語(yǔ)言 聲明： function ―? ‖ (i, j : integer ) return plex。 function ―? ‖ (x, y : plex ) return plex。 函數(shù)和算符的重載 子表達(dá)式的可能類型集合 例 Ada語(yǔ)言 聲明： function ―? ‖ (i, j : integer ) return plex。 function ―? ‖ (x, y : plex ) return plex。 使得算符 ?重載， 可能的類型包括： integer ? integer ? integer integer ? integer ? plex plex ? plex ? plex 函數(shù)和算符的重載 子表達(dá)式的可能類型集合 例 Ada語(yǔ)言 聲明： function ―? ‖ (i, j : integer ) return plex。 function ―? ‖ (x, y : plex ) return plex。 使得算符 ?重載， 可能的類型包括： integer ? integer ? integer 2 ? (3 ? 5) integer ? integer ? plex plex ? plex ? plex 函數(shù)和算符的重載 子表達(dá)式的可能類型集合 例 Ada語(yǔ)言 聲明： function ―? ‖ (i, j : integer ) return plex。 function ―? ‖ (x, y : plex ) return plex。 使得算符 ?重載， 可能的類型包括： integer ? integer ? integer 2 ? (3 ? 5) integer ? integer ? plex (3 ? 5) ? z plex ? plex ? plex z是復(fù)型 函數(shù)和算符的重載 以 函數(shù)作用為例，考慮類型檢查 在每個(gè)表達(dá)式都有唯一的類型 時(shí)，函數(shù)作用 的類型檢查是： E?E1 (E2 ) {E. type := if E2. type = s and E1. type = s ? t then t else type_ error } 函數(shù)和算符的重載 確定表達(dá)式可能類型的集合 產(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ù)和算符的重載 例：表達(dá)式 3 ? 5可能的類型集合 E: {i, c} E: {i} 3: {i} E: {i} 5: {i} ? : {i ? i ? i, i ? i ? c, c ? c ? c } 函數(shù)和算符的重載 縮小可能類型的集合 產(chǎn) 生 式 語(yǔ) 義 規(guī) 則 E? ? E E?. types := E. types E. unique := if E?. types = { t } then t else type_error E?. code := E ? id E. types := lookup(id. entry) := gen( ?:‘ E. unique) 函數(shù)和算符的重載 E ? E1 (E2) E. types := {s? | E2. types中存在一個(gè)s， 使得 s ? s?屬于 E1. types} t := E. unique S := {s | s ? E2. types and s ? t ? E1. types } E2. unique := if S = { s } then s else type_error E1. unique := if S = { s }then s ? t else type_error := || || gen(?apply‘ ?:‘ E. unique) 函數(shù)和算符的重載 注意 : 重載的函數(shù)和符號(hào)的引入使得程序員可以用一個(gè)名字或符號(hào)表示多個(gè)不同類型的函數(shù)或運(yùn)算，它也不像引入類型構(gòu)造器或類型變量那樣能豐富我們所能表達(dá)的類型。 本 章 要 點(diǎn) ? 靜態(tài)檢查所涉及的內(nèi)容：類型檢查、控制流檢查、唯一性檢查和關(guān)聯(lián)名字檢查等。 ? 類型表達(dá)式、類型系統(tǒng)和類型檢查。 ? 設(shè)計(jì)完成類型檢查的語(yǔ)法制導(dǎo)定義。 ? 代換、實(shí)例和合一。 ? 重載函數(shù)和多態(tài)函數(shù)的區(qū)別。 ? 類型推斷。 例 題 1 C語(yǔ)言 ? 稱 amp。為地址運(yùn)算符， amp。a為變量 a的地址。 ? 數(shù)組名代表數(shù)組的首地址。 問(wèn)題： 如果 a是一個(gè)數(shù)組名，那么表達(dá)式 a和 amp。a的值都是數(shù)組 a的首地址，它們的使用是否有區(qū)別的？ 例 題 1 C語(yǔ)言 ? 稱 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 類型的數(shù)組 a[ i1 ][ i2 ]… [ in ]來(lái)說(shuō) ， 表達(dá)式 a的類型是： pointer(array(0.. i2 –1, … array(0.. in –1, t)… )) 表達(dá)式 amp。a的類型是： pointer(array(0.. i1 –1, … array(0.. in –1, t)… )) 例 題 2 C語(yǔ)言程序引用 sizeof（ 求字節(jié)數(shù)運(yùn)算符 ） 時(shí) ，該運(yùn)算是在編譯該程序時(shí)完成 ， 還是在運(yùn)行該程序時(shí)完成 ？ 說(shuō)明理由 。 習(xí) 題 ? 第一次： , ? 第二次： , ? 第三次：