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.

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`

).

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:

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
)
```

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))
)
```

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
)
```

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)
)
```

$ \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))
)
```

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).

```
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
```

```
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
```

```
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
```

```
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,
or post an issue on this
blog's github repo.