Lambda-encoding derivation, take 2

I had the basic idea of the lambda-encoding of lambda terms right, but I was sloppy with the type derivation. The important piece that I missed was that the result type of the continuation needs to appear in two places. In general, we say a type α is equivalently representable as a function from continuations to final results:

α = (α → ο) → ο

Or you can think of this in logical terms as the equivalence

α = (α ⇒ ο) ⇒ ο

I can prove this easily with classical logic, but I had trouble finding resources presenting the axioms and standard equivalences of intuitionistic logic, and I don't feel like trying to come up with a correct, intuitionistic derivation.

The derivation of disjoint unions as pure arrow types is simple, at least using the normal rules of classical logic:

  α ∨ β
= ((α ∨ β) ⇒ ο) ⇒ ο
= ((α ⇒ ο) ∧ (β ⇒ ο)) ⇒ ο
= (α ⇒ ο) ⇒ (β ⇒ ο) ⇒ ο

Notice how the currying makes much more sense than it did last time, now that the second occurrence of the result type is there. Implication and conjunction are obviously not equivalent (duh)! But you can curry a conjunction that occurs on the left-hand side of an implication.

Again, I'm not sure how hard this is to prove intuitionistically. But assuming that goes through okay, we get the type equivalence:

α + β = (α → ο) → (β → ο) → ο