nLab function monad



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Mapping space



In a cartesian closed category/type theory π’ž\mathcal{C}, given any object/type WW there is a monad

[W,βˆ’]:π’žβ†’π’ž [W,-] \colon \mathcal{C} \to \mathcal{C}

given by forming the internal hom out of WW, hence the β€œspace of functions” out of WW. 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 WW (an β€œenvironment”).



The reader monad does not generally arise from a monadic adjunction. Algebras may not be easily characterizable. When WW 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,βˆ’]:π’žβ†’π’ž[W,-] \colon \mathcal{C}\to \mathcal{C} is right adjoint to the writer comonad WΓ—(βˆ’)W\times (-).

Just as the writer comonad is canonically a monad when WW 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 WW there is the base change adjoint triple

π’ž /W⟢∏ W⟡W *βŸΆβˆ‘ Wπ’ž \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

∏ WW *=[W,βˆ’]:π’žβŸΆπ’ž \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

*←Wβ†’*β†’*. \ast \leftarrow W \rightarrow \ast \rightarrow \ast \,.

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

Relation to random variables in probability theory

It makes sense to think of [W,βˆ’][W,-] as producing spaces of random variables (Verdier 14) depending on possible worlds w∈Ww\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 *∏ WW^\ast \prod_W and W *βˆ‘ WW^\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∈Ww \in W is to consider not the reader monad but the state monad [W,WΓ—(βˆ’)][W,W \times (-)]. This allows programs not only to depend on the state w∈Ww\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∈Ww\in W but never change it, then these standard constructs may be reduced from using the state monad to using just the reader monad.


A treatment of opacity in linguistics via the function monad

Last revised on January 8, 2021 at 12:50:54. See the history of this page for a list of all contributions to it.