第9章類型推斷-文庫吧資料
2024-10-06 15:36本頁面
【正文】 數(shù)作用到非多態(tài)變元而沒有中間的類型作用 引 言 ? 語言 L和擦除函數(shù) Erase: L ? L?的類型推斷問題是： 對給定的表達式 U?L?， 找出 L的類型化項 ? M:?， 使得 Erase(M) = U ? 一般來說，可能有無數(shù)多的方式用來將類型信息插入項 – 可以給 ?f.? (f x)以形式為 (? ??) ? ? ??的任何類型 引 言 ? 例 若擦除的結(jié)果是 (?t.?x:) (?t.?x:) – 這 兩個函數(shù)表達式必須作用到某個類型變元 – 原來的項必定有下面的形式 ((?t.?x:)?1) ((?t.?x:)?2) – ?1 和 ?2只要滿足 ?1 ??2??2就可以了 – 原來的項應(yīng)該是 ((?t.?x:) t ? t) ((?t.?x:) t) 引 言 ? 類型推斷的另一種觀點是 – 定型是由一組推理規(guī)則給出 合式公式的語法和證明規(guī)則給出一個邏輯系統(tǒng) – 類型推斷算法正好是一個公理理論的判定過程 決定一個合式公式是否可證明 – 判定過程是回答是或不是，而類型推斷算法必須構(gòu)造類型化的項 引 言 ? 類型推斷和類型檢查 – 類型檢查 看成是用語法制導(dǎo)的方式，根據(jù)上下文有關(guān)的定型條件判定項是否為良類型的項的過程 ? ?x:?.M : ? – 把對帶無類型 ?的定型判定問題叫做 類型推斷 ? ? : ? 帶類型變量的 ??類型推斷 語言 ?t? 考慮語言 ?t?的類型推斷 ? 語言 ?t? – 類型由下面文法 定義 ? ::= b | t | ? ? ? – 項由下面文法 定義 M ::= c | x | ?x: ?.M | M M ? ?t?的定型公理和推理規(guī)則同 ??的相同 – 限制：項常量的類型一定不含類型變量 帶類型變量的 ??類型推斷 ? 命題 令 ? M??是任意的良類型 ?t?項。如果由類型化項上的 ?和 ?歸約有 M?? N， 那么由無類型項上的同樣歸約有 Erase(M) ?? Erase(N)。 M ? M1 ? . . . ? Mk Erase(M) ? Erase(M1) ? . . . ? Erase(Mk) 帶類型變量的 ??類型推斷 ? 事實 一個無類型項 U， 只有不存在從它開始的無類型歸約的無窮序列時，它才可能被類型化 – 推論 1 如果 U不是強范式的，那么就不存在可推導(dǎo)的定型 ? M:?， 使得 Erase(M) = U – 推論 2 如果 U是不可類型化的，那么由的主語歸約性質(zhì)，知道沒有一個能歸約到 U的項是可類型化的 M ? M1
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1