natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
hom-set, hom-object, internal hom, exponential object, derived hom-space
loop space object, free loop space object, derived loop space
In a cartesian closed category/type theory , given any object/type there is a monad
given by forming the internal hom out of , hence the βspace of functionsβ out of . 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 (an βenvironmentβ).
The reader monad does not generally arise from a monadic adjunction. Algebras may not be easily characterizable. When is a 2 element set, algebras correspond to idempotent semigroups, also known as rectangular bands.
In a cartesian closed category/type theory , the reader monad is right adjoint to the writer comonad .
Just as the writer comonad is canonically a monad when 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.
If the type system is even a locally cartesian closed category/dependent type theory then for each type there is the base change adjoint triple
In terms of this then the function monad is equivalently the composite
of context extension followed by dependent product.
One may also think of this as being the polynomial functor associated with the span
(Notice that the comonad obtained by composing the other way around, , is the modal operator usually called necessity.)
It makes sense to think of as producing spaces of random variables (Verdier 14) depending on possible worlds (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 and may be called necessity and possibility, respectively).
In Haskell, the traditional way to model that a program may depend on random states is to consider not the reader monad but the state monad . This allows programs not only to depend on the state , 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 but never change it, then these standard constructs may be reduced from using the state monad to using just the reader monad.
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
Last revised on January 8, 2021 at 12:50:54. See the history of this page for a list of all contributions to it.