Warum verbieten induktive Datentypen Typen wie `data Bad a = C (Bad a -> a)`, wo die Typrekursion vor -> auftritt?

Question

Agda Handbuch auf Inductive Data Types and Pattern Matching Zustände:

Normalisierung zu gewährleisten, müssen induktive Vorkommen in streng positive Positionen erscheinen. Zum Beispiel wird der folgende Datentyp nicht zulässig:

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

da ein negatives Auftreten von Bad im Argumente an den Konstruktor ist.

Warum ist diese Anforderung für induktive Datentypen erforderlich?

Answer 1

Der Datentyp Sie gab besondere ist, dass es sich um eine Einbettung des Lambda-Kalkül untypisierten ist.

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

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

Mal sehen, wie. Recall, der nicht typisierten Lambda-Kalkül hat diese Begriffe:

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

Wir haben eine Übersetzung [[e]] von nicht typisierten Lambda-Kalkül Begriffe Agda nach Art definieren Bad (wenn auch nicht in Agda):

[[x]]  = x 
[[\x. e]] = bad (\x -> [[e]]) 
[[e e']] = unbad [[e]] [[e']] 

Sie jetzt kann Ihren bevorzugten nicht terminierenden untypisierten Lambda-Ausdruck verwenden, um einen nicht terminierenden Ausdruck vom Typ Bad zu erzeugen. Zum Beispiel haben wir (\x. x x) (\x. x x) auf den nicht abbrechenden Ausdruck des Typs Bad unten übersetzen könnten:

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x)) 

Obwohl der Typ eine besonders geeignete Form für dieses Argument sein passiert ist, kann es mit einem wenig Arbeit zu einem verallgemeinert Datentyp mit negativem Auftreten der Rekursion.

Answer 2

Ein Beispiel, wie solch ein Datentyp es erlaubt, einen beliebigen Typ zu bewohnen, ist in Turner, D.A. (2004-07-28), Total Functional Programming, sect. 3.1, Seite 758 in Regel 2: Typ Rekursion muss covariant sein „

---

Lassen Sie uns eine aufwändigere Beispiel mit Haskell machen wir mit einem beginnen werde. "Schlecht" rekursive Datentyp

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

.

und die Y combinator daraus ohne jede andere Form der Rekursion konstruieren. das bedeutet, dass ein Datentyp aufweist, so uns, jede Art von Rekursion erlaubt zu konstruieren, oder jede Art von einer unendlichen Rekursion bewohnen.

Die Y-Kombinator im untypisierten Lambda-Kalkül als

Y = λf.(λx.f (x x)) (λx.f (x x)) 

Der Schlüssel definiert ist, dass wir x sich in x x anzuwenden. In typisierten Sprachen ist dies nicht direkt möglich, weil es keinen gültigen Typ x hätte. Aber unsere Bad Datentyp ermöglicht diese Modulo Hinzufügen/Entfernen von den Konstruktor:

selfApp :: Bad a -> a 
selfApp (x@(C x')) = x' x 

x :: Bad a machen, können wir den Konstruktor auszupacken und die Funktion nach innen x selbst anwenden. Sobald wir wissen, wie Sie dies tun, dann ist es einfach, die Y Combinator zu konstruieren:

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 

Beachten Sie, dass weder selfApp noch yc rekursiv sind, gibt es keine rekursiven Aufruf einer Funktion selbst. Rekursion erscheint nur in unserem rekursiven Datentyp.

Wir können überprüfen, dass der konstruierte Kombinator tatsächlich das tut, was er sollte. Wir können eine Endlosschleife machen:

loop :: a 
loop = yc id 

oder berechnen die GCD lassen sagen:

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