more

acl.cool/site/draft/nomad.dj

@@ -1,4 +1,4 @@
-# Living Free with Monads
+# A Monad in OCaml
 
 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 . . .
 
@@ -6,7 +6,7 @@ _Anyway_ . . .
 
 Lets take a look at a `Monad` definition in OCaml and walk through the clues that suggest a monad's implementation.
 
-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.
+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 notion of a program abstraction boundary.
 
 ```ocaml
 module type Monad = sig
@@ -16,13 +16,13 @@ module type Monad = sig
 end
 ```
 
-Above is a module _signature_. Signatures themselves can be thought of as analogous 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.
+Above is a module _signature_. Signatures themselves can be thought of as relating to modules in much the same way that types relate to values (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 exposing _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 three items together are what constitute a monad.
 
 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 that multifarious bundle of 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`.
+Hopefully, one of that multifarious bundle of phrasings made at least a little bit of sense--- what exactly is meant by "context" is the key to this whole endeavor, but I'm going to 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 of `t`. The specialized context of the resulting `'a t` value will be in some sense basic, empty, default, null; it is the starting-point context that exists just to have `x` in it, so that computations involving `x` can take place in that sort of context at some point in the future.
+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 of `t`. The specialized context of the resulting `'a t` value will be in some sense basic, empty, default, null; it is the starting-point context that exists just to have `x` in it, so that computations involving `x` can take place in that sort of context later on.
 
 
 ```ocaml
@@ -33,9 +33,9 @@ module ListMonad = struct
 end
 ```
 
-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.
+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), characteristic of 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. 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_. 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.
 
 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.
 
@@ -69,4 +69,6 @@ Here we see the completed implementation of the `list` monad in the module `List
 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)
 
-[^action-std]: This gives rise to a standard term. See [Monads as Computations](https://wiki.haskell.org/Monads_as_computation).
+[^action-std]: This gives rise to a standard term. See [Monads as Computations](https://wiki.haskell.org/Monads_as_computation).
+
+So the list monad allows us to write non-determinsitic code in much the same style as we would write fundamentally simpler determinstic code