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: A → A

ε_x: T(x) → x

and

Δ_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 = Id_T(x)

b) For Δ_x: T(x) → T(T(x)) and T(ε_x): T(T(x)) → T(x) we should have T(ε_x) _° Δ_x = Id_T(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 ↦ {(x₀, x₁, ...)}

We need to define ε_X (extract and Δ_x (duplicate).

ε_X can be defined like this: ε_X(x₀,...) is x₀;

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(x_i,j) = x_i+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, ...).

Conclusion

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.