But What IS a Monad?
This is an article that defines what a Monad while trying to stay as close as possible to its roots in Category Theory.
If you've ever heard of monads in the context of functional programming, you've likely also heard that they are just "Monoids in the Category of Endofunctors". But what does that even mean?
Well for one, this quote could use some more detail. The more descriptive quote is: "a monad in is just a monoid in the category of endofunctors of , with product replaced by composition of endofunctors and unit set by the identity endofunctor."
Throughout this article, we will define "Category", "Endofunctor" and "Monoid" in a fictional programming language, and put these definitions together to define a Monad.
A Category (designated using curly letters, i.e. ), for the purposes of this article, is simply some defined set of mathematical objects (numbers, values, types, terms, or even categories themselves) as well as some set of "morphisms" defined between the objects. A category also has some conventions such as:
- Every object has a morphism to itself (called the identity morphism)
- Morphisms can be combined together into other morphisms much like function composition.
- Morphism composition is associative.
Functors in category theory are simply morphisms in a "category of categories". Where categories are objects and functors are just morphisms that map one category to another. This can be visualized at either a high level of abstraction where the functor is just one arrow between two categories (). Or at a lower level where a functor could be represented as many parellel arrows uniquely mapping every object and morphism in category to an object or morphism in category .
Endofunctors are just the special case where the two categories and are the same category. Endofunctors are essentially just a mapping between each object and morphism in a category to another object/morphism in the same category.
Endofunctors come up often when working in a specific Categories. For example all the types in a programming language, form a category, where the morphisms are functions defined between them. This category is called Type
, and can be thought of as the "type of types".
There are many programming languages that have endofunctors. Option
in Rust, Maybe
in Haskell, or really any kind of wrapper type in any language is technically an endofunctor. While most languages have endofunctors, most don't have a powerful enough type system to formalize the definition of endofunctors itself. (For rustaceans, think of it like a trait
that you can implement for type constructors like Option
or Vec
, not Option<T>
, just Option
by itself. this is not yet possible in rust at the time this article was written).
When defining what it means to be an Endofunctor formally within a given Category of objects (i.e. a Type System), one needs a powerful dependently-typed lagnuage. For the purposes of this article, we will be using a fictitious dependently-typed language. The following is an outline of some of the general features of the language.
Pseudocode Definitions (skip this if you think you can grok the psuedocode first try):
# If you are used to haskell-based currying the first two definitions of `Likelyhood` would be similar to providing two constructors for the same object like the following: Likelyhood_a : Num -> Float -> Likelyhood Likelyhood_b : Float -> Num -> Likelyhood # But the 3rd definition would only be equivalent to Likelyhood_a
Okay now that we have pseudocode out of the way, we can get to defining an endofunctor :D
In this language, Endofunctors can be defined as a dependent collection of two functions: obj_map: A -> F<A>
which maps the object of the category, and a function func_map
that takes an arbitrary function A -> B
where B
can be anything and returns a function F<A>
-> F<B>
, mapping the morphisms from the initial object. When this definition is used as a "type class" (think trait
or interface
), it allows the user to abstract over a specific endofunctor definition and refer to all endofunctors as a collective.
Examples of various type constructors and specifications (implementations) of the Endofunctor class.
NOTICE: New Syntax / Convention, identity
is the name assigned to the expression [T] [v] v
. But that expression has also been associated with a type ([T : Type] [T] T
). The type of identity
is automatically assigned the name (translated from snake_case to PascalCase): ^Identity
.
There is analogous syntax for finding a value defined for a given type. This may not always resolve because multiple values could be defined for a given type.
Example: to refer to impl_option_endofunctor, you can instead infer the definition via: _ : Endofunctor(Option)
.
This also works when defining "implementations". You can use _
to not define a name, and instead let type inference do its job.
OKAY, Now we can get back to defining the Monad! According to category theory, a monad in a category is a monoid in the category of endofunctors of some other category. We know what endofunctors are, what what is a Monoid?
Wikipedia describes a monoid (the algebraic version) as an set () equipped with a binary operation we will call "multiplication" () and particular member of the set called the "unit".
To translate this into a typed programming language, we will define a monoid as a type class (a.k.a. trait / interface) that can be implemented for objects. The definition of the type class is parameterized on the set and includes a set of two morphisms, unit and multiplication as well as the two monoid laws of associativity and identity: , and
Now that we have a monoid, we can talk about types that are monoids! (Assume Nat
is the type of natural numbers)
Alright lets do another one! This time on a type we've actually seen before (I'll add type annotations for unit and multiplication so its more clear what is going on here)
Oh wait, since Option
is a endofunctor, isn't this just a Monad? (A monad is a monoid defined on an endofunctor after all) Lets try and pinpoint a more exact definition of a Monad :)
If you followed all that, You should now have a good understanding of what a Monad is! (Specifying it is essentially the same as a monoid above)