Functor/Applicative/Monad instances

[BlackCapCoder]

Every function related to (-->) can be implemented in terms of modesPones:

trans bc ab = introImpl $ modusPonens bc . modusPonens ab

lmapImpl ab bc = bc `trans` introImpl ab
rmapImpl bc ab = introImpl bc `trans` ab
dimapImpl ab cd bc = introImpl cd `trans` bc `trans` introImpl ab

elimImpl = flip modesPones
modusTollens impl q' = introNot $ \p -> contradicts' q' (modusPonens impl p)

It seems like (-->) is just a new name for (->) within proofs - modesPones is function application and trans is composition.

modusPonens :: Proof (a --> b) -> Proof a -> Proof b
($)         ::       (a  -> b) ->       a ->       b

trans       :: Proof (b --> c) -> Proof (a --> b) -> Proof (a --> c)
(.)         ::       (b  -> c) ->       (a  -> b) ->       (a  -> c)

Knowing this we can write a sensible Functor instance:

-- Given 'a' we can produce 'b'
-- Therefor, 'a' implies 'b'
impl :: (a -> b) -> Proof (a --> b)
impl _ = axiom

instance Functor Proof where
  fmap = modusPonens . impl

Issue #2 argues against having Functor/Applicative/Monad instances on the grounds that lifting functions into a proof is confusing: The proof is merely a statement known to be true, so how can I run a function inside of it if it does not contain any values?

My proposed solution is to interpret Proof a not as "a is true" but "a is inhabited", yielding the following Applicative and Monad instances:

-- I have observed an instance of 'a'
-- Therefor, there exist instances of 'a'
observe :: a -> Proof a
observe _ = axiom

-- There exist a proof that proves the existence of a proof of 'a'
-- Therefor, a proof of 'a' exist
proofOfProof :: Proof (Proof a) -> Proof a
proofOfProof _ = axiom

instance Applicative Proof where
  pure  = observe
  (<*>) = ap

instance Monad Proof where
  a >>= f = join $ fmap f a
    where
      join = proofOfProof

Just having these instances give us a lot of utility. In addition I propose replacing custom datatypes with type aliases:

type FALSE = Void
type TRUE = ()
type And = (,)
type Or = Either
type Implies = (->)

These changes does not buy us more power: We still cannot create instances of FALSE nor prove 'p' from 'Not p' outside of Classical.

As before all operations on proofs are O(0), and a partial or diverging function can prove a false or undecidable statement in finite time:

-- before changes
axiom :: ∀ a. Proof a
axiom = introImpl (fix id) `modusPonens` true
axiom = introImpl \case `modusPonens` true

-- after changes
axiom :: ∀ a. Proof a
axiom = fix id <$> true
axiom = \case <$> true