Dependent types over Church-encoded type in PTS/CoC

Question

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?

Answer 1

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.

2. Add one more sort:

   * : □ : △
   

   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.