11
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$ Jan 14 '16 at 11:35
  • $\begingroup$ @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. $\endgroup$
    – user34012
    Jan 14 '16 at 12:12
9
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ As I can see, we cannot convert #Bool₁ -> #Bool₂, isn't it? $\endgroup$
    – user34012
    Jan 14 '16 at 17:07
  • $\begingroup$ @ZeitRaffer That's right. You can't convert from #Bool₁ to #Bool₂ $\endgroup$ Jan 14 '16 at 17:13
  • 1
    $\begingroup$ 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)? $\endgroup$
    – Stefan
    Jun 14 '18 at 20:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy