1

我正在尝试实现一个玩具常规类型系统，以确保一些良好的侧向约束并允许在其中展开 mu 绑定。表示这些类型的数据类型包含用于定点 ( ) 的构造函数、由最近的封闭 Mu 绑定项 ( ) 以及零和一个参数类型运算符（分别为和Mu）替换。VarNullaryUnary

为了确保这些类型的格式正确，它们作为三个Bool参数跟踪它们是否具有 aMu作为它们的头构造函数、aVar作为它们的头构造函数，或者它们中的Var任何地方。

data A : Bool -- Is Mu headed?
      -> Bool -- Is Var headed?
      -> Bool -- Contains any Var's?
      -> Type where
Mu : A False False _ -> A True False False
Var : A False True True
Nullary : A False False False
Unary : A _ _ m -> A False False m

为了实现 Mu-headed 类型的展开，我需要执行替换，特别是我需要实现“Mu x. F ====> F[(Mu x. F)/x]”。

除了需要一些来生成第三个类型参数有效的证明之外，该函数subst似乎很简单：

total subst : A m1 v1 c1 -> A m2 v2 c2 -> (c3 ** ((A (m2 || (v2 && m1)) 
                                                     (v2 && v1) 
                                                     c3)
                                             ,(c3 = (c2 && c1))))
subst _ Nullary = (_ ** (Nullary,Refl))
subst w (Unary a) with (subst w a)
  | (c3** (a',aeq)) = (c3 ** (Unary a',aeq))
subst w Var = (_ ** (w,Refl))
subst w (Mu a) = (_ ** (Mu a,Refl))

我尝试并未能编写一个稍微清理此返回类型的包装器。

total subst' : A m1 v1 c1 -> A m2 v2 c2 -> A (m2 || (v2 && m1)) 
                                             (v2 && v1) 
                                             (c2 && c1)
subst' a1 a2 with (subst a2 a2)
  | (_**(a',aeq)) ?=  a'

当我尝试解决这个元变量时，我发现它aeq : x = c2 && Delay c2不像aeq : x = c2 && Delay c1我预期的那样（回想一下 ( &&) 在它的第二个参数中是惰性的）。

难道我做错了什么？这是预期的行为吗？FWIW，我成功地为展开（未显示）编写了一个非常相似的包装器。

4

1 回答 1

1

我想问题是线路

subst' a1 a2 with (subst a2 a2)

您不是要调用substanda1还是a2相反？

于 2015-05-14T15:26:24.483 回答