We show how to program with the law of excluded middle. We specifically avoid call/cc, which is overrated.
NOT NOT A -> A
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)) -> aWe 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))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.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) > -- 42We 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).
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 bWe 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, alphawhere
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.
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML