# Logical equivalences in Haskell ●

The blogpost Classical Logic in Haskell established a way to prove equivalences between logical propositions and *law of excluded middle* by writing intances of `Iso`

for the same propositions wrapped in a `newtype`

. Vladimir’s post contain proofs of some important propositions. I had fun proving them myself. I wanted to continue with some more.

Recently, I did the Logic and Proof course to learn both proof techniques and Lean theorem prover. It was fun. So I picked few propositions from the exercises of the Propositional Logic in Lean chapter to try write equivalence proofs for them.

Below are the propositions as newtypes (their logical notations mentioned as comment) and subsequently the `Iso`

instances to prove their equivalences with `Lem`

. As mentioned in the original blogpost, one nice way to progress here is by taking clues from the type system itself in the form of typed holes.

Let’s set some language pragmas

```
:set -XMultiParamTypeClasses
:set -XRankNTypes
:set -XInstanceSigs
:set -XScopedTypeVariables
:set -XTupleSections
```

Required `Iso`

class from the original blogpost put inside a module so that it can be imported for rest of the sections

```
module Proof where
import Data.Void (Void, absurd)
class Iso a b where
to :: a -> b
from :: b -> a
-- Law of excluded middle
-- forall P. P \/ -P
newtype Lem m =
Lem
forall a .
(Either a (a -> m Void))) m (
```

```
import Data.Void
import Proof
```

And now the propositions…

```
-- forall. P,Q. P /\ (P -> Q) -> Q
import Control.Monad.Fix
newtype Prop1 m =
Prop1
forall a b.
(-> m b)) -> m b)
(a , (a
-- proof, implication elimination <==> LEM
instance Monad m => Proof.Iso (Prop1 m) (Lem m) where
from :: Lem m -> Prop1 m
= Prop1 $ uncurry (flip id)
from _
to :: Prop1 m -> Lem m
Prop1 i) = Lem $ fmap Left $ i (id, pure . fix) to (
```

```
-- forall. P,Q. P -> - (- P /\ B)
newtype Prop2 m =
Prop2
forall a b.
(-> m (((a -> m Void), b) -> m Void)))
(a
-- proof, Prop2 <==> LEM
instance Monad m => Proof.Iso (Prop2 m) (Lem m) where
to :: Prop2 m -> Lem m
Prop2 p) = Lem $ pure $ Right proof where
to ( proof :: a -> m Void
= p x >>= ($ (proof, x))
proof x
from :: Lem m -> Prop2 m
Lem l) = Prop2 $ flip fmap l . proof where
from ( proof :: a -> Either a (a -> m Void) -> (((a -> m Void), b) -> m Void)
= either (flip fst) (\f _ -> f x)
proof x
```

```
-- forall. P,Q. - (P /\ Q) -> (P -> - Q)
import Control.Applicative (liftA2)
newtype Prop3 m =
Prop3
forall a b.
(-> m Void) -> m (a -> m (b -> m Void)))
((a,b)
-- proof, Prop3 <==> LEM
instance Monad m => Proof.Iso (Prop3 m) (Lem m) where
to :: Prop3 m -> Lem m
Prop3 p) = Lem
to ($ fmap Right
$ proof
>>=
-> pure (liftA2 (>>=) f (flip id)))
(\f where
proof :: m (a -> m (a -> m Void))
= p (\(x,y) -> proof >>= (($ y) =<<) . ($ x))
proof
from :: Lem m -> Prop3 m
Lem l) = Prop3
from ($ (\f ->
pure
$ \a ->
either (const . f . (a ,)) id <$> l)
```

```
-- forall. P,Q. -P /\ -Q -> - (P \/ Q)
newtype Prop4 m =
Prop4
forall a b.
(-> m Void , b -> m Void) -> m (Either a b -> m Void)))
((a
-- proof, Prop4 <==> LEM
instance Monad m => Proof.Iso (Prop4 m) (Lem m) where
to :: Prop4 m -> Lem m
Prop4 p) = Lem
to ($ pure
$ Right
>>=) . flip id . Left)
((proof where
proof :: m (Either a a -> m Void)
= curry p ((proof >>=)
proof . flip id
. Left)
>>=)
((proof . flip id
. Right)
from :: Lem m -> Prop4 m
= Prop4 $ uncurry $ (pure .) . either from _
```

*This is an IHaskell Notebook which is pretty cool for above kind of experiments. Much more feature rich than GHCi. I got the inspiration from Vaibhav Sagar who writes all his posts as IHaskell Notebooks.*