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

_{0}, x

_{1}, ...)}

We need to define ε

_{X}(

`extract`

and Δ_{x}(

`duplicate`

).ε

_{X}can be defined like this: ε

_{X}(x

_{0},...) is x

_{0};

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

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

`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:

Post a Comment