第9章類(lèi)型推斷-資料下載頁(yè)
2025-09-19 15:36本頁(yè)面
【導(dǎo)讀】類(lèi)型推斷是把無(wú)類(lèi)型的或“部分類(lèi)型化的”項(xiàng)。它通過(guò)推導(dǎo)未給出的類(lèi)型信息來(lái)完成這個(gè)變換。類(lèi)型推斷兼有兩方面的優(yōu)點(diǎn)。加了類(lèi)型變量后的??約束變量的類(lèi)型、類(lèi)型抽象和類(lèi)型作。是一種相對(duì)應(yīng)的“無(wú)類(lèi)型”語(yǔ)言，或者是部分類(lèi)。程序的語(yǔ)法由文法。語(yǔ)言L和擦除函數(shù)Erase:L?一般來(lái)說(shuō)，可能有無(wú)數(shù)多的方式用來(lái)將類(lèi)型信。的定型判定問(wèn)題叫做類(lèi)型推斷。的定型公理和推理規(guī)則同??類(lèi)型項(xiàng)上的同樣歸約有Erase??事實(shí)一個(gè)無(wú)類(lèi)型項(xiàng)U，只有不存在從它開(kāi)始。中的每個(gè)變量t用S代替。結(jié)果SM同M的區(qū)別僅在?S，那么S比R更一。引理令E是類(lèi)型表達(dá)式之間的任意等式集合。存在一個(gè)算法Unify，使得如果E是可合一的，那么Unify計(jì)算得出一個(gè)最一般的合一代換.找出最一般的代換S，使得S??
【正文】 s ? t}) in {x : Sr} ? {x : Ss} xx:St 帶類(lèi)型變量的 ??類(lèi)型推斷 ? 定理 如果 PT (U) = ? M:?， 那么 Erase (M) = U， 并且 ? M:?的每個(gè)實(shí)例是可證明的 ? 定理 如果 ? M:?是可證明的定型斷言 ， 并且Erase (M) = U， 那么 PT (U)一定成功 ， 并產(chǎn)生一個(gè)定型斷言 ， 使得 ? M:?是它的一個(gè)實(shí)例 帶類(lèi)型變量的 ??類(lèi)型推斷 隱式定型 – 歷史上 ， 許多類(lèi)型推斷問(wèn)題都被公式化為對(duì)無(wú)類(lèi)型項(xiàng)使用證明規(guī)則進(jìn)行證明的問(wèn)題 – 這些證明系統(tǒng)通常稱為 隱式定型 系統(tǒng) ， 因?yàn)橐粋€(gè)項(xiàng)的類(lèi)型不是由項(xiàng)的語(yǔ)法顯式地給定的 – 此時(shí) ， 類(lèi)型推斷本質(zhì)上是一個(gè)公理理論的判定問(wèn)題 帶類(lèi)型變量的 ??類(lèi)型推斷 ? 隱式定型證明 系統(tǒng) ? c:? c是類(lèi)型 ?的常量 ， ?中無(wú)類(lèi)型變量 (cst) x:? x:? (var) (abs) (app) (add var) ?, x : ? U : ? ? (?) : ? ?? ? U : ? ?? ? V: ? ? UV : ? ? U : ? ?, x : ? U : ? x不在 ?中 帶類(lèi)型變量的 ??類(lèi)型推斷 ? 引理 如果 ? M:?是良類(lèi)型的項(xiàng) ， 那么 |C ? Erase(M) ??. 反過(guò)來(lái) , 如果 |C ? U ??， 那么存在類(lèi)型化的項(xiàng) ? M:?， 使得 Erase(M)=U 帶類(lèi)型變量的 ??類(lèi)型推斷 定型和合一的等價(jià) ? 類(lèi)型推斷和合一是算法地等價(jià)的 – 每個(gè)類(lèi)型推斷問(wèn)題產(chǎn)生一個(gè)合一問(wèn)題 – 每個(gè)合一問(wèn)題出現(xiàn)在某個(gè)項(xiàng)的類(lèi)型推斷中 帶類(lèi)型變量的 ??類(lèi)型推斷 另一個(gè)類(lèi)型推斷算法 本質(zhì)上是從定型到合一的歸約 TE(c, t) = {t = ?}, 其中 ?是 c的類(lèi)型 ， ?中無(wú)自由變量 TE(x, t) = {t = tx}， 其中 tx 是 x的類(lèi)型變量 TE(U V, t) = TE(U, r) ?TE(V, s) ?{r = s ?t} 其中 r， s都是新的類(lèi)型變量 TE(?, t) = TE(U, s) ?{t = tx ?s} 其中 s是新的類(lèi)型變量 – 如果 U是無(wú)類(lèi)型項(xiàng) ， t是類(lèi)型變量 ， 并且 E = TE(U, t)， 那么 U的每個(gè)定型是 S ?U U: St的一個(gè)實(shí)例 （對(duì)某個(gè)使 E能夠合一的 最一般合一代換 S） 習(xí) 題 第一次：
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1