Gozintas and Gozoutas revisited

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.