# Dependent types over Church-encoded type in PTS/CoC

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 * and 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 -> *.

1. I can split D : Bool -> * into pair of D True and D False. Are there the canonical way to create D again? I want to reproduce isomosphism Bool -> T = Product T T by an analogue of function if at type level but I cannot write this function as simple as original if because we cannot pass kinds in arguments like types.

2. 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 if)

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?

3. I can write down the constructors for BoolDep like 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?

• Very nice question. I've just a small problem I've troubles understanding why $\text{Product T T}$ should be equal to $\text{Bool} \to T$. Expanding the definitions $\text{Bool} \to T$ should be $(\forall (t : *) \to (t \to t \to t)) \to T$ while $\text{Product} T T$ should be equal to $\forall (t : *) \to ((T \to T \to t) \to t)$, so why should these two types be the same? Or have I done some errors in my calculations? – Giorgio Mossa Jan 14 '16 at 11:35
• @Giorgio Mossa see cstheory.stackexchange.com/questions/30923/… - if you have parametricity (not in all models but in the initial (syntactic) one) then you have the isomorphism. – ZeitRaffer Jan 14 '16 at 12:12

You can't do this using the traditional Church encoding for Bool:

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

... because you can't write a (useful) function of type:

#Bool → *

The reason why, as you noted, is that you can't pass in * as the first argument to #Bool, which in turn means that the True and False arguments may not be types.

There are at least three ways you can solve this:

1. Use the Calculus of Inductive Constructions. Then you could generalize the type of #Bool to:

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

... and then you would instantiate n to 1, which means you could pass in *₀ as the second argument, which would type-check because:

*₀ : *₁

... so then you could use #Bool to select between two types.

* : □ : △

Then you would define a separate #Bool₂ type like this:

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

This is essentially a special case of the Calculus of Inductive constructions, but produces less reusable code since now we must maintain two separate definitions of #Bool, one for each sort that we wish to support.

3. Encode #Bool₂ directly within the Calculus of Constructions as:

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

If the goal is to use this directly within unmodified morte then only approach #3 will work.

• As I can see, we cannot convert #Bool₁ -> #Bool₂, isn't it? – ZeitRaffer Jan 14 '16 at 17:07
• @ZeitRaffer That's right. You can't convert from #Bool₁ to #Bool₂ – Gabriel Gonzalez Jan 14 '16 at 17:13
• Hmm... IIUC you call "Calculus of Inductive Constructions" a calculus with an infinite hierarchy of types, but AFAIK the original CIC did not have such a thing (it only added Inductive types to the CoC). You may be thinking of the Luo's ECC (Extended calculus of constructions)? – Stefan Jun 14 '18 at 20:36