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

Question

Agda 手册 Inductive Data Types and Pattern Matching状态:

To ensure normalisation, inductive occurrences must appear in strictly positive positions. For instance, the following datatype is not allowed:

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

since there is a negative occurrence of Bad in the argument to the constructor.

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

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'

我们可以定义从无类型 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))

虽然该类型恰好是该参数的一种特别方便的形式，但只需做一些工作就可以将其推广到任何出现负递归的数据类型。