This commit is contained in:
Alexander 2025-06-13 12:54:22 -04:00
parent a056164bd7
commit af2cdd53db

View file

@ -35,36 +35,48 @@ end
Since `t` here is `list`, `return` 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), which is characteristic of a computational model in which all possible paths are taken _simultaneously_. Considered in this light, `[x]` is a value where so far only one path has been taken, i.e. where no choices[^choice] between execution paths have been made up to this point. Examining the code above, notice how the implementation of `return` inherently gives rise to the "no choices" notion of the empty context, which is embedded in it by definition. That notion, that the empty context means no choices have been made, is specific to nondeterminism, and `return` is what encodes it into the formal structure of the `ListMonad` module.
In its most natural interpretation, `list` represents--- or simulates[^physical] ---the property of [nondeterminism](https://en.wikipedia.org/wiki/Nondeterministic_Turing_machine), which is characteristic of a computational model in which all possible paths are taken _simultaneously_. A value of type `'a list` thus represents all possible results of a particular computation of type `'a`, with each result being a list element. Considered in this light, `[x]` is a value where only one path is taken, i.e. where no branches in execution are encountered. Examining the code above, notice how the implementation of `return` inherently gives rise to the "no branches" notion of the empty context, which is embedded in it by definition. That notion, that the null context means there are no branches, is specific to nondeterminism, and `return` is what encodes it into the formal structure of the `ListMonad` module.
Finally, we move on to `bind`. `bind` is the driving force of monads; it performs the heavy lifting that makes them a useful tool for structuring algorithms. An 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, that captures what is meant by "context" in general. A context should thusly be thought of as some computation that is driven by, given its basic structure by, the underlying computation in `'a`. In other words, every time a program manipulates an `'a t`, some additional, implicit action[^action-std] is carried out alongside--- or possibly modifying ---that direct interaction with the context or its underlying value. This implicit action is embedded in the implementation of `bind`, and thus it is the definition of a `bind` function for a type constructor that fundamentally determines what is the context in question, what that context _means_ informally, and how it behaves.
Finally, we move on to `bind`. `bind` is the driving force of monads; it performs the heavy lifting that makes them a useful tool for structuring algorithms. An 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 of the `Monad` signature, that captures what is meant by "context" in general. A context should thusly be thought of as some computation that is driven by, given its basic structure by, the underlying computation in `'a`. In other words, every time a program manipulates an `'a t`, some additional, implicit action[^action-std] is carried out alongside--- or possibly modifying ---that direct interaction with the context or its underlying data. This implicit action is embedded in the implementation of `bind`, and thus it is the `bind` function for a type constructor that fundamentally determines what is the context in question, what that context _means_ informally, and how it behaves.
```ocaml
module ListMonad = struct
type 'a t = 'a list
let return x = [x]
let rec bind (f : 'a -> 'b list) : 'a list -> 'b list = function
let rec bind (f : 'a -> 'b list) (xs : 'a list) : 'b list =
match xs with
| [] -> []
| x :: xs -> f x @ bind f xs
| x :: xs' -> f x @ bind f xs'
end
```
Here we see the completed implementation of the `list` monad in the module `ListMonad`. There are a couple of things to note.
Here is the completed implementation of the module `ListMonad`, in which we have implemented the `list` monad. A good way to think about what any implementation of bind is doing at a high level is that it
1. foo
1. bar
1. extracts the value of the underlying type `'a` from `xs`,
1. transforms it _via_ `f`, producing `'b` along with new context, and
1. uses that new context, along with the original context of `xs`, to determine the final context of the returned `'b t`.
The "value of the underlying type" may be literally a single value of type `'a`, but it needn't be. In the body of `ListMonad.bind` above, we are actually extracting a whole list's worth of alphas, applying `f` to them as we recurse over the list structure--- these constitute the "underlying value" of the `'a list` `xs`.
So, how are those ideas played out for lists? If `xs` is empty, `bind` returns the empty list; that's an obvious way to handle it. Otherwise, we have a recursive case. The list is _not_ empty here, so we can safely
1. take the first element `x` and the remaining elements `xs'`,
1. apply `f` to `x` to obtain a new `'b list`, and
1. append the result of `f x` to a recursive call `bind f xs'`.
We know that the `bind` function returns a `'b list`, so we're appending the `'b list` `f x` to the `'b list` `bind f xs'`, thus obtaining the `'b list` that we return the caller.
Pay careful attention to the parallels here. You may think we didn't use the context of the original `xs`, but we did! We recursed over the context, in fact; it determined the call structure of `bind`.
***
[^physical]: Of course, we say that `list` _simulates_ nondeterminism for the same reason that we say physical computers simulate Turing machines: both are constrained by the resource limitations of physical reality and thus less capable than the theoretical devices they seem to emulate.
[^choice]: A choice is between two or more options; if there's just one option, `x`, there's no choice.
[^alpha]: Pronounced "alpha tee".
[^object]: "Object" in the general sense; nothing to do with object-orientation or kin.
[^capture-define]: TODO: 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
TODO: 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
[^action-std]: This gives rise to a standard term. See [Monads as Computations](https://wiki.haskell.org/Monads_as_computation).