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$
  • $\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$ – Giorgio Mossa 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$ – ZeitRaffer 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$
  • $\begingroup$ As I can see, we cannot convert #Bool₁ -> #Bool₂, isn't it? $\endgroup$ – ZeitRaffer Jan 14 '16 at 17:07
  • $\begingroup$ @ZeitRaffer That's right. You can't convert from #Bool₁ to #Bool₂ $\endgroup$ – Gabriel Gonzalez 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

Not the answer you're looking for? Browse other questions tagged or ask your own question.