爲什麼歸納數據類型禁止類型爲'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