Comonad
A monad puts values into a context with return and chains functions . A comonad does the reverse: it takes values out with extract and extends functions , which compute one value from a whole context, to the context as a whole[1][7].
Definition
A comonad on a type constructor has two operations:
Equivalently, a comonad has duplicate : , which replaces each position with the whole context focused there, and extend f = map f . duplicate.
Laws
The laws are the duals of the monad laws[1]:
Example: cellular automata
A zipper, a structure with one position in focus, is a comonad: extract reads the focus, and extend f computes f with the focus moved to each position in turn. A rule of an elementary cellular automaton is a function from a cell's neighbourhood to its next state, that is, a function , and one generation is extend of it[3].
A ring of cells as a comonad in OCaml, rule 30, and a check of the laws.
module type COMONAD = sigtype 'a tval extract : 'a t -> 'aval extend : ('a t -> 'b) -> 'a t -> 'b tend(* A ring of cells with one in focus: a zipper whose ends wrap around. *)module Ring = structtype 'a t = { cells : 'a array; focus : int }let extract w = w.cells.(w.focus)(* Apply f with every cell in focus in turn. *)let extend f w = { w with cells = Array.init (Array.length w.cells) (fun i -> f { w with focus = i }) }let duplicate w = extend Fun.id wlet at w d = let n = Array.length w.cells in w.cells.((w.focus + d + n) mod n)end(* An elementary cellular automaton is a function from a neighbourhood toa cell, so one generation is extend of it. *)let rule n w =let bit b = if b then 1 else 0 inlet k = 4 * bit (Ring.at w (-1)) + 2 * bit (Ring.extract w) + bit (Ring.at w 1) in(n lsr k) land 1 = 1let show w = String.init (Array.length w.Ring.cells) (fun i -> if w.Ring.cells.(i) then '#' else '.')
Running it.
...............#.............................###...........................##..#.........................##.####.......................##..#...#.....................##.####.###...................##..#....#..#.................##.####..######...............##..#...###.....#.............##.####.##..#...###...........##..#....#.####.##..#.........##.####..##.#....#.####....extend extract = id: trueextract (extend f w) = f w: trueextend f . extend g = extend (f . extend g): trueduplicate has 5 rings of 5 cells
The rule never mentions positions or indices: it only reads the focus and its two neighbours, and extend supplies every focus. The ring wraps around, so the pattern would eventually meet itself.
Other comonads
The pair is the environment comonad, a value with read-only context. Non-empty lists and streams are comonads whose extend sees each suffix, which models computations over a history such as moving averages[1]. The store comonad, a function together with a position , underlies lenses: a lens is a coalgebra of the store comonad[6]. Orchard and Mycroft proposed a do-like notation for comonads[2], and Haskell's comonad package provides the class and these instances[5].
History
Comonads, under the name cotriples, appear in category theory alongside monads from the 1960s[7]. Uustalu and Vene developed comonads as notions of computation, dual to Moggi's monads, in the 2000s[1]. Piponi's 2006 post showing that cellular automata are comonadic popularized the idea among Haskell programmers[3]. Rule 30 is one of the elementary cellular automata Wolfram studied in 1983[4].
see also
- MonadIn functional programming, a monad is a type constructor m with two operations, return : a -> m a and bind : m a -> (a -> m b) -> m b, satisfying three laws. It lets code with some extra behaviour, such as failure, several results, configuration, state or I/O, be written as a sequence of ordinary steps, with the behaviour defined once in bind. The notion comes from category theory.
- ZipperA zipper represents a data structure together with a focus, a position inside it: the substructure at the focus, and the path from the focus back to the root together with everything to either side of that path. Moving the focus one step and editing at the focus take constant time, and the structure is persistent, so edits share everything off the path. The type of paths is the derivative of the structure's type, in the sense of calculus.
- LensA lens is a first-class pair of a getter and a setter for one part of a structure, with laws that make them agree: you get back what you set, setting what you got changes nothing, and a second set overwrites the first. Lenses compose, so a path through nested immutable records is one value that can read or update the part at its end. They originated in work on the view-update problem, and in Haskell are usually encoded as functions polymorphic in a functor, which makes composition ordinary function composition.
further reading
- [1]T. Uustalu, V. Vene, “Comonadic notions of computation”, Electronic Notes in Theoretical Computer Science 203 (2008).
- [2]D. Orchard, A. Mycroft, “A notation for comonads”, IFL (2012).
- [3]D. Piponi, “Evaluating cellular automata is comonadic”, blog post, A Neighborhood of Infinity (2006).
- [4]S. Wolfram, “Statistical mechanics of cellular automata”, Reviews of Modern Physics 55 (1983).
- [5]E. Kmett, the comonad package for Haskell, Control.Comonad.
- [6]J. Gibbons, M. Johnson, “Relating algebraic and coalgebraic descriptions of lenses”, Electronic Communications of the EASST 49 (2012).
- [7]S. Mac Lane, Categories for the Working Mathematician, ch. VI, Springer (1971).
last updated