minor styling + some writing

This commit is contained in:
Alexander 2025-06-12 12:04:01 -04:00
parent ef028bb4de
commit 3a1da22c36
5 changed files with 103 additions and 15 deletions

View file

@ -0,0 +1,44 @@
# Functors and Applicatives for Free[^falsehood]
It's usually possible to derive implementations of general structures from those of more specific ones, e.g. `Applicative` from `Monad` and `Functor` from `Applicative`. Here's how to do it and and why it's probably best avoided.
```ocaml
module type Functor = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
end
module type Applicative = sig
type 'a t
val pure : 'a -> 'a t
val apply : ('a -> 'b) t -> 'a t -> 'b t
end
module type Monad = sig
type 'a t
val return : 'a -> 'a t
val bind : ('a -> 'b t) -> 'a t -> 'b t
end
module ApplicativeOfMonad (M : Monad) :
Applicative with type 'a t = 'a M.t = struct
type 'a t = 'a M.t
let pure = M.return
let apply f x = M.(bind (fun y -> bind (fun g -> return (g y)) f) x)
end
module FunctorOfApplicative (A : Applicative) :
Functor with type 'a t = 'a A.t = struct
type 'a t = 'a A.t
let map f x = A.(apply (pure f) x)
end
module FunctorOfMonad (M : Monad) :
Functor with type 'a t = 'a M.t = struct
include FunctorOfApplicative(ApplicativeOfMonad(M))
end
```
It turns out that there are multiple ways to implement the derivation functors--- also multiple ways to implement a particular monad ---and they don't all behave the same, which means it's hard to predict whether the more-general, derived implementations are the "natural" ones that you expected to get without _ad hoc_ testing, which obviously rather defeats the point of "free".
[^falsehood]: Unsurprisingly, I lied. You have to buy a `Monad` first.

View file

@ -0,0 +1 @@
- Good Eats, Chocolate Lava Cake and Chocolate Mousse episode: great style; plenty of references

View file

@ -1,12 +1,12 @@
# Living Free with Monads
It's an old tradition that any programmer who thinks they know something useful about monads eventually goes off and writes a blog post about their revelation.
It's an old tradition that any programmer who thinks they know something useful about monads eventually succumbs to the temptation to go off and write a blog post about their revelations . . .
_Anyway_ ...
_Anyway_ . . .
Lets take a look at a `Monad` definition (yeah, I know) in OCaml and walk through the clues that suggest a monad's implementation. Modules make OCaml a great language to explore abstract structures.
Lets take a look at a `Monad` definition in OCaml and walk through the clues that suggest a monad's implementation.
An OCaml module can be thought of as a record containing types and terms that constitutes an abstraction boundary through information hiding. OCaml's type/module system allows a programmer to selectively expose information about a module to the outside world and, dually, to selectively depend on particular module structure. Modules are the primary mechanism by which OCaml code is structured and provide programmers the machinery of composition and code reuse.
In OCaml, abstract structures such as monads are typically best represented using [modules](https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html). A module is essentially a record, containing types and terms, along with a manifest or interface that allows a programmer to selectively expose information about that module to the outside world and, dually, to selectively depend on particular characteristics of other modules. Modules provide programmers the machinery of composition and reuse and are the primary mechanism by which OCaml code is structured, neatly capturing the idea of a program abstraction boundary.
```ocaml
module type Monad = sig
@ -16,27 +16,39 @@ module type Monad = sig
end
```
Above is a module _signature_, which can be thought of as the analogue in module-space to a type in value-space (hence `module type` in the syntax). A module signature defines the set of all possible modules that comply with the structure it describes. In this case, we give a name to the set of modules containing _at least_ a type constructor `'a t`, a function `return : 'a -> 'a t`, and a function `bind : ('a -> 'b t) -> 'a t -> 'b t`. Abstractly, these are what constitute a monad.
Above is a module _signature_. Signatures themselves can be thought of as the analogue in module-space to types in value-space (hence `module type` in the syntax); each one defines the set of all possible modules that comply with the structure it describes. In this case, we give the name "`Monad`" to the set of modules containing _at least_ a type constructor `'a t`[^alpha], a function `return : 'a -> 'a t`, and a function `bind : ('a -> 'b t) -> 'a t -> 'b t`. Abstractly, these together are what constitute a monad.
It's helpful to think about what each of these items means in general before examining them in more concrete terms. `t` is a function from types to types, also known as a type constructor. `list` and `option` are such type constructors. The presence of `t` in our `Monad` signature--- specifically the fact that it's parametric--- represents the idea that a monad is essentially a _context_ around underlying computations of an abstract type. For some particular `'a` and some particular module that fits the `Monad` signature, `'a` is the type of the essential computation; that is, `t` is the generic context itself, and `'a t` is an instance of that generic context which is specific to the inner type `'a`; `'a t` is the type of alphas in the `t` sort of context. What exactly is meant by "context" here is the key to this whole endeavor, but I'll avoid addressing it directly until we're a little further along.
It's helpful to think about what each item means in general before examining them in more concrete terms. `t` is a function from types to types, also known as a type constructor. `list` and `option` both are examples of type constructors. The presence of `t` in our `Monad` signature--- specifically the fact that it's parametric, i.e. `'a t` rather than just `t` ---represents the idea that a monad is essentially a _context_ around underlying computations of an abstract type. For some particular `'a` and some particular module that fits the `Monad` signature above, `'a` is the type of the underlying computation; that is, `t` is the generic context itself, and `'a t` is an instance of that generic context which is specific to the inner type `'a`; `'a t` is the type of alphas in the `t` sort of context.
Hopefully, one of those multifarious phrasings made at least a little bit of sense--- what exactly is meant by "context" is the key to this whole endeavor, but I'll avoid addressing it directly until we're a little further along. For now, let's consider `return`.
If `t` is the generic context, then `return` is the function that makes it specific or "specializes" it to the type `'a` of some particular value `x : 'a`. This function takes an object[^object] of the base type `'a` and puts it into the context `t`.
```ocaml
module ListMonad = struct
type 'a t = 'a list
val return : 'a -> 'a t
let return : 'a -> 'a t = fun x -> [x]
. . .
end
```
`list` forms a monad when equipped with suitable definitions of `return` and `bind`, though I've omitted those definitions for now to focus on the first item. The meaning of `list` as a monad--- that is, the context that `list` and its natural accompanying definitions of `bind` and `return` represent--- is interesting, broadly useful, and sufficiently non-obvious as to demand some intuition. I'll use it as a running example.
Since `t` here is `list`, this is the function that takes an argument and sticks it into a list, i.e. `fun x -> [x]`. As you might guess, `list` forms a monad when equipped with suitable definitions of `return` and `bind` (the latter of which is omitted for now). The meaning of `list` as a monad--- that is, the context that `list` and its natural accompanying definitions of `bind` and `return` represent ---is interesting, broadly useful, and sufficiently non-obvious as to demand some intuition, so I'll use it as a running example. In its most natural interpretation, `list` represents--- or simulates[^physical] ---the property of [nondeterminism](https://en.wikipedia.org/wiki/Nondeterministic_Turing_machine), a computational model in which all possible paths are taken _simultaneously_. Considered in this light, `[x]` is a value where only one path has been taken so far, i.e. where no choices[^choice] have been made up to this point. Notice how the implementation of `return` inherently gives rise to the "no choices" notion of the empty context; it is embedded in it by definition. That notion is specific to nondeterminism, and `return` is what encodes it into the formal structure of the `ListMonad` module.
Let us finally now consider `bind`. `bind` is the driving force behind monads, performing all of the heavy lifting that makes for a useful tool in structuring algorithms. The implementation of `bind` is what captures the meaning of a particular sort of context and contextual data by encoding it into a `Monad` instance. Thus, it is `bind` _abstractly_, as it appears in the definition[^capture-define] of the `Monad` signature, which captures what is meant by "context" in general. Generally, a context should be thought of as some additional or different computation that is driven by the underlying computation in `'a`. In other words, every time a program manipulates an `'a t`, some implicit action is carried out either in addition to the direct interaction with the context or underlying value, or modifying them. This implicit action is embedded in the definition of `bind`, and thus it is the definition of a `bind` function for a type constructor that fundamentally determines what the context is or means and how it behaves.
***
// return will have embedded in it some notion of the empty or default context for a value : `'a`
A context should be thought of as some additional or different computation that is driven by the underlying computation in `'a`. In other words, ever time you work with an `'a t`, some implicit action is carried out in addition to whatever direct manipulations of the context or underlying value you perform. This implicit action is embedded in the definition of `bind`, and thus it is the definition of a `bind` function for a type constructor that fundamentally determines what the context is or means and how it behaves.
[^physical]: Of course, we say that `list` _simulates_ nondeterminism for the same reason that we say physical computers simulate turning machines: both are constrained by the resource limitations of physical reality and thus strictly weaker than the theoretical devices they seem to emulate.
A "functor" in OCaml parlance is distinct from anything called a "functor" anywhere else, being essentially a function from modules to modules. For practical reasons, modules and value-level programs are stratified from one another in OCaml, so a functor does not literally have a function type, but the mental model is useful all the same. We will encounter some functors of both sorts later on.
[^choice]: A "choice" is between two or more options; if there's just one option, you don't have a choice.
[^alpha]: Pronounced "alpha tee".
[^object]: "Object" in the general sense; nothing to do with object-orientation or the like.
[^capture-define]: be explicit about how monads exist independently and we are _capturing_ them in the particular language of ocaml. `list` forms a monad whether we actually implement that monad, or not
A "functor" in OCaml parlance is distinct from anything called a "functor" elsewhere, being essentially a function from modules to modules. For practical reasons, modules and value-level programs are stratified from one another in OCaml, so a functor does not literally have a function type, but the mental model is still basically correct. We will encounter some functors of both sorts later on.
(aside: this stratification is not theoretically needed, re 1ml)