haskell - 表示头部正态 lambda 演算 AST 中的固定点

Question

考虑以下在类型检查期间获得的规范化术语表示：

data Normal a
  = Neutral (Neutral a)
  | Type
  | Pi (Normal a) (Normal (Maybe a))
  | Abstract (Normal (Maybe a))

data Neutral a
  = Variable a
  | Apply (Neutral a) (Normal a)

我希望能够在这个框架内表示一个固定点，或者至少以一种保留其 head-normal 属性的方式表示，这对于实现替换和定义相等非常方便。

起初，我想使用在微积分本身中定义的定点组合器。不过，Y 组合子是不可能的，因为对于这个术语表示，我不能将 lambda 应用于 lambda。Z 组合器接近我想要的，但假设结果是一个函数。

如果我只是简单地进行图形缩减，我会与 Haskell 本身打成一片，从而导致一个惰性无限语法树。但是，由于这被用于依赖类型检查器，我需要能够测试术语的定义相等性——这样会陷入无限循环。