cedille-cast-02.ced

module cedille-cast-02.

{-
    ◂     \f
    ★     \s
    ∀     \a
    ➔     \r
    Λ     \L
    Π     \p
    ●     \h
    ·     \.
    ι     \i.
    β     \b
    ρ     \R
    ς     \y
-}

cNat ◂ ★ = ∀ X: ★. X ➔ (X ➔ X) ➔ X.
czero ◂ cNat = Λ X. λ base. λ step. base.
csucc ◂ cNat ➔ cNat
  = λ n. Λ X. λ base. λ step. step (n base step).

{-
  Hello and welcome back to the Cedille cast, a series of videos showing how to
  write programs and proofs in Cedille. This episode is the second and final
  part of a sequence showing how it is possible to /derive/ induction for
  impredicative λ-encodings in Cedille.

  The first video showed a failed attempt at trying to do so using just the
  impredicative Calc. of Cons. + dependent pair types. The point of this was to
  show where we get stuck in this attempt, in order to motivate the new typing
  constructs that Cedille adds to complete the proof. Along the way, we noticed
  our first crucial observation -- that the proofs that *particular* number
  encodings satisfied induction looked a lot like the encodings themselves!

  The first insight into completing the proof of induction is making use of this
  strange coincidence -- could we somehow take advantage of the fact that
  numbers are "intrinsically" inductive? Can we view them as being *both* their
  own iterators *and* their own proofs of induction? Yes, we can -- by
  introducing the dependent intersection!

  Well, before talking about dependent intersection, let's just talk about a
  regular, non-dependent intersection type -- namely the idea that a single term
  can have two types. Let's start with a simple example -- the fact that zero
  can be both a Nat and a Bool!
-}

Bool ◂ ★ = ∀ X: ★. X ➔ X ➔ X.
true ◂ Bool = Λ X. λ then. λ else. then.
flse ◂ Bool = Λ X. λ then. λ else. else.

{-
  In a language with primitive inductive types, there usually is not a
  reasonable way that we could relate terms of type Bool with terms of type Nat.
  But in Cedille, these are just lambda terms -- and we can notice immediately
  that the term `true` and `zero` share the same untyped representation.
  Intersection gives us a way to state that these two terms are really the same,
  just with different type annotations

  Note that ι is input with \i
-}

zeroιtrue ◂ ι _: cNat. Bool
  = [ czero , true ].

{-
  The lhs erases to λ base. λ step. base, and the rhs erases to λ then. λ else.
  then -- and these are alpha convertible! Even though `else` has type `X` and
  `step` has type `X ➔ X`, it doesn't really matter because neither of these
  terms are used in the bodies of czero and true
-}

czero2 ◂ cNat = zeroιtrue.1 .
true2  ◂ Bool = zeroιtrue.2 .

{-
  Now, by the way, that .1 and .2 notation is for projecting from an
  intersection. The idea is that .1 lets you "view" the lhs of the intersection,
  and .2 lets you view the rhs.

  Note that in this example it's definitely non-dependent because I haven't
  given the first component a name -- that's what the underscore in ι _: cNat.
  Bool means. Adding dependency means that the second type (the rhs of the
  intersection) can /depend upon/ the term given for the lhs of the intersection
  -- but the twisty thing about this is that the terms for the lhs and rhs are
  ultimately the /same/ (untyped) term! You can think of the dependent
  intersection as telling a kind of story: first, here's a simpler type I can
  give for this term; next, here's a more enriched type for this term -- which,
  by the way, can mention itself threw the "view" of the term given in the left
  hand side of the intersection!

  We will make this more concrete by using the dependent intersection on cNats
  and proofs that they are inductive. We begin by defining the predicate that a
  particular cNat is inductive.
-}

iNat ◂ cNat ➔ ★
  = λ n: cNat. ∀ P: cNat ➔ ★. P czero ➔ ({- Π -} ∀ m: cNat. P m ➔ P (csucc m)) ➔ P n.

izero ◂ iNat czero
  = Λ P. λ base. λ step. base.

isucc ◂ {-Π-} ∀ m: cNat. iNat m ➔ iNat (csucc m)
  = Λ m. λ im. Λ P. λ base. λ step. step -m (im base step).

{- Indeed, the real Nat is the intersection of all cNats that are also proofs
   of their own induction!
-}

Nat ◂ ★ = ι x: cNat. iNat x.

zero ◂ Nat = [ czero , izero ].
succ ◂ Nat ➔ Nat = λ n. [ csucc n.1 , isucc -n.1 n.2 ] .

{-
  Unfortunately we run into trouble with our successor case. The successor for
  cNat only takes one argument (the predecessor), but the successor for iNat
  requires its predecessor, which has an indexed type... *and* the term
  occupying the index! That is to say, we have to give some cNat first so that
  we know which cNat our iNat is referring too! So there's this extra argument n.1
  in the middle that we only really for typing the second argument, and this is
  thwarting convertibility of these two terms. How frustrating!

  Fortunately, we can address this with the next construct Cedille adds --
  irrelevant products, ∀. Earlier we said that you can think of this as being the
  quantifier for types, but this is not the whole story -- now we can reveal
  that it's the quantifier for *all* erased entities, which includes terms as
  well! An erased term is used only for typing, but does not appear in the
  erasure of the term (you can think of this as the "run time" of the term.)
  Let's go ahead and make the cNat required by the successor case /irrelevant/

  Note that Cedille requires we mark application to an irrelevant argument with
  the dash -

  Now we can make some progress proving induction! Right now we're quite there
  yet. We have Nat, which gives us induction for cNats -- but we don't have an
  induction principle Nats themselves! Let's try to prove induction on Nats and
  see where this goes wrong before we add the final typing construct.
-}

indNat-fail1 ◂ ∀ P: Nat ➔ ★. P zero ➔ (∀ m: Nat. P m ➔ P (succ m)) ➔ Π n: Nat. P n
  = Λ P. λ base. λ step. λ n. n.2 ·{-●-}P base step.

{- So close! But our "induction" proof only holds for cNats, not
   Nats. So we need to express our motive concerning P as a property concerning
   cNats. And to do *that*, we need a way to convert cNats to Nats.
-}

cNat2Nat ◂ cNat ➔ Nat
  = λ n. n zero succ.

{-
   But similar to the last video, we need some way to relate the Nat we got from
   "rebuilding" our cNat by giving it `zero` and `succ` to the original Nat! See
   here
-}

indNat-fail2 ◂ ∀ P: Nat ➔ ★. P zero ➔ (∀ m: Nat. P m ➔ P (succ m)) ➔ Π n: Nat. P n
  = Λ P. λ base. λ step. λ n. n.2 ·(λ n: cNat. P (cNat2Nat n)) base step.

{-
   We're told that n is not necessarily equal to cNat2Nat n -- well, you'll have
   to forgive Cedille here for eagerly applying erasure on terms, because what
   it's really saying is that it can't see that {n ≃ cNat2Nat n.1}. Happily
   enough we can prove this as it stands in Cedille, with just cNat induction,
   using a built in equality type!
-}

refNat ◂ Π n: Nat. { n ≃ cNat2Nat n.1 }
  = λ n. n.2 ·(λ x: cNat. {x ≃ cNat2Nat x}) β (Λ m. λ eq. ρ+ ς eq - β).

{-
   Now, besides impredicativity, this might just be one of the most
   controversial things Cedille does. Because if you look closely, the variable
   x is used as if it had two different types -- x is used both where it's
   expected to have type Nat and type cNat. You can do this in Cedille because
   its equality is *UNTYPED*. In Cedille, equality means merely βη equality
   of untyped λ-expressions.

   Again, this may seem strange, but in an extrinsic theory in Cedille, we
   consider the ultimate meaning of an expression to be its erased, pure λ-term,
   not the type annotations ascribed to it. So the things we really care about
   equating are pure λ-terms!

   The last piece missing from this puzzle in seeing how this definition could
   possibly make sense, is understanding the erasure for projections .1 and .2
   of dependent intersections. Since both the lhs and rhs of an intersection
   have the same untyped underlying term, first and second projections get
   erased -- because all they are are "views" into the same term. To make what
   I'm saying more concrete:
-}

proj1Erase ◂ Π m: Nat. { m ≃ m.1} = λ m. β.
proj2Erase ◂ Π m: Nat. { m ≃ m.2} = λ m. β.

{-
   This allows us to say, at the end of the day, that we get the same untyped
   λ-term n from running cNat2Nat on n.1 -- and that even though the result we
   get might have a different type than n, since it's the same untyped term, in
   a sense we already know we can ascribe to it both types cNat and Nat.

   With reflection proven, we can now, finally, derive induction.
-}

indNat ◂ ∀ P: Nat ➔ ★. P zero ➔ (∀ m: Nat. P m ➔ P (succ m)) ➔ Π n: Nat. P n
  = Λ P. λ base. λ step. λ n.
     [ pf = n.2 ·(λ n: cNat. P (cNat2Nat n)) base (Λ m. λ pf'. step -(cNat2Nat m) pf')]
     - ρ (refNat n) - pf.


-- ADDENDUM: Computation Law
-- Induction is just iteration!
compLaw ◂ ∀ P: Nat ➔ ★. Π base: P zero. Π step: (∀ m: Nat. P m ➔ P (succ m)). Π n: Nat.
    {indNat base step n ≃ n base step}
  = Λ P. λ base. λ step. λ n. β.