nLab function monad

Idea

In a cartesian closed category/type theory $\mathcal{C}$, given any object/type $W$ there is a monad

$$[W,-] \colon \mathcal{C} \to \mathcal{C}$$

given by forming the internal hom out of $W$, hence the “space of functions” out of $W$. This is sometimes called the function monad. Its unit is given by sending values to constant functions with that value, and the monad operation is given by evaluating on the diagonal.

In the context of monads in computer science this monad is called the reader monad or environment monad. It serves to write programs in which all operations may “read in” a state of type $W$ (an “environment”).

Properties

Algebras

The reader monad does not generally arise from a monadic adjunction. Algebras may not be easily characterizable. When $W$ is a 2 element set, algebras correspond to idempotent semigroups, also known as rectangular bands.

Relation to the writer comonad and state monad

In a cartesian closed category/type theory $\mathcal{C}$, the reader monad $[W,-] \colon \mathcal{C}\to \mathcal{C}$ is right adjoint to the writer comonad $W\times (-)$.

Just as the writer comonad is canonically a monad when $W$ is a monoid, so the reader monad is a comonad in that case, and then it is sometimes called the “traced comonad”.

The composite of writer comonad followed by reader monad is the state monad.

In terms of dependent type theory

If the type system is even a locally cartesian closed category/dependent type theory then for each type $W$ there is the base change adjoint triple

$$\mathcal{C}_{/W} \stackrel{\overset{\sum_W}{\longrightarrow}}{\stackrel{\overset{W^\ast}{\longleftarrow}}{\underset{\prod_W}{\longrightarrow}}} \mathcal{C}$$

In terms of this then the function monad is equivalently the composite

$$\prod_W W^\ast = [W,-] \;\colon\; \mathcal{C} \longrightarrow \mathcal{C}$$

of context extension followed by dependent product.

One may also think of this as being the polynomial functor associated with the span

$$\ast \leftarrow W \rightarrow \ast \rightarrow \ast \,.$$

(Notice that the comonad obtained by composing the other way around, $W^\ast \prod_W$, is the modal operator usually called necessity.)

Relation to random variables in probability theory

It makes sense to think of $[W,-]$ as producing spaces of random variables (Verdier 14) depending on possible worlds $w\in W$ (Toronto-McCarthy 10b, slide 24).

The intuition behind the Reader monad, for a mathematician, is perhaps stochastic variables. A stochastic variable is a function from a probability space to some other space. So we see a stochastic variable as a monadic value. (Verdier 14)

you could interpret this by regarding random variables as reader monad computations. (Toronto-McCarthy 10b, slide 35)

Toronto-McCarthy 10a, 2.2, Toronto 14, 6.2 call the function monad the random variable idiom.

(While, from the perspective of modal type theory, its siblings $W^\ast \prod_W$ and $W^\ast \sum_W$ may be called necessity and possibility, respectively).

In Haskell, the traditional way to model that a program may depend on random states $w \in W$ is to consider not the reader monad but the state monad $[W,W \times (-)]$. This allows programs not only to depend on the state $w\in W$, but also to change it (for instance to a new number generated by a random number generator). If however one restricts attention to programs that just depend on/read in a random environment $w\in W$ but never change it, then these standard constructs may be reduced from using the state monad to using just the reader monad.

Related concepts

• maybe monad

• continuation monad

• writer comonad, state monad

References

• Wikipedia, Environment monad.

• Neil Toronto, Jay McCarthy, From Bayesian notation to pure Racket, via measuretheoretic probability , in Implementation and Application of Functional Languages, 2010 (web)

• Neil Toronto, Jay McCarthy, From Bayesian Notation to Pure Racket, talk notes 2010 (pdf)

• Neil Toronto, Useful Languages for Probabilistic Modeling and Inference, PhD Thesis, 2014 (pdf, slides)

• Olivier Verdier, The Reader and Writer Monads and Comonads, 2014

A treatment of opacity in linguistics via the function monad

• Gianluca Giorgolo, Ash Asudeh, Monads as a Solution for Generalized Opacity, paper

• Gianluca Giorgolo, Ash Asudeh, Perspectives, Semantics and Pragmatics, vol. 9, paper