第10章子定型-資料下載頁
2024-09-28 16:45本頁面
【導(dǎo)讀】子定型是類型上的一種關(guān)系，該關(guān)系隱含一。和子定型有關(guān)的語言概念是記錄、對象及依。本章考慮子定型和體現(xiàn)子定型在程序設(shè)計中。等式理論和語義模型。類型化面向?qū)ο笳Z言。當(dāng)兩個類型相等時，若表達(dá)式屬其中一個類型，有子定型的簡單類型化?本節(jié)用子定型來拓展??–Sub是類型常量b,b??在每個系統(tǒng)中，對每種類型形式，至少有一。對第二個變元是單調(diào)的，但是對第一個變元是。int解釋成一個函數(shù)集合，這些函數(shù)的定。項的所有定型規(guī)則：、、的正好包含同樣的公理。–通常，只有在??Mx在M中不是自由的。適當(dāng)?shù)囟xM（?是可推導(dǎo)的，因此
【正文】 col_point = ?x: int, y: int, c: color, move: int ? int ? col_point? – 總希望 col_point是 point的子類型 – 關(guān)鍵看 “ 相容 ” – 可以通過考慮操作 序列來理解 它們的相容性 遞歸類型和對象的記錄模型 ? 第二個例子： 子定型失敗在表面上類似的遞歸記錄類型上 type simple_set = ?member? : elt ? bool, insert: elt ? simple_set, intersect: simple_set ? simple_set? type sized_set = ?member? : elt ? bool, insert: elt ? sized_set, intersect: sized_set ? sized_set, size: int? 兩個 intersect的變元類型是不同的 遞歸類型和對象的記錄模型 type simple_set = ?member? : elt ? bool, insert: elt ? simple_set, intersect: simple_set ? simple_set? type sized_set = ?member? : elt ? bool, insert: elt ? sized_set, intersect: sized_set ? sized_set, size: int? – 假定 s, t: simple_set且 r: sized_set – 計算兩個簡單集合的交集的表達(dá)式 t – 表達(dá)式 t可能會引起錯誤 遞歸類型和對象的記錄模型 type simple_set = ?member? : elt ? bool, insert: elt ? simple_set, intersect: simple_set ? simple_set? type sized_set = ?member? : elt ? bool, insert: elt ? sized_set, intersect: sized_set ? sized_set, size: int? type sized_set? = ?member? : elt ? bool, 改用 insert: elt ? sized_set?, sized_set? intersect: simple_set ? sized_set?, 來解決 size: int? 遞歸類型和對象的記錄模型 ? ?:, record, ?的等式規(guī)則和子定型規(guī)則 (trans :)（ ） (? :)（ ） record :)（ ） – 需要一條推理規(guī)則從相等斷言得到子定型斷言 ，還需要一條規(guī) 則用于遞歸類型 ? :?, ? :? ? :? ? :?, ?? :?? ? ??? :? ??? ?1 : ? 1, . . . , ?n : ? n ? l1:?1 , …, ln:?n, ln+1:?1 , …, ln+m:?m? : ? l1 :?1, …, ln:?n? ? 遞歸類型和對象的記錄模型 ? ?:, record, ?的等式規(guī)則和子定型規(guī)則 – 從相等斷言 得到子定型斷言的規(guī)則 (= :) – 用于遞歸類型的規(guī)則 t在 ?中不是自由的 ， s在 ?中不是自由的 (? :) ? = ? ? : ? , s : t ?? : ? ? ?s.? : ?t.? ? 遞歸類型和對象的記錄模型 ? 證明 col_point : point – 最后一步的 形式必定是 – 應(yīng)先證 int : int和 col_point : point ? int ? (int ? col_point) : int ? (int ? point) – 后者從 自反性和假設(shè) col_point : point， 兩次應(yīng)用(? :)規(guī)則可得 col_point : point ? ?x: int, y: int, move: int?int?col_point, c: color? : ?x: int, y: int, move: int?int ? point? ? col_point. ?. . .? : ? point. ?. . .? 遞歸類型和對象的記錄模型 ? 加相等測試方法到點和有色點 ,則子定型失敗 type eq_point = ?x: int, y: int, eq: eq_point ? bool? type eq_col_point=?x: int, y: int, eq:eq_col_point?bool, c: color? – 最后 一步的形式總是 – 需要先證 int : int和 eq_col_point : eq_point ? (eq_col_point ? bool) : (eq_point ? bool) – 后者需要證明 eq_col_point : eq_point ? eq_point : eq_col_point eq_col_point :eq_point ? ?x:int, y:int, eq:eq_col_point?bool, c:color? : ?x: int, y: int, eq: eq_point? bool? ? eq_col_point. ?. . .? : ? eq_point. ?. . .? 習(xí) 題 第一次： , 第二次：
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1