Tipe dependen atas tipe yang dikodekan Gereja dalam PTS / CoC

Saya bereksperimen dengan sistem tipe murni dalam kubus lambda Barendregt, khususnya dengan yang paling kuat, Kalkulus Konstruksi. Sistem ini memiliki macam *dan BOX. Sebagai catatan, di bawah ini saya menggunakan sintaks konkret dari Mortealat https://github.com/Gabriel439/Haskell-Morte-Library yang dekat dengan kalkulus lambda klasik.

Saya melihat kita dapat meniru tipe induktif dengan semacam pengkodean seperti Gereja (alias isomorfisma Boehm-Berarducci untuk tipe data aljabar). Sebagai contoh sederhana saya menggunakan tipe Bool = ∀(t : *) -> t -> t -> tdengan konstruktor True = λ(t : *) -> λ(x : t) -> λ(y : t) -> xdan False = λ(t : *) -> λ(x : t) -> λ(y : t) -> y.

Saya melihat bahwa tipe fungsi level-level Bool -> Tadalah isomorfik untuk pasangan tipe Product T Tdengan Product = λ(A : *) -> λ(B : *) -> ∀(t : *) -> (A -> B -> t) -> tparametrik modulo klasik dengan fungsi if : Bool -> λ(t : *) -> t -> t -> tyang sebenarnya merupakan identitas.

Semua pertanyaan di bawah ini adalah tentang representasi tipe dependen Bool -> *.

1. Saya dapat dibagi D : Bool -> *menjadi sepasang D Truedan D False. Apakah ada cara kanonik untuk menciptakan Dlagi? Saya ingin mereproduksi isomosisme Bool -> T = Product T Tdengan analog fungsi ifpada level type tetapi saya tidak dapat menulis fungsi ini sesederhana aslinya ifkarena kita tidak dapat melewatkan jenis dalam argumen seperti tipe.

2. Saya menggunakan jenis tipe induktif dengan dua konstruktor untuk menyelesaikan pertanyaan (1). Deskripsi tingkat tinggi (Agda-style) adalah tipe berikut (digunakan sebagai ganti tipe-level if)

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

   dengan penyandian berikut di PTS / CoC:

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

   Apakah pengkodean saya di atas benar?

3. Saya dapat menuliskan konstruktor untuk BoolDepseperti kode ini untuk DepTrue : ∀(T : *) -> ∀(F : *) -> T -> BoolDep T F True:

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

tapi saya tidak bisa menuliskan fungsi terbalik (atau fungsi apa pun di arah terbalik). Apa itu mungkin? Atau haruskah saya menggunakan representasi lain untuk BoolDepmenghasilkan isomorfisme BoolDep T F True = T?

Anda tidak dapat melakukan ini menggunakan pengkodean Gereja tradisional untuk Bool:

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

... karena Anda tidak dapat menulis fungsi tipe (berguna):

#Bool → *

Alasan mengapa, seperti yang Anda catat, adalah bahwa Anda tidak dapat meneruskan *sebagai argumen pertama #Bool, yang pada gilirannya berarti bahwa Truedan Falseargumen mungkin bukan tipe.

Setidaknya ada tiga cara Anda bisa menyelesaikan ini:

1. Gunakan Kalkulus Konstruksi Induktif. Maka Anda dapat menggeneralisasi jenis #Boolke:

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

   ... dan kemudian Anda akan instantiate nke 1, yang berarti Anda bisa masuk *₀sebagai argumen kedua, yang akan ketik-cek karena:

   *₀ : *₁
   

   ... jadi Anda dapat menggunakan #Booluntuk memilih antara dua jenis.

2. Tambahkan satu jenis lagi:

   * : □ : △
   

   Maka Anda akan mendefinisikan #Bool₂tipe terpisah seperti ini:

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

   Ini pada dasarnya adalah kasus khusus dari Kalkulus konstruksi Induktif, tetapi menghasilkan kode yang kurang dapat digunakan kembali karena sekarang kita harus mempertahankan dua definisi terpisah #Bool, satu untuk setiap jenis yang ingin kami dukung.

3. Menyandikan #Bool₂langsung dalam Kalkulus Konstruksi sebagai:

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

Jika tujuannya adalah untuk menggunakan ini secara langsung di dalam yang tidak dimodifikasi mortemaka hanya pendekatan # 3 yang akan bekerja.