asdf
This commit is contained in:
Alexander
parent
655dc262f0
commit
7e670c7406
3 changed files with 46 additions and 20 deletions
|
|
@ -8,7 +8,7 @@ If you want to look at the implementation ahead-of-time, [Hackage](https://hacka
|
|||
|
||||
_Distfix grammars and notation are more commonly referred to as "mixfix", but the paper calls them "distfix" and that's what I'm sticking with._
|
||||
|
||||
The idea of distfix grammars is to provide a formalism for manipulating user-defined operators. The formalism is weaker than that of context-free grammars --- CFGs can describe far more languages then DFGs --- but it is because of this weakness that we can reason about DFGs with relative ease.
|
||||
The idea of distfix grammars is to provide a formalism for manipulating user-defined operators. The formalism is weaker than that of context-free grammars--- CFGs can describe far more languages then DFGs--- but it is because of this weakness that we can reason about DFGs with relative ease.
|
||||
|
||||
Let's look at a definition.
|
||||
|
||||
|
|
|
|||
|
|
@ -39,12 +39,14 @@ module FunctorOfMonad (M : Monad) :
|
|||
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". On the other hand, the derivations here can be performed pretty mechanically, with little insight, by following the types in much the same way one might mechanically prove an easy proposition.
|
||||
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". On the other hand, the derivations here can be performed pretty mechanically, with little insight, by following the types in much the same way one might mechanically prove an easy proposition.
|
||||
|
||||
***
|
||||
|
||||
The modules above that seem to have parameters, do; these modules are called "functors". 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.
|
||||
The modules above that seem to have parameters, do; these modules are called "functors". 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[^1ml], so a functor does not literally have a function type, but the mental model is still basically correct.
|
||||
|
||||
A subtlety of the OCaml module system is that if a module is defined with a particular `module type` a.k.a. signature attached, e.g. `module M : S = struct...`, all the types that are abstract in the signature `S` will _also_ be abstract in the module itself. This means that the compiler can't see or be convinced that for some `F (M)` with `type t = M.t` in `F`, `M.t` and `(F (M)).t` are equal. This is because both types are abstract, meaning the underlying type is not available. To fix this, we can explicitly expose the equality by using the `with type` construct. In the above, `Functor with type 'a t = 'a M.t`--- for example ---exposes the equality of the two types, so that functions defined as expecting arguments of `'a t` can accept `'a M.t`, and _vice versa_.
|
||||
A subtlety of the OCaml module system is that if a module is defined with a particular `module type` a.k.a. signature attached, e.g. `module M : S = struct...`, all the types that are abstract in the signature `S` will _also_ be abstract in the module itself. This means that the compiler can't see or be convinced that for some `F (M)` with `type t = M.t` in `F`, `M.t` and `(F (M)).t` are equal. This is because both types are abstract, meaning the underlying type is not available. To fix this, we can explicitly expose the equality by using the `with type` construct. In the above, `Functor with type 'a t = 'a M.t`--- for example--- exposes the equality of the two types, so that functions defined as expecting arguments of `'a t` can accept `'a M.t`, and _vice versa_.
|
||||
|
||||
[^falsehood]: Unsurprisingly, that's a lie. You have to buy a `Monad` first.
|
||||
[^falsehood]: Unsurprisingly, that's a lie. You have to buy a `Monad` first.
|
||||
|
||||
[^1ml]: See [1ML](https://people.mpi-sws.org/~rossberg/1ml/1ml-jfp-draft.pdf) for an OCaml-like language without this stratification.
|
||||
|
|
@ -18,13 +18,12 @@ end
|
|||
|
||||
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, or a "generic type"[^not-quite] in some languages. `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.
|
||||
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, or a "generic type"[^not-quite] in some languages. `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, something in that 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 later on.
|
||||
|
||||
|
||||
```ocaml
|
||||
module ListMonad = struct
|
||||
type 'a t = 'a list
|
||||
|
|
@ -33,11 +32,11 @@ module ListMonad = struct
|
|||
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.
|
||||
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_. 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.
|
||||
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 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.
|
||||
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--- and gives additional structure to--- the underlying computation in `'a`. In other words, every time a program manipulates an `'a t`, some additional, implicit computation is carried out alongside, or possibly modifying, that direct interaction with the context or data therein. This implicit computation 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
|
||||
|
|
@ -50,23 +49,48 @@ module ListMonad = struct
|
|||
end
|
||||
```
|
||||
|
||||
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
|
||||
Above is the completed definition of `ListMonad`, including `bind`. A good way to think about what any implementation of bind is doing at a high level is that it
|
||||
|
||||
1. extracts the value of the underlying type `'a` from `xs`,
|
||||
1. transforms it _via_ `f`, producing `'b` along with new context, and
|
||||
1. transforms it _via_ `f`, producing some `'b` value with its own associated 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`.
|
||||
The "value of the underlying type" may be literally a single value of type `'a`, but it needn't be. In `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`. To understand how this plays out concretely, let's walk through the definition `ListMonad.bind`.
|
||||
|
||||
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
|
||||
If `xs` is empty, `bind` returns the empty list; this is the usual base case for recursion on lists. If `xs` is not empty, we have an inductive case; it is safe to
|
||||
|
||||
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'`.
|
||||
1. apply `f` to `x` to obtain a new `'b list`,
|
||||
1. append the result of `f x` to the 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.
|
||||
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 a new `'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`.
|
||||
Pay careful attention to the parallels here with the high-level steps outlined previously. It may seem at first that we don't use the original context, but we do! We recurse over the context, i.e. the list structure of the `'a list` `xs`; it determines the call graph of `bind` and is integral to the final result of the function.
|
||||
|
||||
```ocaml
|
||||
let sqrt (x : float) =
|
||||
if x < 0 then invalid_arg "negatives have no sqrt" else
|
||||
if x = 0 then [0] else
|
||||
let pos_root = Float.sqrt x in [pos_root; ~-.pos_root]
|
||||
|
||||
let various_floats = [1.0; 4.0; 9.0]
|
||||
|
||||
let together : float ListMonad.t = ListMonad.bind sqrt various_floats
|
||||
```
|
||||
|
||||
Here's an example of the monad in action. `together` is `[1.0; -1.0] @ [2.0; -2.0] @ [3.0; -3.0]`, which of course is `[1.0; -1.0; 2.0' -2.0; 3.0; -3.0]`. In this case, we used the taking-all-branches nature of the list monad to compute all the square roots of the numbers in the provided list. If taking the square-root is considered to be an ambiguous operation[^i-know], then *yada yada*. This monad is often used to run operations that have some ambiguous result, to capture the idea that multiple possible return values are valid, e.g. "the square root of four" can be considered ambiguous, since both 2^2^ and (-2)^2^ are 4. Another example of this can be found in parsing with ambiguous grammars. Parser combinator libraries often make it easy to define ambiguous-on-the-face parsers and resolve the ambiguity through some convention, but perhaps
|
||||
|
||||
looks like multiple return with only one in the chain, but the sequencing is what gives us nondeterminism; multiple return doesn't chain the same. To do this without a monad we'd need to do
|
||||
|
||||
```ocaml
|
||||
bad shit
|
||||
```
|
||||
|
||||
The list monad allows us to write non-deterministic code in much the same style as we would write fundamentally simpler deterministic code, albeit with substantial boilerplate. We can reduce this boilerplate by making use of OCaml's `let*` [binding operators](https://ocaml.org/manual/5.3/bindingops.html#ss:letops-rationale)[^haskocaml].
|
||||
|
||||
```ocaml
|
||||
insert code using binding operators
|
||||
```
|
||||
|
||||
***
|
||||
|
||||
|
|
@ -82,6 +106,6 @@ TODO: be explicit about how monads exist independently and we are _capturing_ th
|
|||
|
||||
[^not-quite]: These are not exactly the same, but the similarity is more important than the difference.
|
||||
|
||||
So the list monad allows us to write non-determinsitic code in much the same style as we would write fundamentally simpler determinstic code
|
||||
[^haskocaml]: Haskell and Lean lack binding operators and instead use [Typeclasses](https://www.haskell.org/tutorial/classes.html) and an infix operator `>>=` for this boilerplate reduction. OCaml, in turn, lacks typeclasses (or the more likely equivalent feature, [modular implicits](https://www.cl.cam.ac.uk/~jdy22/papers/modular-implicits.pdf)).
|
||||
|
||||
(aside: this stratification is not theoretically needed, re 1ml)
|
||||
[^i-know]: Whether taking the square root of a number _is_ considered to be ambiguous tends to be regional. In some regions, only to the positive root is referred to, by convention.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue