第9章類型推斷(編輯修改稿)
2024-11-03 15:36 本頁面
【文章內(nèi)容簡介】 用到類型表達式 ? S?是把 ?中的每個變量 t用 S (t)代替 – 類型代換 S作用到類型指派 ? S ? = {x: S? | x: ? ? ?} – 類型代換 S作用到 ?t?項 結(jié)果 S M同 M的區(qū)別僅在 ?約束變元的類型 帶類型變量的 ??類型推斷 ? 實例 定型斷言 ?? M?:??是 ? M:?的 實例 ， 如果存在類型代 換 S使得 ?? ? S ?, M? = S M并且 ?? = S? ? 引理 如果定型斷言 ? M:?是可推導的 ， 那么它的每個實例 S ? ??? SM:S?也是可推導的 帶類型變量的 ??類型推斷 合一算法 ? 合一 如果 E是一個類型表達式之間的等式集合 ， 如果對每 個等式 ? = ? ?E都有 S? ? S?， 那么類型代換 S合一 E ? 例 E = {s = t ? v, t = v ? w} S = {?t, v ? w?, ?s, (v ? w) ? v?} 代換結(jié)果 {(v ? w) ? v = (v ? w) ? v, v ? w = v ? w} S合一 E 帶類型變量的 ??類型推斷 ? 最一般的合一代換 – 如果存在某個代換 T使得 R = T?S， 那么 S比 R更一般 – 如果不存在比 S更一般的代換 ， 則稱 S是最一般的合一代換 – 最一般代換是使 E的每個等式的代換結(jié)果在語法上為真的最簡單的方式 帶類型變量的 ??類型推斷 ? 例 E = {s = t ? v, t = v ? w} 最一般的合一代換 S = {?t, v ? w?, ?s, (v ? w) ? v?} 代換結(jié)果 {(v ? w) ? v = (v ? w) ? v, v ? w = v ? w} 另一個合一代換 S? = {?t, (w ? w) ? w?, ?s, ((w ? w) ? w) ? (w ? w)?, ?v, w ? w?} 代換結(jié)果 {((w ? w) ? w)?(w ? w)=(w ? w) ? w??(w ? w), (w ? w) ? w? = (w ? w) ? w} 帶類型變量的 ??類型推斷 ? 引理 令 E是類型表達式之間的任意等式集合 。存在一個算法 Unify， 使得如果 E是可合一的 ，那么 Unify(E)計算得出一個最一般的合一代換 .如果 E不可合一 ， 那么 Unify(E)失敗 ? 如果 ?和 ??都是類型指派 ， 那么合一可以用來找出最一般的代換 S， 使得 S ? ?S ??都是合式的 。 – 直接合一所有等式 ? = ?的集合就可以了 ， 其中 x:? ? ?并且 x:? ? ?? 帶類型變量的 ??類型推斷 ? 遞歸算法 Unify 1. Unify(?) = ? 2. Unify(E ? {b1 = b2}) = if b1 ? b2 then f
教學課件相關(guān)推薦
鄂ICP備17016276號-1