Logical equivalences in Haskell ●

January 3, 2019

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 .
            m (Either a (a -> m Void)))

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. 
            (a , (a -> m b)) -> m b)
            
-- proof, implication elimination <==> LEM
instance Monad m => Proof.Iso (Prop1 m) (Lem m) where
    from :: Lem m -> Prop1 m
    from _ = Prop1 $ uncurry (flip id)
            
    to :: Prop1 m -> Lem m
    to (Prop1 i) = Lem $ fmap Left $ i (id, pure . fix)

-- forall. P,Q. P -> - (- P /\ B)

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

-- forall. P,Q. - (P /\ Q) -> (P -> - Q)
import Control.Applicative (liftA2)

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

-- forall. P,Q. -P /\ -Q -> - (P \/ Q)

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

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.