我们可以向 Daan Leijen 的HMF寻求一些想法。(他处理“foralls”的活页夹,这也被认为是可交换的。
特别是,他重新绑定了正文中出现顺序的变量。
然后,术语的比较涉及以相同的方式进行 sklemizing 并比较结果。
我们可以通过用本地无名表示替换那个 skolemization pass 来做得更好。
data Bound t a = Bound {-# UNPACK #-} !Int t | Unbound a
instance Functor (Bound t) where ...
instance Bifunctor Bound where ...
data Expr a
= Lambdas {-# UNPACK #-} !Int (Expr (Bound () a))
| Var a
所以现在在 lambda 下出现的 Bound 是直接被 lambda 绑定的变量,以及你想在出现中放入的任何类型信息,这里我只是使用了 ()。
现在封闭项在 'a' 中是多态的,如果您按其使用站点对 lambda 的元素进行排序(并且可以确保您始终通过删除未使用的项来规范化 lambda),则 alpha 等效项仅与 (==) 进行比较,并且如果您需要开放条款,您可以使用 Expr String 或其他一些表示形式。
Expr 和 Bound 签名的更具肛门保留性的版本将使用存在类型和类型级别 natural 来识别被绑定的变量的数量,并在 Bound 构造函数中使用“Fin”,但是因为您已经必须维护不变量你绑定的变量不超过 lambda 中出现的 # ,并且类型信息在所有变量中都Var (Bound n _)
一致n
,维护另一个不是太大的负担。
更新:您可以使用我的bound
包以完全独立的方式对此进行改进!