Friday, 30 January 2015

Life by Comonads: 1


Why did the chicken cross the Mobius Strip? 
 - To get to the same side

Prepping the Intuition

Comonads are the categorical duals are monads. So it pretty much means we have to reverse the notions that persist related to monads.

Well, from a computational perspective, monads allow us to:
  • Execute actions using  some input, producing an output wrapped in a context. Functions of the form a -> m b
  • Allow us to use the results of previous computations as inputs to further actions that produce some more context and subsequently resolve the nested contexts into a single context (>>=), in a sensible manner; for a sequence of actions the order in which we resolve the contexts is irrelevant a.k.a. the monad laws.

Thus in some sense the opposite of the above intuitions gives: 
  • Comonads allow us to consume values wrapped in a context producing some output, values for the form (w a -> b)
  • Duplicate a context and extract a value from the inner context such that using extract on the inner context yeilds the original comonadic value:   A function of the form = (w a -> b) -> w a -> w b
  • We invert the 'm' to get a 'w' for type-constructor variables

Comonad Instances

Looking at the source we see that (e,) and ((->) m) are instances of the Comonad class. 
Now that's the writer and the reader monads except the Monoid constraint is required of the 'reader' comonad.

Let's go ahead and implement them:
instance Comonad (e,) where
  extract (_, a) = a
  duplicate (e, a) = (e, (e, a))
  extend (e, a) f = (e, f (e, a))

The (e,) comonad carries around an e with it. When extracting a value we simply ignore the environment. 
Duplicate, duplicates the environment. But thats exactly what the reader monad does, but in a somewhat opposite sense. That oppositeness is clarified on reversing the arrows for the respective functions.
return' :: a -> r -> a
return' :: a -> r -> a
return' :: r -> a -> a
return' :: (r, a) -> a
extract :: (r, a) -> a

(>>=)' :: m a -> (a -> m b) -> m b
(>>=)' :: w b -> (w b -> a) -> w a
extend :: w b -> (w b -> a) -> w a

While this probably shouldn't be surprising, one has to admire the magnificent machinery of category theory. Something as innocent as looking the other way has divine repercussions. 

Armed with that knowledge we're going in to Monoid m => ((->) m), expecting a Writer monad like behavior. 

instance Monoid m => Comonad ((->) m) where
  extract f = f mempty
  duplicate m f = \w -> \w' -> f (w <> w')
  extend m f = \w -> f (\w' -> m (w <> w'))

Sure enough, we see the same sort've writing behavior but with more emphasis on viewing the result than accumulating. 


So that's pretty cool, reading and writing are duals of each other and in some sense opposite notions which is made formal by their representation as mathematical objects. I always find it fascinating to see mathematics - a pure and exact - describe something I thought was really vague, though granted in the projection we loose some nuances of the concepts.

So while that's helped my understanding of the duality between monads and commands, comonads haven't distinguished themselves apart from being interesting theoretical specimen. They simply appear to be the other side of the same strip. 

Next up, we move on to a real Life algorithm.

No comments:

Post a Comment