返回学习路线

D03：审核一个类型化表达式小库 ​

给定接口与程序 ​

本题使用按值求值、词法作用域、数学整数、不可变列表和记录。引用是唯一可变对象。Expr与eval固定为下列签名，构造器与求值分支含义同名字所示：

Lit   : Int → Expr Int
Truth : Bool → Expr Bool
Add   : Expr Int → Expr Int → Expr Int
Less  : Expr Int → Expr Int → Expr Bool
If    : ∀a. Expr Bool → Expr a → Expr a → Expr a
eval  : ∀a. Expr a → a

Eq类只有方法 eq:∀a.Eq a⇒a→a→Bool。注册的基本实例只有Eq Int和Eq Bool，含义为普通整数相等和布尔相等；列表实例由Eq a构造Eq(List a)，无重叠实例、无默认化。显式字典类型为 EqDict a={eq:a→a→Bool}。

待审核小库如下，A是有意放入的可疑代码，其他部分需要补接口或检查调用。

A. let cache = ref [] in
     cache := [4];
     if head(!cache) then 1 else 0

B. fresh = λ(). ref []
   applyBoth = λf. (f 6, f false)

C. sameResult p q = eq (eval p) (eval q)
   eI = Add (Lit 2) (Lit 3)
   eB = Less (Lit 2) (Lit 3)
   testI = sameResult eI (Lit 5)
   testB = sameResult eB (Truth true)

D. p = { name="draft", expr=eI, checked=true }
   q = replace p.name with "ready"
   answer = eval q.expr

E. a = [9,8,7,6]          // 此处只作长度为4的不可变数组
   next(a,n,i) = let j=i+1 in get(a,j)
   get要求 0 <= j && j < n，且n等于数组长度

另给进阶支线的两个对象：

PairWith = λA:*. λB:*. A × B
h = ΛF:*→*. ΛA:*. λz:F A. z

data Perfect a = Leaf a | Node (Perfect (a × a))
t = Node (Node (Leaf ((1,2),(3,4))))

任务 ​

1. 若错误地把cache泛化为 ∀a.Ref(List a)，写出A的存储轨迹及卡住位置；用值限制指出应在何处拒绝
2. 给fresh与applyBoth填写满足意图的签名；说明两次调用fresh为什么能分别产生整数列表引用和布尔列表引用，而applyBoth的参数必须保留内部量词
3. 给sameResult写最一般的受约束接口，展开成显式类型/字典参数；为testI、testB选字典并算出结果；判断交换两份字典是否合法
4. 列出eval在Lit、Less、If三个分支的局部等式与递归实例，解释为什么把Less分支改成返回0会失败
5. 为D抽出一个对任意剩余字段有效的rename函数签名；给出本次行变量替换与name缺失条件，算answer
6. 为E给出足以安全读取下一元素的i前置精化，分别核验n=4、i=2和i=3；对不安全输入写出失败的具体索引
7. 求PairWith、PairWith Int、h的kind或类型，检查 h[PairWith Int][Bool](7,true)；再给depth的全称递归签名，列出t各层元素类型和深度

答案：引用与参数量词 ​

A分配一个地址ℓ，开始 $\sigma (\ell )=[]$。错误泛化让写入使用List Int、读取使用List Bool；写后 $\sigma (\ell )=[4]$，读取和head实际得到整数4，最终变成 if 4 then 1 else 0，没有合法布尔分支可走。这个列表非空，所以失败不是head的空列表边界。

正确规则在 ref [] 处不泛化，给cache一个共享α。写入[4]确定α=Int，if条件又要求α=Bool，因此静态检查拒绝。它没有等到运行时才判断同一地址该如何解释。

fresh的签名为

右侧是λ值，可泛化环境外的a。执行两次fresh产生不同新地址，分别存Int和Bool列表不会互相污染；每一个返回的引用仍是单态的。

applyBoth需要

检查体时对f的两次出现分别实例化为Int→Int和Bool→Bool。把∀移到整个箭头外，会让一次调用中的f只具有一个固定a→a，无法同时支持6和false。传入多态id时结果为 (6,false)；传入Int上的加一函数则失败，因为它不能满足任意刚性类型上的a→a承诺。

答案：约束与字典 ​

sameResult使用同一a上的两个Expr，eval分别返回a，eq产生Eq a条件。接口为

翻译为

sameResultD : ∀a. EqDict a → Expr a → Expr a → Bool
sameResultD = Λa. λ(d:EqDict a). λ(p:Expr a). λ(q:Expr a).
  d.eq (eval[a] p) (eval[a] q)

testI译成 sameResultD[Int] intEq eI (Lit 5)，两次求值都是5，结果true。testB译成 sameResultD[Bool] boolEq eB (Truth true)，两次求值都是true，结果true。

将boolEq放到第一处或intEq放到第二处都类型不符：需要的EqDict Int与EqDict Bool不能互换。即使方法在机器层面都有某种相同调用约定，也不能据此绕过类型要求。另提供第二份Int字典只会形成同类型的另一种操作选择，不是把Bool字典强制当Int字典。

答案：局部等式与GADT求值 ​

检查eval的签名时，外层α是任意刚性类型。

Less分支返回0会在目标Bool下遇到Int，拒绝。Lit分支的α≡Int只在该分支有效，不能带到Less分支，也不能把eval的全称接口改成只接收Expr Int。

答案：行与保留字段 ​

抽出的rename签名为

本次 $r=\{expr:ExprInt,checked:Bool\}$，name确实不在r里。q保留expr=eI和checked=true，只把name改为"ready"，所以q.expr:Expr Int，answer=5。若只给rename闭合签名 {name:String}→{name:String}，从该接口本身无法恢复结果的expr字段；共享行变量才明确保存这个对应关系。

答案：下一元素的精化 ​

已知n≥0且数组长度等于n，一个足够的前提是

令j=i+1，得到j≥1≥0；由i<n−1得到i+1<n，故j满足get的两侧界限。这里所有运算都在数学整数上，没有溢出。

n=4、i=2时前提为0≤2且2<3，成立；j=3，读取数组第四项6。n=4、i=3时3<3为假，接口应拒绝；若错误执行，j=4，违反j<4而越过数组末端。原本较弱的0≤i<n仅保证当前元素存在，不保证下一个元素存在。

进阶答案：类型计算与多态递归 ​

PairWith具有kind $\ast \to \ast \to \ast$，PairWith Int具有kind $\ast \to \ast$。h的类型为

实例化后参数类型 $(PairWithInt)Bool$经两次类型β归约变为Int×Bool，所以该应用合法并返回 (7,true)。若把h的第一个类型参数换成Int，kind就不匹配；这个失败发生在读取二元组项之前。

depth的接口为 $\mathrm{\forall }a.Perfecta\to Int$，Leaf返回0，Node t返回1+depth t。给定t的元素类型沿递归为

最内层Leaf深度0，两层Node各加一，结果2。单态递归占位类型会强迫β=β×β，occurs check拒绝；全称递归签名允许每次实例化不同参数，不修改当前层的刚性类型变量。

验收标准 ​

• 不安全引用例必须只用一个具体地址，并在if收到整数处指出真实卡住
• applyBoth的量词在参数内部；fresh的量词在工厂接口外部，两者解决不同问题
• sameResultD的字典类型、eval实例和构造器索引一致，testI/testB均为true
• GADT等式逐分支使用，不能跨分支累积
• 行替换保留expr和checked；下一元素读取有严格上界，i=3必须拒绝
• 可检查的显式签名不等于检查器能自动推断所有扩展的主类型

相关入口：值限制公理库值限制与安全泛化Value restriction · Relaxed value restriction限制带引用的let泛化，阻止同一存储单元被独立实例化为不兼容类型。、高秩多态公理库高秩多态与局部检查Higher-rank polymorphism · Rank-n polymorphism把全称量词放进函数参数类型，并用实例化、刚性变量与逃逸检查验证多态承诺。、受约束类型公理库受约束类型方案Qualified types · Constrained type scheme在多态方案中保留操作所需的谓词条件，以独立的蕴涵和实例解析判断调用是否有证据。、字典传递公理库类型类的字典传递翻译Type class dictionary passing · Dictionary translation把类型类条件编译为方法记录参数，并区分译后类型正确与不同证据选择的语义一致性。、GADT公理库广义代数数据类型 GADTGeneralized algebraic data type · GADT通过构造器的结果类型取得分支局部等式，使ML式索引数据的消去结果随类型参数精确变化。。行、谓词精化与类型算子为选修支线，题面已给足所需数据。