Contents

# Contents

## Idea

The store comonad (also costate comonad) is a comonad (in computer science) used to implement computational storage and retrieval of data in functional programming.

As a comonadic triple $(D,\varepsilon,\delta)$ it is given by an endofunctor,

$DX : X \rightarrow W \times [W,X],$

with natural transformations the counit,

$\varepsilon : DX \rightarrow Id_X$
$\varepsilon(v,f) \mapsto f(v),$

usually called extract and comultiplication,

$\delta: DX \rightarrow DDX$
$\delta (s, v) \mapsto (s, \lambda s' . (s', v)),$

simply called duplicate.

## Properties

### Realization in dependent type theory

In a locally Cartesian closed category/dependent type theory $\mathbf{H}$, then to every type $W$ is associated its base change adjoint triple

$\mathbf{H}_{/W} \stackrel{\overset{\sum_W}{\longrightarrow}}{\stackrel{\overset{W^\ast}{\longleftarrow}}{\underset{\prod_W}{\longrightarrow}}} \mathbf{H} \,.$

In terms of this the store comonad is the composite

$Store = \sum_W W^\ast \prod_W W^\ast$

of context extension, followed by dependent product , followed by context extension, followed by dependent sum.

Here $\prod_W W^\ast = [W,-]$ is called the function monad or reader monad and $\sum_W W^\ast = W \times (-)$ is the writer comonad.

## Reference

Last revised on August 24, 2018 at 11:13:47. See the history of this page for a list of all contributions to it.