[TYPES] Constructive Law of Excluded Middle

[oleg@okmij.org]

Continuing the discussion of teaching constructive proofs by
contradiction, we show how to program with the law of excluded
middle. We specifically avoid call/cc, which is overrated.

Proofs by contradiction are not exclusive to classical logic. For
example, weak reductio -- proving the negation of a proposition A by
assuming A and exhibiting a contradiction -- is intuitionistically
justified. Constructively, to prove the negation of A one has to build
a witness of the type A->F where F is a distinguished type with no
constructors. Strong reductio -- proving A by contradiction with the
assumption of NOT A -- is equivalent to the implication 
NOT NOT A -> A, or ((A->F)->F) -> A. This implication is equivalent
to the law of excluded middle (LEM) (which can be shown by negating
the law of contradiction) and is certainly not intuitionistically
or constructively justified.

It might be surprising therefore that one can still write a 
non-divergent Haskell term whose type is isomorphic to
   forall a. ((a->F)-F) -> a
To be precise, the type is
   forall a. (forall m. Monad m => ((a -> m F) -> m F)) -> a
We will argue how all this isn't quite the double-negation translation
and how call/cc and the related Cont monad can be avoided.  In fact,
call/cc is an overkill for the computational version of LEM.  But
first, a few preliminaries.

> {-# LANGUAGE EmptyDataDecls, Rank2Types #-}
> module LEM where
> import Control.Monad.Identity
>
> data F -- no constructors

We should justify that a function of the type 
forall m. Monad m => t1 -> m t2 is just as pure as the function
t1 -> t2. (Meta-variable t denotes some type).  The key is the universal
quantification over m. Informally, a term of the type (forall m. Monad
m => m t) cannot have any effect because types of that form can only 
be introduced by `return'.  More precisely,
     forall m. Monad m => m t        is isomorphic to t
     forall m. Monad m => t1 -> m t2 is isomorphic to t1 -> t2, etc.
One direction of the isomorphism is easy to show, for example

> purify :: (forall m. Monad m => ((a -> m b) -> m b)) -> ((a->b)->b)
> purify f = \k -> runIdentity (f (return . k))

To show the other direction, we traverse a term, inserting
return before each constant or variable and replacing applications with
flip bind, aka (=<<). Thus, if a proof term for the proposition 
(NOTNOT a) isn't already in the form 
(forall m. Monad m => ((a -> m F) -> m F)), we can always make it so.


As the second preliminary, we introduce a Sum type and make it an
instance of Monad. We could have used the built-in Either type
(however, its MonadError instance needs an Error constraint, which
gets in the way).

> data Sum a b = L a | R b
> instance Monad (Sum e) where
>     return = R
>     R x >>= f = f x
>     L x >>= f = L x


We are now ready to demonstrate the proof term for the proposition
(NOT NOT a -> a).

> h :: (forall m. Monad m => ((a -> m F) -> m F)) -> a
> h g = case g (\x -> L x) of
>         R x -> error "Not reachable"
> 	  L x -> x


One may be concerned about the `error' function (which can be replaced
by any divergent term, e.g., undefined). We can prove however that
the case R x is never taken, and so no divergence actually occurs.  If
the function g ever invokes its argument, an `exception' (the L
alternative of Sum) is raised, which propagates up. The function g,
whose type is polymorphic over m, has no way to intercept the
exception. Hence, the L case will be taken in the function h. The R
case can only be taken if g can return a value without invoking its
argument. That is not possible however since no value of the type F
can be constructed.

We will demonstrate the strong reductio later; for now we show a
simple illustration. First, we introduce

> -- A proof term for a -> NOT NOT a
> lift :: forall a m. Monad m => a -> ((a -> m F) -> m F)
> lift x = \k -> k x

Then 
 *LEM> h $ lift "forty-two"
 "forty-two"

In fact, we can show that h (lift x) evaluates to x for all x.

One may ask if our constructive strong reductio works only for atomic
proposition or for all propositions. If the proposition is an
implication, one could try to be clever, defining

> t3 k = k (\() -> k return >> return ())

Note the non-linear use of k. The evaluation h t3 will bind k to
(\x -> L x) and so the `exception' L will `leak out' of
h. Fortunately, this clever cheating does not work, again because of
the polymorphism over m. The inferred type of t3 is
  t3 :: (Monad m) => ((() -> m ()) -> m a) -> m a
and hence the application h t3 is ill-typed because `Quantified type
variable `m' escapes'. The type system ensures that the result of h
has a pure type (or isomorphic to a pure type), and so does indeed
denote a proposition.

We now show how to obtain a proof term that represents LEM directly.
We represent the disjunction in LEM in its elimination form (that
is, Church-encoded). We show two versions, without or with currying:

> lem :: (forall m. Monad m => (a -> m w, (a -> m F) -> m w)) -> w
> lem sum = case neg (\x -> L x) of
> 		  R y -> y
> 		  L y -> case pos y of
> 			   R z -> z
> 			   L _ -> error "unreachable"
>   where (pos,neg) = sum


> lem1 :: (forall m. Monad m => (a -> m w)) ->
> 	  (forall m. Monad m => (a -> m F) -> m w) -> w
> lem1 pos neg = case neg (\x -> L x) of
> 		  R y -> y
> 		  L y -> runIdentity $ pos y


No matter what 'a' is, we can always produce either it or its
negation. Here is a more interesting illustration:

> ex_falso_quodlibet :: F -> a
> ex_falso_quodlibet falsum = h (\k -> return falsum)

> tlem  = lem (return, \k -> ex_falso_quodlibet =<< k 42)
> -- 42
> tlem1 = lem1 return (\k -> ex_falso_quodlibet =<< k 42)
> -- 42

We have just proven the existence of 42 by contradiction, using
strong reductio.

Our terms lem and lem1 are not in the image of the double-negation
translation of (A + NOT A). Indeed, the double-negation translation of
the latter is NOTNOT (NOT A + NOT NOT A), which is
    ((Either (a -> F, (a->F)->F))->F)->F
This is different from the type of our lem and lem1. Applying Glivenko
theorem directly to (A + NOT A) gives
    NOT (NOT a & NOTNOT a), or
    (a->F, (a->F)->F) -> F
which is again different from the type of our lem and lem1.

Furthermore, although our terms h and lem have `classical' types, we
remain within constructive logic. The term h is total, but the
function g may not necessarily be so. We know that if g ever
invokes its argument (that is, it constructed an object of the type
a), then (h g) does produce that object. NOTNOT A does imply A in this
case. The function g cannot return without invoking its argument. But
the function g may diverge before invoking its argument. We have thus
confirmed the old result that LEM is intuitionistically justified for
decidable propositions.

We stress that we have never used the continuation monad. Our monad
Sum is much weaker: it does not permit one to restart an exception,
let alone restart the exception multiple times. It seems we can do a
lot without call/cc. This subject is elaborated in 
Limit-Computable Mathematics (LCM).