數(shù)據(jù)類型檢查基礎(chǔ)知識(shí)-資料下載頁(yè)
2025-03-08 08:40本頁(yè)面
【正文】 58 June 5, 2023 多態(tài)函數(shù)（ 8） ? 多態(tài)函數(shù)的類型檢查與普通函數(shù)的類型檢查的區(qū)別 ? 同一表達(dá)式中的多態(tài)函數(shù)的不同出現(xiàn)不需要變?cè)邢嗤念愋? ? 類型等價(jià)概念的不同，通過(guò)“合一”判定類型是否等價(jià) 下圖中，如果用 pointer(integer)代替 αi， 則 pointer(αi)和pointer(pointer(integer))結(jié)構(gòu)等價(jià) ? 兩個(gè)子表達(dá)式合一的結(jié)果的記錄 通常，類型變量可以出現(xiàn)在幾個(gè)類型表達(dá)式中，如果 s和 s?的合一使得變量 α代表類型 t， 則在類型檢查的過(guò)程中 α必須繼續(xù)代表 t a p p l y : αoa p p l y : αid e r e f0: p o i n t e r ( αo)→ αod e r e fi: p o i n t e r ( αi)→ αiq: p o i n t e r ( p o i n t e r ( i n t e g e r ))deref(deref(q))的 帶標(biāo)記的語(yǔ)法樹59 June 5, 2023 多態(tài)函數(shù)（ 9） ? 代換、實(shí)例和合一 ? 代換： ? 將類型表達(dá)式中的類型變量用其所代表的類型表達(dá)式去替換 用代換 S去替換表達(dá)式 t中所有類型變量的函數(shù)： function subst( t : type_expression ) : type_expression begin if t 是基本類型 then return t else if t是變量 then return S(t) else if t是 t1→t2 then subst(t1)→subst(t2) end ? 為了方便，用 S(t)表示 subst作用于 t后所得的類型表達(dá)式，這個(gè)結(jié)果 S(t)叫做 t的實(shí)例 60 June 5, 2023 多態(tài)函數(shù)（ 10） ? 如果代換 S對(duì)變量 α沒有指定表達(dá)式，則假定 S(α)是 α，即 S是這種變量的恒等映射 例：用 s t表示 s是 t的實(shí)例 pointer(integer) pointer(α) pointer(real) pointer(α) integer→integer α→α pointer(α) β α β 下面左邊的類型表達(dá)式不是右邊的實(shí)例 integer real (代換不能用于基本類型 ) integer →real α→α (α的代換不一致 ) integer →α α→α (α的所有出現(xiàn)都應(yīng)代換 ) 61 June 5, 2023 多態(tài)函數(shù)（ 11） ? 如果存在某個(gè)代換 S， 使得 S(t1)=S(t2)， 則這兩個(gè)表達(dá)式 t1和 t2能合一 ? 最一般的合一代換：對(duì)表達(dá)式中的變量限制最少的代換，表達(dá)式 t1和 t2最一般的合一代換有如下的性質(zhì) ? S(t1)=S(t2) ? 對(duì)任何其它滿足 S?(t1)=S?(t2)的代換 S?,代換 S?(t1)是 S(t1)的實(shí)例 ? 下面，我們說(shuō)合一是指最一般的合一代換 62 June 5, 2023 多態(tài)函數(shù)（ 12） ? 多態(tài)函數(shù)的檢查和推導(dǎo) ? 過(guò)程 ? 全稱量詞的消除：把類型表達(dá)式 t中的約束變量用新的變量代替， fresh(t) ? 合一操作：基于合一和代換的圖， unify( m ,n ) ? 如果結(jié)點(diǎn) m和 n分別代表類型表達(dá)式 e和 f， 若 S(e)=S(f)，則結(jié)點(diǎn) m和 n在代換 S下等價(jià) ? 兩個(gè)表達(dá)式的等價(jià)： ? 根必須等價(jià) ? 兩個(gè)結(jié)點(diǎn)等價(jià)，當(dāng)且僅當(dāng)它們代表同樣的算符，且其對(duì)應(yīng)的子結(jié)點(diǎn)等價(jià) ? 類型檢查：從葉結(jié)點(diǎn)開始，自下而上進(jìn)行檢查 63 June 5, 2023 多態(tài)函數(shù)（ 14） ? 檢查多態(tài)函數(shù)的翻譯方案： E→E1(E2) { p := mkleaf(newtypevar)。 unify( , mknode(?→?, , p)。 := p } E→E1 , E2 { := mknode( ? ? , , ) } E→id { := fresh( ) } ? 函數(shù)作用 E→E1(E2)的類型檢查：如果 =α 且=β ， 則 α 必須是函數(shù)，并使得某個(gè)未知類型 r滿足α =β →r ? 自下而上確定類型的總結(jié)： 表達(dá)式 ：類型 代換 q ： pointer(pointer(integer)) derefi ： pointer(α i) → α i derefi(q) ： pointer(integer) α i = pointer(integer) derefo ： pointer(α o) → α o derefo(derefi(q)) ： integer α 0 = integer 64 June 5, 2023 多態(tài)函數(shù)（ 15） ? 例：表達(dá)式 derefo(derefi(q))的類型檢查：從葉結(jié)點(diǎn)開始 ? 構(gòu)造分別表示 derefo， derefi和 q的類型圖 ? 函數(shù)作用 derefi(q)由構(gòu)造從類型 q到新類型變量 β 的函數(shù)結(jié)點(diǎn) n來(lái)檢查 ? 注意： α i和 pointer(integer)的結(jié)點(diǎn)都標(biāo)記為 8，即 α i和這個(gè)類型表達(dá)式合一 ? 最終， α o和 integer合一 pointer ： 2→：3α o：1deref 0pointer ： 5→：6α i：4deref iqpointer ： 9pointer ： 8integer ： 7pointer ： 2→：3α o：1p oi nt er ： 5m →： 6α i： 8p o i n t e r ： 5p o i n t e r ： 8i n t e g e r ： 7n →： 6β 1 ： 865 June 5, 2023 多態(tài)函數(shù)（ 16） ? 例： ML函數(shù)類型的類型推導(dǎo)： fun length ( lptr ) = if null( lptr ) then 0 else length( tl( lptr ) ) + 1。 分別引入類型變量 β 和 γ 表示 length和 lptr的類型， length(lptr)的類型和函數(shù)體的類型匹配，所以 length的類型是 類型聲明及要檢查的表達(dá)式 intege rαlist α. ?? )( ) ) 1 ) )lptr tl( leng th( 0, ),lptr null( ( if r),leng th(lpt ( match :match。 :。 :1。 :0 :tl : null :if。 :lptr。 :leng th???????????????α αα α. int egerint egerint eger int eger int eger 。 )li st( αi)li st( αi α. 。 bo olea n)li st( αi α. 。α ααbo olea n α. γ β 66 June 5, 2023 多態(tài)函數(shù)（ 17） 行 表達(dá)式 ：類型 代換 (1) lptr ： γ (2) length ： β (3) length( lptr ) ： δ β =γ → δ (4) lptr ： γ (5) null ： list(α n)→ boolean (6) null( lptr ) ： boolean γ = list(α n) (7) 0 ： integer (8) lptr ： list(α n) (9) tl ： list(α t)→ list(α t) (10) tl( lptr )： list(α n) α t→ α n (11) length ： list(α n)→ δ (12) length( tl( lptr ) ) ： δ (13) 1 ： integer (14) + ： integer integer→integer (15) length( tl( lptr ) ) + 1： integer δ =integer (16) if ： boolean α i α i→ α i (17) if ( … ) ： integer α i=integer (18) match ： α m α m→ α m (19) match( … ) ： integer α m=integer 67 演講完畢，謝謝觀看！
規(guī)章制度相關(guān)推薦
鄂ICP備17016276號(hào)-1