Typy zależne od typu kodowanego przez Kościół w PTS / CoC

Eksperymentuję z systemami czystego typu w sześcianie lambda Barendregta, a konkretnie z najsilniejszym z nich, Rachunkiem Konstrukcji. Ten system ma rodzaje *i BOX. Dla przypomnienia, poniżej używam konkretnej składni Mortenarzędzia https://github.com/Gabriel439/Haskell-Morte-Library, która jest zbliżona do klasycznego rachunku lambda.

Widzę, że możemy emulować typy indukcyjne za pomocą pewnego rodzaju kodowania podobnego do Kościoła (znanego również jako izomorfizm Boehm-Berarducci dla algebraicznych typów danych). Dla prostego przykładu używam typu Bool = ∀(t : *) -> t -> t -> tz konstruktorami True = λ(t : *) -> λ(x : t) -> λ(y : t) -> xi False = λ(t : *) -> λ(x : t) -> λ(y : t) -> y.

Widzę, że typ funkcji na poziomie terminu Bool -> Tjest izomorficzny w stosunku do par typu Product T To klasycznej Product = λ(A : *) -> λ(B : *) -> ∀(t : *) -> (A -> B -> t) -> tparametryczności modularnej za pomocą funkcji, if : Bool -> λ(t : *) -> t -> t -> tktóra w rzeczywistości jest identyczna.

Wszystkie poniższe pytania dotyczą reprezentacji typów zależnych Bool -> *.

Mogę podzielić D : Bool -> *na parę D Truei D False. Czy istnieje kanoniczny sposób na Dponowne utworzenie ? Chcę odtworzyć izomoszmizm Bool -> T = Product T Tprzez analog funkcji ifna poziomie typu, ale nie mogę napisać tej funkcji tak prostej jak oryginał, ifponieważ nie możemy przekazywać rodzajów w argumentach takich jak typy.

Używam rodzaju indukcyjnego z dwoma konstruktorami do rozwiązania pytania (1). Opis wysokiego poziomu (w stylu Agda) to następujący typ (używany zamiast poziomu if)

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

z następującym kodowaniem w PTS / CoC:

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

Czy moje kodowanie powyżej jest prawidłowe?

Mogę zapisać konstruktory dla BoolDeptakiego kodu dla DepTrue : ∀(T : *) -> ∀(F : *) -> T -> BoolDep T F True:

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

ale nie mogę zapisać funkcji odwrotnej (ani żadnej funkcji w kierunku odwrotnym). Czy to możliwe? Czy powinienem użyć innej reprezentacji BoolDepdo wytworzenia izomorfizmu BoolDep T F True = T?

type-theory type-systems dependent-type

— ZeitRaffer
źródło

Bardzo miłe pytanie. Mam tylko mały problem, ja już kłopoty zrozumienia, dlaczego powinna być równa . Rozszerzanie definicji powinno być podczas gdy powinno być równe , więc dlaczego te dwa typy powinny być takie same? Czy popełniłem błędy w moich obliczeniach?

Product T T

$\text{Product T T}$

Bool \to T

$\text{Bool} \to T$

Bool \to T

$\text{Bool} \to T$

(\forall (t : *) \to (t \to t \to t)) \to T

$(\forall (t : *) \to (t \to t \to t)) \to T$

Product T T

$\text{Product} T T$

\forall (t : *) \to ((T \to T \to t) \to t)

$\forall (t : *) \to ((T \to T \to t) \to t)$

— Giorgio Mossa

@Giorgio Mossa patrz cstheory.stackexchange.com/questions/30923/... - jeśli masz parametryczność (nie we wszystkich modelach, ale w początkowej (syntaktycznej)), to masz izomorfizm.

— ZeitRaffer

Nie możesz tego zrobić za pomocą tradycyjnego kodowania Kościoła dla Bool:

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

... ponieważ nie możesz napisać (przydatnej) funkcji typu:

#Bool → *

Powodem, dla którego, jak zauważyłeś, jest to, że nie możesz podać *pierwszego argumentu #Bool, co z kolei oznacza, że argumenty Truei Falsemogą nie być typami.

Istnieją co najmniej trzy sposoby rozwiązania tego problemu:

Użyj rachunku konstrukcji indukcyjnych. Następnie możesz uogólnić typ #Boolna:
```
#Bool = ∀(n : Nat) → ∀(Bool : *ₙ) → ∀(True : Bool) → ∀(False : Bool) → Bool
```
... a potem będzie instancję ndo 1, co oznacza, że może przejść w *₀jako drugi argument, który typu check, ponieważ:
```
*₀ : *₁
```
... więc możesz użyć #Booljednego z dwóch typów.
Dodaj jeszcze jeden rodzaj:
```
* : □ : △
```
Następnie zdefiniowałbyś osobny #Bool₂typ taki jak ten:
```
#Bool₂ = ∀(Bool : □) → ∀(True : Bool) → ∀(False : Bool) → Bool
```
Jest to zasadniczo szczególny przypadek rachunku konstrukcji indukcyjnych, ale produkuje mniej kodu wielokrotnego użytku, ponieważ teraz musimy zachować dwie oddzielne definicje #Bool, po jednej dla każdego rodzaju, który chcemy wspierać.
Koduj #Bool₂bezpośrednio w rachunku konstrukcji jako:
```
#Bool₂ = ∀(True : *) → ∀(False : *) → *
```

Jeśli celem jest użycie tego bezpośrednio w niezmodyfikowanym mortestanie, zadziała tylko podejście nr 3.

— Gabriel Gonzalez
źródło

Jak widzę, nie możemy przekonwertować # Bool₁ -> # Bool₂, prawda?

— ZeitRaffer

@ZeitRaffer Zgadza się. Nie można przekonwertować z #Bool₁na#Bool₂

— Gabriel Gonzalez

Hmm ... IIUC nazywasz „Rachunkiem konstrukcji indukcyjnych” rachunkiem o nieskończonej hierarchii typów, ale AFAIK pierwotny CIC nie miał czegoś takiego (dodał tylko typy indukcyjne do CoC). Być może myślisz o ECC Luo (rachunek różniczkowy konstrukcji)?

— Stefan