I'm experimenting with pure type systems in Barendregt's lambda cube, specifically with the most powerfull one, the Calculus of Constructions. This system has sorts
BOX. Just for the record, below I'm using the concrete syntax of the
Morte tool https://github.com/Gabriel439/Haskell-Morte-Library which is close to the classical lambda calculus.
I see we can emulate inductive types by some kind of Church-like encoding (a.k.a. Boehm-Berarducci isomorphism for algebraic data types).
For a simple example I use type
Bool = ∀(t : *) -> t -> t -> t with the constructors
True = λ(t : *) -> λ(x : t) -> λ(y : t) -> x and
False = λ(t : *) -> λ(x : t) -> λ(y : t) -> y.
I see that the type of term-level functions
Bool -> T is isomorphic to pairs of type
Product T T with classical
Product = λ(A : *) -> λ(B : *) -> ∀(t : *) -> (A -> B -> t) -> t modulo parametricity by means of function
if : Bool -> λ(t : *) -> t -> t -> t which is in fact identity.
All questions below will be about representations of dependent types
Bool -> *.
I can split
D : Bool -> *into pair of
D False. Are there the canonical way to create
Dagain? I want to reproduce isomosphism
Bool -> T = Product T Tby an analogue of function
ifat type level but I cannot write this function as simple as original
ifbecause we cannot pass kinds in arguments like types.
I use a kind of an inductive type with two constuctors to solve question(1). The high level description (Agda-style) is the following type (used instead of type-level
data BoolDep (T : *) (F : *) : Bool -> * where DepTrue : T -> BoolDep T F True DepFalse : F -> BoolDep T F False
with the following encoding in PTS/CoC:
λ(T : *) -> λ(F : *) -> λ(bool : Bool ) -> ∀(P : Bool -> *) -> ∀(DepTrue : T -> P True ) -> ∀(DepFalse : F -> P False ) -> P bool
Is my encoding above correct?
I can write down the constructors for
BoolDeplike this code for
DepTrue : ∀(T : *) -> ∀(F : *) -> T -> BoolDep T F True:
λ(T : *) -> λ(F : *) -> λ(arg : T ) -> λ(P : Bool -> *) -> λ(DepTrue : T -> P True ) -> λ(DepFalse : F -> P False ) -> DepTrue arg
but I cannot write down the inverse function (or any function in the inverse direction). Is it possible? Or should I use another representation for
BoolDep to produce an isomorphism
BoolDep T F True = T?