When I find something interesting and new, I post it here - that's mostly programming, of course, not everything.

Monday, August 31, 2009

a sample comonad

Comonads still look a little bit enigmatic to programmers; I'm going to show a practical example from which one can start perceiving the notion.

First, definition. A comonad is dual to monad; which may or may not be a good explanation. So, okay, a formal definition.

A comonad is a functor T: AA

εx: T(x) → x


Δx: T(x) → T(T(x))

together with three conditions similar to monadic conditions:

a) For Δx: T(x) → T(T(x)) and εT(x): T(T(x)) → T(x) we should have εT(x) ° Δx = IdT(x)

b) For Δx: T(x) → T(T(x)) and T(εx): T(T(x)) → T(x) we should have T(εx) ° Δx = IdT(x)

c) For Δx: T(x) → T(T(x)), ΔT(x): T(T(x)) → T(T(T(x))), T(Δx): T(T(x)) → T(T(T(x))) we should have T(Δx) ° Δx = ΔT(x) ° Δx

Here's a nice compact comonad implementation in Haskell; I hope the author won't mind my quoting the code:

class Functor w => Comonad w where
extract :: w a -> a
duplicate :: w a -> w (w a)
extend :: (w a -> b) -> w a -> w b

So, in this notation, the axioms will look like this:

extract . duplicate == id
fmap extract . duplicate == id
duplicate . duplicate == fmap duplicate . duplicate

The author of the code also specifies axioms for extend, but I find it superfluous; it is enough to have functoriality and the comonad laws actually.

I wanted to bring a good example of comonad. Here how one could be produced.

If we have a monoid M, we can have a comonad of functions from a given M to sets. A monoid is a... okay, a set that has associative multiplication and unit defined: 1: → M, m: M×M → M, such that m(a, 1) = m(1, a) = a.

So, let's take the functor which to each set X maps a set of functions from a given monoid M to X. It is known to be a functor; now, how come functions from a monoid to a set form a comonad? I would not go into details here, and will just demonstrate how we have a comonadic structure for one specific monoid, ℕ, the monoid of natural numbers: [0..∞).

So what we have is a functor that, given a set X, builds the set of all sequences in X. I plan to demonstrate that this functor is a comonad.

X ↦ {(x0, x1, ...)}

We need to define εX (extract and Δx (duplicate).

εX can be defined like this: εX(x0,...) is x0;

Why so? A general definition of extract for the case of monoid is taking f(0) for a function f: M → X (a composition 1 → M → X ).

and Δx can be defined like this: Δx(xi,j) = xi+j

Again, this is because T(T(X)) in our case is the set of functions M → M → X, which is equivalent to the set of functions from M×M → X. For each f: M → X we can define M×M → M → X by composing the monoid multiplication (which is addition if we are talking about natural numbers) and f.

Or, in other words, duplicate (x0, x1, ...} == ((x0, x1, ...), (x1, x2, ...), ...); (extract . duplicate) (x0, x1, ...) will return the first element, (x0, x1, ...), that is, it is the same as id.

If we apply fmap extract to ((x0, x1, ...), (x1, x2, ...), ...), we will get a sequence of first elements of each sequence, that is, again, (x0, x1, ...).


In my view, Haskell community, probably for the sake of being closer to the people, oversimplifies IO.

In my view, while output is a monad, input can be interpreted as a comonad. When a machine is taking input, it has no control over external environment, it just consumes; the input acts on the machine. To make the input comonad look like a monad, the authors use tricks, forcing the whole evaluation happen inside not the main Haskell category, but its image under a certain functor... but I don't think this is the right place and time to discuss adjoint functors here.

No comments:


Subscribe To My Podcast