Classical Logic in Haskell

Dec 14, 2018

During a very pleasant conversation at a recent Bucharest FP meetup, somebody mentioned that Cont is, almost exactly, Peirce's law. I remembered seeing a tweet from Phil Freeman which proves that they are indeed equivalent. I thought it would be a fun exercise to prove other equivalences from classical logic.

This post assumes you are familar with: - the Curry-Howard correspondence, - classical and intuitionistic logic (for example, see it explained using Coq in Software Foundations), and - one of Haskell, Agda, Idris or Coq.

# MonadCont and the Law of Excluded Middle

Haskell and PureScript define MonadCont, which represent monads that support the call-with-current-continuation (callCC) operation:

class Monad m => MonadCont m where
callCC :: ((a -> m b) -> m a) -> m a 

callCC generally calls the function it receives, passing it the current continuation (the a -> m b). This acts like an abort method, or an early exit.

The interesting part is that this monad looks very similar to Peirce's law:

$((P \to Q) \to P) \to P$

If we replace P with a (or m a) and Q with m b, we get the exact same thing. Since we are dealing with monads, we need to use Kleisli arrows, so all implications from logic must be lifted as such (so P -> Q becomes a -> m b).

## Proving equivalences

In order to keep things clean, I decided to wrap each equivalent law in its own newtype and write an instance of Iso (which translates to iff) between each of the laws and the law of excluded middle.

{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module Logic where

import           Control.Applicative (liftA2)
import           Data.Void           (Void, absurd)

class Iso a b where
to :: a -> b
from :: b -> a

This is just a neat way of having to prove both implications in an iff, packed as to and from. Moving on, we can declare the following types:

### Peirce's law

Starting with the formula from logic, we can easily write out the Haskell type by just keeping in mind we have to transform all implications to Kleisli arrows:

$\forall P, Q. ((P \to Q) \to P) \to P$

newtype Peirce m =
Peirce
(  forall a b
.  ((a -> m b) -> m a)
-> m a
)

### Law of Excluded Middle

The key part to remember here is that negation in classical logic translates to -> Void in intuitionistic logic (and -> m Void in our case, since we are using Kleisli arrows):

$\forall P. P \lor \neg P$

newtype Lem m =
Lem
(  forall a
.  m (Either a (a -> m Void))
)

### Double Negation

Nothing new here, just rewriting negation as -> m Void:

$\forall P. \neg \neg P \to P$

newtype DoubleNegation m =
DoubleNegation
(  forall a
.  ((a -> m Void) -> m Void)
-> m a
)

### De Morgan's Law

The only new thing here is that we translate and to tuples, and or to Either:

$\forall P, Q. \neg (\neg P \land \neg Q) \to P \lor Q$

newtype DeMorgan m =
DeMorgan
(  forall a b
.  ((a -> m Void, b -> m Void) -> m Void)
-> m (Either a b)
)

### Implication to Disjunction

$\forall P, Q. (P \to Q) \to Q \lor \neg P$

newtype ImpliesToOr m =
ImpliesToOr
(  forall a b
.  (a -> m b)
-> m (Either b (a -> m Void))
)

## Proofs

If this is interesting to you, this would be a good place to look away and try for yourself. If you do, keep in mind that typed holes are a very useful tool in this process (see this for an example).

### Lem and Peirce

instance Monad m => Iso (Lem m) (Peirce m) where
to :: Lem m -> Peirce m
to (Lem lem) = Peirce proof

where
proof
:: ((a -> m b) -> m a)
-> m a
proof abort = lem >>= either pure (go abort)

go
:: ((a -> m b) -> m a)
-> (a -> m Void)
-> m a
go abort not_a = abort $fmap absurd . not_a from :: Peirce m -> Lem m from (Peirce p) = Lem$ p go

where
go
:: (Either a (a -> m Void) -> m Void)
-> m (Either a (a -> m Void))
go not_lem = pure . Right $not_lem . Left ### Lem and DoubleNegation instance Monad m => Iso (Lem m) (DoubleNegation m) where to :: Lem m -> DoubleNegation m to (Lem lem) = DoubleNegation proof where proof :: ((a -> m Void) -> m Void) -> m a proof notNot = lem >>= either pure (go notNot) go :: ((a -> m Void) -> m Void) -> (a -> m Void) -> m a go notNot notA = fmap absurd$ notNot notA

from :: DoubleNegation m -> Lem m
from (DoubleNegation dne) = Lem $dne not_exists_dist ### Lem and DeMorgan instance Monad m => Iso (Lem m) (DeMorgan m) where to :: Lem m -> DeMorgan m to (Lem lem) = DeMorgan proof where proof :: ((a -> m Void, b -> m Void) -> m Void) -> m (Either a b) proof notNotANotB = lem >>= either pure (go notNotANotB) go :: ((a -> m Void, b -> m Void) -> m Void) -> (Either a b -> m Void) -> m (Either a b) go notNotANotB = fmap absurd . notNotANotB . liftA2 (,) (. Left) (. Right) from :: DeMorgan m -> Lem m from (DeMorgan dm) = Lem$ dm go

where
go
:: (a -> m Void, (a -> m Void) -> m Void)
-> m Void
go (notA, notNotA) = notNotA notA

### Lem and ImpliesToOr

instance Monad m => Iso (Lem m) (ImpliesToOr m) where
to :: Lem m -> ImpliesToOr m
to (Lem lem) = ImpliesToOr proof

where
proof
:: (a -> m b)
-> m (Either b (a -> m Void))
proof fab = either Left (go fab) <$> lem go :: (a -> m b) -> (b -> m Void) -> Either b (a -> m Void) go fab notB = Right$ notB <=< fab

from :: ImpliesToOr m -> Lem m
from (ImpliesToOr im) = Lem \$ im pure

The full source code is available on my github.

Questions? Comments? Tweet them at me or post an issue on this blog's github repo.