Partially implements a natural deduction system in Haskell

NaturalDeduction.hs

{-# LANGUAGE TypeOperators #-}
module NaturalDeduction where

data (⊥) -- no inhabitants
type (¬)p = p -> (⊥)
type (∧) = (,)
type (∨) = Either
type (→) = (->)

modusTollens :: (p → q) ∧ (¬)q → (¬)p
modusTollens (φ, ψ) = ψ . φ

true :: truth
true = true

exclMid :: p ∧ (¬)p
exclMid = true

type p ↔ q = (p → q) ∧ (q → p)

dblNeg :: p ↔ (¬)((¬) p)
dblNeg = (flip ($), true)

transposition :: (p → q) ↔ ((¬)q → (¬)p)
transposition =
    (curry modusTollens, \c p -> -- c = contrapositive
        undoDblNegate $ curry modusTollens c $ dblNegate p)
            where (dblNegate, undoDblNegate) = dblNeg