为什么归纳数据类型禁止类型如`data Bad a = C(Bad a - > a)`其中类型递归发生在 - >？之前？

Question

关于归纳数据类型和模式匹配的 Agda手册:

为确保正常化,归纳事件必须出现在严格的正位置.例如,不允许以下数据类型:

data Bad : Set where
  bad : (Bad ? Bad) ? Bad

因为构造函数的参数中存在负面的Bad.

为什么归纳数据类型需要此要求？

Answer 1

您提供的数据类型是特殊的,因为它是无类型 lambda演算的嵌入.

data Bad : Set where
  bad : (Bad ? Bad) ? Bad

unbad : Bad ? (Bad ? Bad)
unbad (bad f) = f

我们来看看如何.回想一下,无类型的lambda演算有以下术语:

 e := x | \x. e | e e'

我们可以定义[[e]]从无类型lambda演算术语到Agda术语类型的翻译Bad(尽管不在Agda中):

[[x]]     = x
[[\x. e]] = bad (\x -> [[e]])
[[e e']]  = unbad [[e]] [[e']]

现在,您可以使用您最喜欢的非终止无类型lambda术语来生成类型的非终止术语Bad.例如,我们可以转换(\x. x x) (\x. x x)为Bad以下类型的非终止表达式:

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x))

虽然类型恰好是这个参数的一种特别方便的形式,但它可以通过一些工作推广到任何具有负递归递归的数据类型.

Answer 2

在Turner,DA(2004-07-28),Total Functional Programming,sect中给出了这种数据类型如何允许我们居住在任何类型中的示例.规则2中的 3.1,第758页:类型递归必须是协变的."

让我们使用Haskell做一个更详细的例子.我们将从"坏"递归数据类型开始

data Bad a = C (Bad a -> a)

并且从中构造Y组合子而没有任何其他形式的递归.这意味着拥有这样的数据类型允许我们构造任何类型的递归,或通过无限递归来居住任何类型.

无类型lambda演算中的Y组合子定义为

Y = ?f.(?x.f (x x)) (?x.f (x x))

关键是我们适用x于自己x x.在类型语言中,这不是直接可能的,因为没有x可能有效的类型.但是我们的Bad数据类型允许这个模数添加/删除构造函数:

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

采取x :: Bad a,我们可以打开它的构造函数并将函数应用于x自身.一旦我们知道如何做到这一点,构建Y组合器很容易:

yc :: (a -> a) -> a
yc f =  let fxx = C (\x -> f (selfApp x))  -- this is the ?x.f (x x) part of Y
        in selfApp fxx

请注意,既不是selfApp也不yc是递归的,也不会对函数自身进行递归调用.递归仅出现在我们的递归数据类型中.

我们可以检查构造的组合子确实做了应有的事情.我们可以做一个无限循环:

loop :: a
loop = yc id

或计算让我们说GCD:

gcd' :: Int -> Int -> Int
gcd' = yc gcd0
  where
    gcd0  :: (Int -> Int -> Int) -> (Int -> Int -> Int)
    gcd0 rec a b  | c == 0     = b
                  | otherwise  = rec b c
      where c = a `mod` b