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

Question

Agda Handbuch auf Induktive Datentypen und Mustererkennung Mitgliedstaaten:

Um eine Normalisierung zu gewährleisten, müssen induktive Ereignisse an streng positiven Positionen auftreten.Beispielsweise ist der folgende Datentyp nicht zulässig:

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

da im Argument für den Konstruktor ein negatives Auftreten von Bad auftritt.

Warum ist diese Anforderung für induktive Datentypen erforderlich?

Answer 1

Der von Ihnen angegebene Datentyp ist insofern besonders, als er eine Einbettung des ist untypisierte lambda-Kalkül.

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

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

Mal sehen, wie.Erinnern Sie sich, der untypisierte Lambda-Kalkül hat diese Begriffe:

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

Wir können eine Übersetzung definieren [[e]] von untypisierten Lambda-Kalkül-Termen zu Agda-Termen vom Typ Bad (wenn auch nicht in Agda):

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

Jetzt können Sie Ihren bevorzugten nicht terminierenden untypisierten Lambda-Term verwenden, um einen nicht terminierenden Term vom Typ zu erzeugen Bad.Zum Beispiel könnten wir übersetzen (\x. x x) (\x. x x) zum nicht terminierenden Ausdruck vom Typ Bad unten:

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

Obwohl der Typ zufällig eine besonders bequeme Form für dieses Argument war, kann er mit ein wenig Arbeit auf jeden Datentyp mit negativem Auftreten von Rekursion verallgemeinert werden.

Answer 2

Ein Beispiel, wie ein solcher Datentyp es uns ermöglicht, jeden Typ zu bewohnen, ist in Turner, D.A.(2004-07-28), Totale funktionale Programmierung, Sekte.3.1, Seite 758 in Regel 2:Typrekursion muss kovariant sein."

---

Lassen Sie uns ein ausführlicheres Beispiel mit Haskell machen.Wir beginnen mit einem "schlechten" rekursiven Datentyp

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

und konstruiere die Y-Kombinator daraus ohne irgendeine andere Form der Rekursion.Dies bedeutet, dass wir mit einem solchen Datentyp jede Art von Rekursion konstruieren oder jeden Typ durch eine unendliche Rekursion bewohnen können.

Der Y-Kombinator im untypisierten Lambda-Kalkül ist definiert als

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

Der Schlüssel dazu ist, dass wir anwenden x zu sich selbst in x x.In typisierten Sprachen ist dies nicht direkt möglich, da es keinen gültigen Typ gibt x könnte möglicherweise haben.Aber unser Bad datentyp ermöglicht dieses Modulo Hinzufügen / Entfernen des Konstruktors:

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

Einnahme x :: Bad a, können wir seinen Konstruktor auspacken und die Funktion darin anwenden auf x selbst.Sobald wir wissen, wie das geht, ist es einfach, den Y-Kombinator 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 sind rekursiv, gibt es keinen rekursiven Aufruf einer Funktion an sich selbst. Rekursion erscheint nur in unserem rekursiven Datentyp.

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

loop :: a
loop = yc id

oder berechnen wir sagen 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