为什么归纳数据类型禁止类型为'data Bad a = C（Bad a - > a）`类型递归出现在 - >之前？

Question

上Inductive Data Types and Pattern Matching状态阿格达手册：

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

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

因为有坏的参数来构造一个负的发生。

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

Answer 1

你给的数据类型的特殊之处在于它是无类型演算的嵌入。

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

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

让我们来看看如何。回想一下，无类型演算有这些条款：

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

我们可以定义从无类型演算方面Bad类型的阿格达术语翻译[[e]]（虽然不是在阿格达）：

[[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，D.A.给出了一个这样的数据类型如何让我们能够居住在任何类型中的例子。 （2004-07-28），Total Functional Programming，第二节。 3.1，页758 规则2：类型递归必须是协变“

---

让我们用Haskell的一个更复杂的例子中，我们将从一个开始。‘坏’递归类型

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

。

和构造从它的Y combinator没有递归的任何其它形式。这意味着具有这样的数据类型允许我们构建任何一种递归的，或由无限递归栖息的任何类型。

在无类型演算的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