previous  next  contents  top

Constructive Law of Excluded Middle


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.
The first part of this message was posted on the TYPES mailing list on Wed, 9 Sep 2009 19:15:05 -0700 (PDT).
I'd like to thank Jacques Carette and Russell O'Connor for helpful discussions.



     > {-# 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))
The other direction is explained in the Appendix, which contains further justifications. Thus, if a proof term for the proposition NOT NOT A is not 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
      *LEM> h $ lift "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 ())
with 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.


Proof term for LEM

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 and 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 proved 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.



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).

Susumu Hayashi: Proof Animation and Limit Computable Mathematics home page
< >


Purity and effect-polymorphism

We now 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). We call (->) a pure arrow, and introduce the notation (:->) for the effectful but effect-polymorphic arrow:

     > type a :-> b = forall m. Monad m => a -> m b
We claim that the two arrows are inter-convertible. Given a term e1 in the lambda-calculus with sums, products and monads whose type contains a pure arrow, we can derive a term e2 whose type has (:->) in place of (->). Conversely, if a term e2 has the type with (:->) we can derive e3 with the same type modulo the replacement of (:->) with the pure arrow. Furthermore, if e3 is the result of `round-tripping' -- transforming the effect-polymorphic e2 that is the result of transforming a pure e1 -- there are no contexts that can distinguish e1 from e3.

We start with simple examples:

     > tt2 :: (a -> b) -> a -> b
     > tt2 = \f -> \x -> f x
     > -- Translation:
     > tt2M :: (a :-> b) :-> (a :-> b)
     > tt2M = \f -> return (\x -> f x)
     > -- or, after applying a monad law:
     > tt2M' = \f -> return (\x -> f =<< (return x))
     > -- Recovering tt2 from tt2M:
     > app :: Monad m => m (a :-> b) -> m a -> m b
     > app f x = do {fv <- f; xv <- x; fv xv}
     > tt2R :: (a -> b) -> a -> b
     > tt2R = \f x -> runIdentity $ (tt2M (\x -> return (f x)) `app` (return x))
A more complex example of the transformation and recovery:
     > tt3 :: ((a->b) -> c) -> b -> c
     > tt3 f b = f (const b)
     > tt3M :: ((a :-> b) :-> c) :-> (b :-> c)
     > tt3M f = return (\b -> f (const (return b)))
     > pure_rev :: (a :-> b) -> (a -> b)
     > pure_rev f = \a -> runIdentity (f a)
     > tt3R :: ((a->b) -> c) -> b -> c
     > tt3R = \f b -> runIdentity $ 
     >           tt3M (\ab -> return (f (pure_rev ab))) `app` (return b)
An interesting example suggested by Russell O'Connor:
     > t1 :: ((((b -> a) -> b) -> b) -> F) -> F
     > t1 = \f -> f (\s -> s (ex_falso_quodlibet . (f . const)))
     > -- or, in the pointed form
     > t1' :: ((((b -> a) -> b) -> b) -> F) -> F
     > t1' = \f -> f (\s -> s (\y -> ex_falso_quodlibet (f (const y)) ))
     > -- Transformation:
     > t1M :: ((((b :-> a) :-> b) :-> b) :-> F) :-> F
     > t1M = \f -> f 
     >          (\s -> s (\y -> (return ex_falso_quodlibet) `ap` 
     >                                    (f (const (return y))) ))
     > -- Recovery:
     > up :: ((b -> a) -> b) -> ((b :-> a) :-> b)
     > up s = \ba -> return (s (pure_rev ba))
     > t1R :: ((((b -> a) -> b) -> b) -> F) -> F
     > t1R f = runIdentity $ t1M (\zM -> return (f (\s -> runIdentity (zM (up s)))))
The transformation is simple and type-directed. To replace a pure arrow with (:->), we have to traverse the term inserting return and monadic applications. The transformation in the other direction is a wrapper transformation using the Identity monad. The latter transformation does not need the term in the source form.

It helps to think of the transformations in terms of an effect system. Each pure function t1 -> t2 can also be regarded an effectful function t1 ->{m} t2 polymorphic over effects m. The conversion from (->) to (:->) is automatic then. To be more precise, the conversion of a term whose type has (->) into a term whose type has (:->) instead is an implicit coercion -- the operational identity. For example, Asai/Kameyama (APLAS 2007) calculus for shift/reset, which is an effect system calculus, has the injection rule:

     Gamma |-p e : t
     Gamma, alpha |- e: t, alpha
where alpha is the answer-type (the effect annotation, essentially). If the term e judged to be pure with the type t, the very same term can be judged effectful for any answer-type alpha. In effect systems, the isomorphism between pure and effect-polymorphic terms is intensional.

The connection between effect-polymorphism and the absence of control effects has been investigated by several people, in particular, Hayo Thielecke.

Hayo Thielecke: From Control Effects to Typed Continuation Passing. POPL 2003.
< >

Last updated October 4, 2009

This site's top page is
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML