16

Agda归纳数据类型和模式匹配手册说明：

为了确保归一化，感应事件必须出现在严格的正位置。例如，不允许使用以下数据类型： 

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

因为在构造函数的参数中有一个负面的 Bad 出现。

为什么这个要求对于归纳数据类型是必要的？

4

2 回答 2

14

您提供的数据类型很特殊，因为它是无类型 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))

尽管该类型恰好是该参数的一种特别方便的形式，但可以通过一些工作将其推广到具有负递归出现的任何数据类型。

于 2012-09-29T08:54:39.960 回答
13

Turner, DA (2004-07-28), Total Functional Programming , sect.中给出了这种数据类型如何让我们适应任何类型的示例。3.1，第 758 页规则 2：类型递归必须是协变的。”

让我们用 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
于 2012-09-29T08:21:05.927 回答