为什么归纳数据类型禁止像 `data Bad a = C (Bad a -> a)` 这样的类型，其中类型递归出现在 -> 的前面？

Question

Agda手册中关于归纳数据类型和模式匹配的部分指出:

为了确保规范性，归纳出现必须在严格正位置。例如，下面的数据类型是不允许的：

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

由于构造函数的参数中存在Bad的负面出现，因此这个要求对归纳数据类型为什么是必要的？

- Petr

Answer 1

你给出的数据类型是特殊的，因为它是未类型化 lambda 演算的嵌入。

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

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

让我们看看如何做。回想一下，无类型的 λ演算有以下术语：

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

我们可以定义一个从未类型化的lambda演算术语到类型为Bad的Agda术语的翻译 [[e]]（尽管不能在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))

尽管这种类型恰巧是这个参数的特别方便的形式，但只要稍加努力就可以将其推广到任何具有递归负数出现的数据类型。

- Daniel Wagner

---

好的回答。我喜欢这个优雅的方法，它包括了理论解释（嵌入非类型λ演算）。能否将其扩展，以便为所讨论的语言（比如Agda）提供任意递归？ - Petr

我刚刚与比我更擅长类型理论的同事聊过，他们认为 Bad 不会产生一个类型为 forall a. a 的术语（这才是你真正关心的；递归只是到达这个目标的一种手段）。他们的观点是这样的：你可以构建一个 Agda 的集合论模型；然后，在该模型中增加一个解释 Bad 为一个单元素集合的部分；由于在结果模型中仍然存在无人居住的类型，因此没有函数将循环的 Bad 术语转化为另一种类型的循环术语。 - Daniel Wagner

Answer 2

"

这样的数据类型允许我们在任何类型中使用，例如在Turner, D.A. (2004-07-28)的函数式编程总体论中提到了一个例子，在第3.1节、758页中的规则2：类型递归必须是协变的。

"

---

让我们使用Haskell创建一个更详细的例子。我们将从一个“不好”的递归数据类型开始。

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

and构造Y组合子，而不使用任何其他形式的递归。这意味着拥有这样一种数据类型使我们能够构建任何类型的递归，或者通过无限递归来占据任何类型。

在未类型化的λ演算中，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

- Petr