Abhängige Typen über kirchencodierten Typen in PTS / CoC

Ich experimentiere mit reinen Typsystemen in Barendregts Lambda-Würfel, speziell mit dem mächtigsten, dem Calculus of Constructions. Dieses System hat Sorten *und BOX. Nur zur Veranschaulichung: Im Folgenden verwende ich die konkrete Syntax des MorteTools https://github.com/Gabriel439/Haskell-Morte-Library, das dem klassischen Lambda-Kalkül nahe kommt.

Ich sehe, wir können induktive Typen durch eine Art kirchenähnliche Codierung emulieren (auch bekannt als Boehm-Berarducci-Isomorphismus für algebraische Datentypen). Für ein einfaches Beispiel verwende ich type Bool = ∀(t : *) -> t -> t -> tmit den Konstruktoren True = λ(t : *) -> λ(x : t) -> λ(y : t) -> xund False = λ(t : *) -> λ(x : t) -> λ(y : t) -> y.

Ich sehe, dass der Typ der Funktionen auf Bool -> TTermebene zu Typpaaren Product T Tmit klassischer Product = λ(A : *) -> λ(B : *) -> ∀(t : *) -> (A -> B -> t) -> tModulo-Parametrizität mittels einer Funktion, if : Bool -> λ(t : *) -> t -> t -> tdie tatsächlich Identität ist, isomorph ist.

Alle folgenden Fragen beziehen sich auf Darstellungen abhängiger Typen Bool -> *.

1. Ich kann mich D : Bool -> *in ein Paar von D Trueund aufteilen D False. Gibt es den kanonischen Weg, Dwieder zu schaffen ? Ich möchte den Isomosphismus Bool -> T = Product T Tdurch ein Analogon der Funktion ifauf Typebene reproduzieren, aber ich kann diese Funktion nicht so einfach wie das Original schreiben, ifda wir keine Arten in Argumenten wie Typen übergeben können.

2. Ich benutze eine Art induktiven Typ mit zwei Konstruktoren, um Frage (1) zu lösen. Die Beschreibung auf hoher Ebene (Agda-Stil) ist der folgende Typ (anstelle von Typ-Ebene verwendet if)

   data BoolDep (T : *) (F : *) : Bool -> * where
     DepTrue : T -> BoolDep T F True
     DepFalse : F -> BoolDep T F False
   

   mit der folgenden Codierung in PTS / CoC:

   λ(T : *) -> λ(F : *) -> λ(bool : Bool ) ->
   ∀(P : Bool -> *) ->
   ∀(DepTrue : T -> P True ) ->
   ∀(DepFalse : F -> P False ) ->
   P bool
   

   Ist meine obige Kodierung korrekt?

3. Ich kann die Konstruktoren für BoolDepdiesen Code aufschreiben für DepTrue : ∀(T : *) -> ∀(F : *) -> T -> BoolDep T F True:

   λ(T : *) ->  λ(F : *) ->  λ(arg : T ) ->
   λ(P : Bool -> *) ->
   λ(DepTrue : T -> P True ) ->
   λ(DepFalse : F -> P False ) ->
   DepTrue arg
   

aber ich kann die Umkehrfunktion (oder irgendeine Funktion in der Umkehrrichtung) nicht aufschreiben. Ist es möglich? Oder sollte ich eine andere Darstellung verwenden BoolDep, um einen Isomorphismus zu erzeugen BoolDep T F True = T?

Sie können dies nicht mit der traditionellen Kirchencodierung tun für Bool:

#Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

... weil Sie keine (nützliche) Funktion vom Typ schreiben können:

#Bool → *

Der Grund dafür ist, wie Sie bemerkt haben, dass Sie nicht *als erstes Argument an übergeben können #Bool, was wiederum bedeutet, dass die Argumente Trueund Falsemöglicherweise keine Typen sind.

Es gibt mindestens drei Möglichkeiten, wie Sie dies lösen können:

1. Verwenden Sie die Berechnung der induktiven Konstruktionen. Dann könnten Sie den Typ von verallgemeinern #Bool:

   #Bool = ∀(n : Nat) → ∀(Bool : *ₙ) → ∀(True : Bool) → ∀(False : Bool) → Bool
   

   ... und dann würden Sie instanziiert nzu 1, was bedeutet , Sie passieren könnte *₀als das zweite Argument, das würde Typprüfung , weil:

   *₀ : *₁
   

   ... also können Sie #Boolzwischen zwei Typen wählen.

2. Fügen Sie eine weitere Sorte hinzu:

   * : □ : △
   

   Dann würden Sie einen separaten #Bool₂Typ wie folgt definieren :

   #Bool₂ = ∀(Bool : □) → ∀(True : Bool) → ∀(False : Bool) → Bool
   

   Dies ist im Wesentlichen ein Sonderfall der Berechnung induktiver Konstruktionen, erzeugt jedoch weniger wiederverwendbaren Code, da wir jetzt zwei separate Definitionen von pflegen müssen #Bool, eine für jede Sorte, die wir unterstützen möchten.

3. Codieren Sie #Bool₂direkt in der Konstruktionsrechnung als:

   #Bool₂ = ∀(True : *) → ∀(False : *) → *
   

Wenn das Ziel darin besteht, dies direkt in unverändert zu verwenden, mortefunktioniert nur Ansatz 3.