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
The state monad is a monad (in computer science) used to implement computational side-effects in functional programming.
A functional program with
output of type
and “mutable state” of type
(e.g. the state of a “random access memory” device, cf. Yates (2019), p. 26 & Fig. 1.10)
is clearly a function (morphism) of function type betwen the product types with :
Now, under the hom-isomorphism of the (Cartesian product internal hom)-adjunction, this is equivalently given by its adjunct, which is a function into the function type (internal hom):
Here the operation is the monad on the type system which is induced by the above adjunction; and this latter function is naturally regarded as a morphism in the Kleisli category of this monad.
In the context of monads in computer science, this monad is called the state monad for mutable states of type .
In a locally Cartesian closed category/dependent type theory , then to every type is associated its base change adjoint triple
In terms of this the state monad is the composite
of context extension followed by dependent sum, followed by context extension, followed by dependent product.
Here is called the function monad or reader monad and is the coreader comonad.
function monad (reader monad)
The abstract notion of the state monad:
Concrete applications via implementation in Haskell:
Lecture notes:
In the generality of the local state monad:
Paul-André Melliès, Local States in String Diagrams, In: G. Dowek (eds.) Rewriting and Typed Lambda Calculi RTA TLCA 2014, Lecture Notes in Computer Science 8560, Springer (2014) [doi:10.1007/978-3-319-08918-8_23]
Last revised on November 3, 2022 at 17:02:39. See the history of this page for a list of all contributions to it.