|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|classical type theory?||internal logic||classical type theory?, logic programming?|
|cut elimination?||counit||beta reduction|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
In computer science, a monad describes a “notion of computation”. Formally, it is a map that
Monads provide one way to “embed imperative programming? in functional programming”, and are used that way notably in the programming language Haskell. (But monads, as well as comonads and related structures, exist much more generally in programming languages; an exposition is in (Harper)).
For instance when the monad forms product types with some fixed type that carries the structure of a monoid, then a Kleisli function may be thought of as a function that produces a “side effect” output of type . The Kleisli composition of two functions and then not only evaluates the two programs in sequence but also combines their -output using the monoid operation of ; so if and then the final result of will be . For example, might be the set of strings of characters, and the monoid operation that of concatenation of strings (i.e. is the free monoid on the type of characters). If the software is designed such that values of type computed in this way appear on the user’s screen or are written to memory, then this is a way to encode input/output in functional programming (see the IO monad? below).
But monads have plenty of further uses. They are as ubiquituous (sometimes in disguise) in computer science as monads in the sense of category theory are (sometimes in disguise) in category theory. This is no coincidence, see Relation to monads in category theory below.
Here the morphism in the middle of the last line makes use of the fact that is indeed a functor and hence may also be applied to morphisms / functions between types. The last morphism is the one that implements the ”-computation”.
The monads arising this way in computer science are usually required also to interact nicely with the structure of the programming language, as encoded in the structure of its syntactic category; in most cases, terms of the language will be allowed to take more than one input, so the category will be at least monoidal, and the corresponding kind of ‘nice’ interaction corresponds to the monad’s being a strong monad.
When monads are defined in Haskell, the Kleisli composition (called ‘bind’) is defined in Haskell. So monads in Haskell are always enriched monads, according to the self-enrichment defined by the function type in Haskell.
Equipping homotopy type theory (say implemented as a programming language concretely in Coq or Agda) with two axiomatic idempotent monads, denoted and , with some additional data and relations, turns it into cohesive homotopy type theory. See also modal type theory.
Another approach to modelling side effects in functional programming languages are
The original reference for monads as ‘notions of computation’ is
Expositions are in
The specification of monads in Haskell is at