This commit is contained in:
Alexander 2025-06-13 08:49:07 -04:00
parent 02c92e795f
commit a056164bd7
3 changed files with 9 additions and 8 deletions

View file

@ -1,48 +0,0 @@
# 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".
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 a simple proposition. So it _is_ a relatively low-effort and low-investment activity.
TODO: explain functors and `with type`.
[^falsehood]: Unsurprisingly, that's a lie. You have to buy a `Monad` first.

View file

@ -66,9 +66,8 @@ Here we see the completed implementation of the `list` monad in the module `List
[^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
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).
So the list monad allows us to write non-determinsitic code in much the same style as we would write fundamentally simpler determinstic code
So the list monad allows us to write non-determinsitic code in much the same style as we would write fundamentally simpler determinstic code
(aside: this stratification is not theoretically needed, re 1ml)