I recently wrote this post about Sequent, my proof language for first-order logic. That project sent me back to the Curry-Howard correspondence, where you can get similar proof-checking capabilities embedded in another language. This post shows how to encode statically checked propositional-logic proofs in Haskell.

The Curry-Howard Correspondence#

The Curry-Howard correspondence says that propositions map to types, and proofs map to programs that inhabit those types. Under that view, proving a proposition means constructing a value of the corresponding type.

For example, a proof of p /\ q contains a proof of p and a proof of q, so it maps to the product type (p, q). A proof of p \/ q contains a proof of p or a proof of q, so it maps to the sum type Either p q. A proof of p => q turns a proof of p into a proof of q, which is a function p -> q.

This setup fits Haskell well, because the type checker can verify that a function has the type for the proposition you claim to prove. Once you encode formulas as types, GHC acts as a small proof checker for that fragment.

Intuitionistic vs. Classical Reasoning#

One thing to be aware of is that this encoding corresponds to intuitionistic logic, not classical logic. In intuitionistic logic, a proof must construct evidence for its conclusion. That fits total functional programming, where a value of type p serves as evidence for p.

Classical logic adds principles such as double-negation elimination, ~~p |- p, and excluded middle, |- p \/ ~p. Those principles are valid in classical logic, but you cannot implement them as total, parametric Haskell functions. For example, a function of type ((p -> Bot) -> Bot) -> p would need to produce an arbitrary p from a contradiction under the assumption ~p. You cannot construct such a p in general.

Haskell includes escape hatches such as undefined, error, nontermination, and unsafe operations. If you use them, you can inhabit almost any type, but the term stops being a meaningful proof. This encoding sticks to the constructive subset where proof checking matches ordinary total programs.

Encoding the Adequate Subset#

First we encode the syntactic constructs from propositional logic.

For the exact snippets below, assume the EmptyCase, ScopedTypeVariables, and TypeOperators language extensions are enabled.

data Bot
type Top = ()

type And p q = (p, q)
type Or p q = Either p q
type Imp p q = p -> q
type Neg p = p -> Bot

type Box p q = p -> q

Falsity (Bot) is simply a datatype with no value constructor, and truth (Top) is a trivially constructible type.

Defining the Rules#

As mentioned, sequents are simply function types, and proofs are function implementations with those types. The common rules for propositional logic then encode as follows.

top_i :: Top
top_i = ()

con_i :: p -> q -> p `And` q
con_i x y = (x, y)

con_e1 :: p `And` q -> p
con_e1 (x, _) = x

con_e2 :: p `And` q -> q
con_e2 (_, y) = y

imp_i :: Box p q -> p `Imp` q
imp_i f = f

imp_e :: (p `Imp` q) -> p -> q
imp_e f x = f x

dis_i1 :: p -> p `Or` q
dis_i1 x = Left x

dis_i2 :: q -> p `Or` q
dis_i2 y = Right y

dis_e :: p `Or` q -> Box p r -> Box q r -> r
dis_e (Left x) f _ = f x
dis_e (Right y) _ g = g y

bot_e :: Bot -> p
bot_e x = case x of {}

neg_i :: Box p Bot -> Neg p
neg_i f = f

neg_e :: p -> Neg p -> Bot
neg_e x f = f x

Encoding Proofs#

Finally, we can encode an actual proof in this small framework. The following is a proof of the sequent p /\ (q \/ r) |- (p /\ q) \/ (p /\ r).

dist :: p `And` (q `Or` r) -> (p `And` q) `Or` (p `And` r)
dist (prem :: (p `And` (q `Or` r)))  =
  let
    l1 = prem :: p `And` (q `Or` r)
    l2 = con_e1 l1 :: p
    l3 = con_e2 l1 :: q `Or` r
    l4_6 = (\(l4 :: q) ->
        let
          l5 = con_i l2 l4 :: p `And` q
          l6 = dis_i1 l5 :: (p `And` q) `Or` (p `And` r)
        in
          l6
        ) :: Box q ((p `And` q) `Or` (p `And` r))
    l7_9 = (\(l7 :: r) ->
        let
          l8 = con_i l2 l7 :: (p `And` r)
          l9 = dis_i2 l8 :: (p `And` q) `Or` (p `And` r)
        in
          l9
        ) :: Box r ((p `And` q) `Or` (p `And` r))
    l10 = dis_e l3 l4_6 l7_9 :: (p `And` q) `Or` (p `And` r)
  in l10

This style is not the most convenient way to prove propositions, but it demonstrates Curry-Howard in practice. You can also get a working checker with very little code.

you've reached the end of the post
until later ~ (＾▽＾)