Was sind die Werte eines polymorph codierten rekursiven algebraischen Datentyps?

Question

Die folgende Frage bezieht sich auf Recursive algebraic data types via polymorphism in Haskell.

Rekursive algebraische Datentypen können in jeder Sprache mit den Fähigkeiten von System F unter Verwendung des universellen parametrischen Polymorphismus realisiert werden. Beispielsweise kann die Art der natürlichen Zahlen eingeführt werden (in Haskell) als

newtype Nat = Nat { runNat :: forall t. (t -> (t -> t) -> t) } 

mit der ‚üblichen‘ natürlichen Zahl ist, wie n

realisiert

\ x0 f -> f(f(...(f x0)...)) 

mit n Iterationen f verwendet.

In ähnlicher Weise kann die Art der Boolesche Werte als

newtype Bool = Bool { runBool :: forall t. t -> t -> t } 

mit den erwarteten Werten eingeführt werden, wahr 'und ‚falsch‘ realisiert als

true = \ t f -> t 
false = \ t f -> f 

Q: Sind alle Bedingungen von Geben Sie Bool oder Nat oder einen anderen potenziell rekursiven algebraischen Datentyp (auf diese Weise codiert) des obigen Formulars ein, bis hin zu einigen Reduktionsregeln der operativen Semantik?

Beispiel 1 (natürliche Zahlen): Ist eine Bedingung vom Typ forall t. t -> (t -> t) -> t 'gleichwertig' in gewissem Sinne mit einem Term der Form \ x0 f -> f (f (... (f x0) ...))?

Beispiel 2 (Boolesche): Ist eine Bedingung vom Typ forall t. t -> t -> t 'gleichwertig' in gewissem Sinne entweder \ t f -> t oder \ t f -> f?

Addendum (interne Version): Falls die Sprache unter Berücksichtigung auch propositionaler Gleichheit auszudrücken fähig ist, diese Meta-mathematische Frage internalisiert werden könnte wie folgt, und ich wäre sehr glücklich, wenn jemand mit kommen würde, eine Lösung dafür: wie folgt

für Funktors m können wir das Universalmodul und eine Dekodierungs-Codierungsfunktion auf sie definieren:

type ModStr m t = m t -> t 
UnivMod m = UnivMod { univProp :: forall t. (ModStr m t) -> t } 

classifyingMap :: forall m. forall t. (ModStr m t) -> (UnivMod m -> t) 
classifyingMap f = \ x -> (univProp x) f 

univModStr :: (Functor m) => ModStr m (UnivMod m) 
univModStr = \ f -> UnivMod $ \ g -> g (fmap (classifyingMap g) f) 

dec_enc :: (Functor m) => UnivMod m -> UnivMod m 
dec_enc x = (univProp x) univModStr 

Q : Falls die Sprache dies ausdrücken kann: ist der Gleichheitstyp dec_enc = id bewohnt?

Answer 1

Im System F (AKA λ2) binden, alle Einwohner von ∀α.α→α→α sind in der Tat λ -gleich K oder K*.

Erstens, wenn M : ∀α.α→α→α dann Normalform hat N (da System F normalisiert) und nach Fach Reduktion Satz (siehe Barendregt: Lambda calculi with types) auch N : ∀α.α→α→α.

Lassen Sie uns untersuchen, wie diese normalen Formen aussehen können. (Wir werden für λ2 Generierung Lemma verwenden, die Barendregt Buch für formale Details sehen.)

Wenn N eine Normalform ist, dass N (oder jedes seiner subexpression) in Kopf Normalform sein muss, dass ein Ausdruck die Form λx1 ... xn. y P1 ... Pk, wo n und/oder k auch 0

Für den Fall N, da sein können muss, weil mindestens eine λ, anfänglich haben wir keine Variable in der Typisierung Kontext gebunden, würde nehmen Sie den Platz von y. So N = λx.U und x:α |- U:α→α.

nun wieder muss es mindestens eine λ im Fall von U, sein, denn wenn U gerade sind y P1 ... Pk dann y einen Funktionstyp (0 auch für k = wir bräuchten y:α→α) haben würde, aber wir haben nur x:α im Kontext. So N = λxy.V und x:α, y:α |- V:α.

Aber V kann nicht λ.. sein, denn dann hätte es Funktionstyp τ→σ. Also V muss nur von der Form z P1 ... Pk sein, aber da wir keine Variable des Funktionstyps im Kontext haben, muss k 0 sein und deshalb V kann nur x oder y sein.

So gibt es nur zwei Begriffe in Normalform vom Typ ∀α.α→α→α: λxy.x und λxy.y und alle anderen Begriffe dieses Typs sind β-gleich einem dieser.

---

Mit einer ähnlichen Argumentation können wir beweisen, dass alle Einwohner von ∀α.α→(α→α)→α sind β-gleich einer Kirche Zeichen. (Und ich denke, dass für Typ ∀α.(α→α)→α→α die Situation etwas schlechter ist,. Wir brauchen auch η-Gleichheit, wie λf.f und λfx.fx entsprechen 1, sind aber nicht β-gleich, nur βη-gleich)

Answer 2

Wenn wir Böden und unsafe Zeug ignorieren, dann ist das einzige, was Sie universell mit Funktionen a -> a tun können, sie zu komponieren. Das stört uns jedoch nicht bei endlichen f (f (... (f x0) ...)) Ausdrücken: Wir haben auch die unendliche Zusammensetzung infty x f = f $ infty x f.

ähnlich sind die einzigen nicht-rekursive Boolesche Werte sind in der Tat \t _ -> t und \_ f -> f, aber Sie können auch Knoten hier, wie

blarg t f = blarg (blarg t f) (blarg f t)