When Howard Met Curry
The Curry-Howard correspondence is a map for moving between logic and type theory, relating propositions with types and proofs with programs. It describes a two-way street, and we can freely move between the two worlds, or perhaps merely two perspectives, so long as we follow the map.
I’ve been working on a language named sequoia, which embeds polarized classical logic in Haskell. Of course, Haskell corresponds to an intuitionistic logic, so we can’t just bring arbitrary classical proofs over directly. We have to use a double-negation translation, importing classical propositions A as intuitionistic propositions ¬¬A. There are several such translations named (and infinitely more possible), differing in how many negations are placed where, but they all get the job done.
Curry-Howard tells us a translation for negations, but we can work this one out ourselves with a little logical knowledge: a negation ¬A can also be encoded as the implication A → ⊥. It’s straightforward enough: “A implies falsehood” means the same thing as “not A.”
