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 Control.Monad ((<=<))
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
Lem lem) = Peirce proof
to (
where
proof :: ((a -> m b) -> m a)
-> m a
= lem >>= either pure (go abort)
proof abort
go :: ((a -> m b) -> m a)
-> (a -> m Void)
-> m a
= abort $ fmap absurd . not_a
go abort not_a
from :: Peirce m -> Lem m
Peirce p) = Lem $ p go
from (
where
go :: (Either a (a -> m Void) -> m Void)
-> m (Either a (a -> m Void))
= pure . Right $ not_lem . Left go not_lem
```

### Lem and DoubleNegation

```
instance Monad m => Iso (Lem m) (DoubleNegation m) where
to :: Lem m -> DoubleNegation m
Lem lem) = DoubleNegation proof
to (
where
proof :: ((a -> m Void) -> m Void)
-> m a
= lem >>= either pure (go notNot)
proof notNot
go :: ((a -> m Void) -> m Void)
-> (a -> m Void)
-> m a
= fmap absurd $ notNot notA
go notNot notA
from :: DoubleNegation m -> Lem m
DoubleNegation dne) = Lem $ dne not_exists_dist from (
```

### Lem and DeMorgan

```
instance Monad m => Iso (Lem m) (DeMorgan m) where
to :: Lem m -> DeMorgan m
Lem lem) = DeMorgan proof
to (
where
proof :: ((a -> m Void, b -> m Void) -> m Void)
-> m (Either a b)
= lem >>= either pure (go notNotANotB)
proof 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
DeMorgan dm) = Lem $ dm go
from (
where
go :: (a -> m Void, (a -> m Void) -> m Void)
-> m Void
= notNotA notA go (notA, notNotA)
```

### Lem and ImpliesToOr

```
instance Monad m => Iso (Lem m) (ImpliesToOr m) where
to :: Lem m -> ImpliesToOr m
Lem lem) = ImpliesToOr proof
to (
where
proof :: (a -> m b)
-> m (Either b (a -> m Void))
= either Left (go fab) <$> lem
proof fab
go :: (a -> m b)
-> (b -> m Void)
-> Either b (a -> m Void)
= Right $ notB <=< fab
go fab notB
from :: ImpliesToOr m -> Lem m
ImpliesToOr im) = Lem $ im pure from (
```

The full source code is available on my github.