# Constructive Law of Excluded Middle

We show how to program with the law of excluded middle. We specifically avoid call/cc, which is overrated.

## Introduction

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

## Preliminaries

```     > {-# LANGUAGE EmptyDataDecls, Rank2Types #-}
> module LEM where
>
> 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
```

## `NOT NOT A -> A`

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

## Conclusions

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

References
< http://www.shayashi.jp/PALCM/ >

## 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`.

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

References
Hayo Thielecke: From Control Effects to Typed Continuation Passing. POPL 2003.
< http://www.cs.bham.ac.uk/~hxt/research/effects.pdf >

### Last updated October 4, 2009

This site's top page is http://okmij.org/ftp/

oleg-at-okmij.org