The Option monad -- in fact, all of the standard container monads that have an empty structure (like the None in Option) -- are *intuitionistic*. What do i mean by that? i mean there is a canonical interpretation of the monad as a kind of negation without an excluded middle. Without the jargon we can understand this as follows. We know that the type A => Option[Option[A]] always has an inhabitant: here's an implementation

- def optSqrd [A] ( a : A ) : Option[Option[A]] = Some(Some( a )) // note that there are a lot more, for example
- def halfOptSqrd [A] ( a : A ) : Option[Option[A]] = if (scala.math.random > .5) { Some( if scala.math.random > .5 { Some( a ) } else { None } ) else { None }

However, the type Option[Option[A]] => A is not guaranteed to have an inhabitant. Either the inner or the outer Option may be None and so we may simply not be able to produce the A. More generally, for any monadic container, C, that may be empty, we have a witness for A => C[C[A]] (this is just two applications of unit). However, we cannot find a reliable witness for C[C[A]] => A for the same reasons that the Option[Option[A]] => A map fails to exist. This is in exact correspondence with the failure of excluded middle in Intuitionistic Logic. In Intuitionistic Logic we may readily prove A => ~~A, but we cannot prove ~~A => A. Of course, this observation begs the question as to whether there are more correspondences to be had. Is there a case where the monad does have a kind of excluded middle or involutive negation?

The truth is that i came to write this post as i was thinking about co-monads and was looking for good examples to explain some points in the forthcoming Monadic Design Patterns for the Web. i'd forgotten -- or rather only just remembered -- that the linear exponential !(-), of Classical Linear Logic, is a paradigmatic co-monad. To see this, let's investigate its (DeMorgan) dual, ?(-), and observe its monadicity. To see that we have a unit for ?(-) consider what we require. The type of unit for this monad would be unit : A => ?A. In this setting the arrow will actually be a *linear *map, which we'll write using lollipop, - -o -; thus, in the logical world we write the type of the unit map as the formula: A -o ?A.

Similarly, in the logical world, to exhibit a map is to exhibit a *proof*. So, what we require is a *proof of the formula* A -o ?A. Here it is

|- ~A, A ( axiom)

|- ~A, ?A (dereliction)

|- ~A # ?A (par)

|- A -o ?A (defn of -o)

(Translating this back into programming terms, you won't be far off if you think of axioms as providing us a set of functions of type A => A, while the other proof rules are higher-order widgets taking functions and returning new ones. Thus dereliction will take a map m: ( A1, ..., An ) => B and return a new map dereliction( m ) : ( A1, ..., An ) => ?B, etc. The analogy is a little off because Linear Logic enjoys so many symmetries that functional programming does not.)

In a similar manner to how we derived our unit map, to see that we have a bind map we have to exhibit a proof of the formula ??A -o ?A. Here it is

|- ~A, A (axiom)

|- ~A, ?A (dereliction)

|- ?A, ~A (exchange)

|- ?A, !~A (weakening)

|- ?A, !!~A (weakening)

|- ?A, ~??A (DeMorgan)

|- ~??A, ?A (exchange)

|- ~??A # ?A (par)

|- ??A -o ?A (defn of -o)

Now, to get the co-monadic structure of !(-) we simply exchange roles in the proofs. To get co-unit, aka extract, we need to exhibit a proof !A -o A. Here it is

|- ~A, A (axiom)

|- A, ~A (exchange)

|- A, ?~A (dereliction)

|- A, ~!A (DeMorgan)

|- ~!A, A (exchange)

|- ~!A # A (par)

|- !A -o A (defn of -o)

(Notice how the structure of this proof mimics its dual -- the proof of A -o ?A -- with two exchanges judiciously inserted at key points.)

Similarly we need a proof of !A -o !!A to exhibit an interpretation of co-bind

|- ~A, A (axiom)

|- A, ~A (exchange)

|- A, ?~A (dereliction)

|- ?~A, A (exchange)

|- ?~A, !A (weakening)

|- ?~A, !!A (weakening)

|- ~!A, !!A (DeMorgan)

|- ~!A # !!A (par)

|- !A -o !!A

This gives the core of a linear monad/co-monad pair to which we may look for guidance about how to develop a deeper and more orderly investigation of monads, co-monads and data/control structure interpretations of those APIs. The linear situation with its pair of exponentials, ? and !, that are linked by a DeMorgan relation provides a monad and co-monad that are intertwined in just the right way to ensure that every request, !A, to unpack an A from a container is always hooked up to a container, ?A, that contains an A. Moreover, the linear situation is also rich enough to encode Intuitionistic Logic (and hence all the computational phenomena in the lambda calculus -- which is the foundation on which Scala is built). This gives us some clue that there might be a more general and rich underlying way to hook up monads and comonads to get much more robust, yet fine-grained views of our containers and control structures. Not to give too much away, but the monadic broker described in this post uses delimited continuations to provide exactly the same guarantees about matching up Gozintas with Gozoutas, as do the Linear Logic exponentials, yet in a non-blocking I/O Node.js-style. More on this in subsequent posts.

## 7 comments:

nice!

I did not know that

unit and join

(as well as)

co-unit and co-join

had such simple interpretations

in Linear Logic

But then again: you're

never to old to learn ...

Luc

In your first paragraph, I think the better analogy is that Option[A] itself is like double negation, rather than a single negation. Just as A implies ~~A but ~~A doesn't (intuitionistically) imply A, you have a function A => Option[A] but not Option[A] => A. That is, you don't need the Option[Option[A]].

@Luc -- thanks!

@Brian -- great observation! i tend to agree.

I do not see how option, which in a topos is just (-)~, can be considered as a double negation or, in general, a closure operation. They are nicely similar, but pretty much different.

On the other hand, the idea of dragging double negation into discourse, as, probably, other Grothendieck topologies, might be very fruitful. But there's a lot of work to be done. In any case, we have to abandon the idea of boolean logic as a foundation of everything, and get used to the fact that in types, logic is intuitionistic, and so there.

Thanks a lot for this inspiring publication!

@Vlad -- It really depends on the type and/or computational system what sort of logic works. Linear types are classical -- in the sense that the negation is involutive.

More generally, a logic/type-system can be viewed in terms of a distributive law between a pair of monads. One monad provides the (free) term language, the other provides a notion of collection. The type system shows how to canonically pull the term language through the notion of collection -- in other words how to move from collections of terms to terms of collections, in a canonical fashion.

In this set up the terms of collections are the formulae and the map turning them into collections of terms constitutes the semantics of the formula. It says what it means for a term to inhabit a formula.

This is all completely general.

I got a big laugh out of your "incorrect" use of "begs the question" in an article about logic! I presume you did this on purpose. Well, your pains were not in vain. Clever, that.

As a musician this reminds me a lot of symmetry and serialism, as a web dev it reminds me of divs and new html5 symantic elements, as a net admin it reminds me of bitmasking/subnetting, the fact that monads span all of these disciplines reinforces the magnitude of the concept of multiplicity. But which is discrete? The container's boundary coordinates or the contents of the container? Nth dimensions to consider, wonderful. Thanks for the c9 lectures, got me into scalacollider! Rawkin emacs on cygwin now, music is math :0)

Post a Comment