pages/acl.cool/site/writings/derive-appfun.dj
2025-08-10 11:54:46 -04:00

72 lines
No EOL
7.3 KiB
Text

# Derived Implementations
Messing around with OCaml a bit a while ago, I discovered a nice concrete way to show the relationship between functors, applicatives, and monads as they're understood in functional programming. The OCaml functor implementations are basically proof terms for the implications that exist between those classes.
```ocaml
module type Monad = sig
type 'a t
val return : 'a -> 'a t
val bind : ('a -> 'b t) -> '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 Functor = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
end
```
Above, we have the usual OCaml signatures for functors[^other-functor], applicative functors, and monads respectively. The only thing of note is that I've written the functions in pipe-last[^pipe-last] style. It's more common to see pipe-first style, which agrees with the usual infix operators, but I don't see any of those around to get offended; do you?
```ocaml
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
```
Each of these functors accepts an instance of a less general structure and uses only the elements that module provides to implement an instance of the more general structure. `FunctorOfMonad` is boring, being just the composition of the others, but those themselves are a bit neat. Looking at the implementation of `map` in terms of `pure` and `apply`, you can see that we have the function `f` put into an empty context and then applied to `x`. Since there's no information about the given functor other than that it _is_ a functor, this implementation is the only way to obtain a new instance of the applicative's backing type `('a -> 'b) t`; there aren't any real options here in the way of implementation[^unique-functor]. The meaning in terms of monads and/or effects is still worth contemplating, though: applicatives tell us what application looks like in a context while monads do the same for composition[^makes-sense].
The more involved implementation in `ApplicativeOfMonad` is where we get some options in terms of implementation and also, not unrelatedly, where potential problems crop up. Because it turns out that there are multiple ways to implement `ApplicativeOfMonad`--- also multiple ways to implement a particular monad or applicative--- it becomes hard to predict whether a derived implementation matches the expected implementation without resorting to _ad hoc_ testing, which would sort of defeat the point of deriving implementations (i.e. less work).
_A concrete example might serve to illustrate better here, but I haven't been bothered to think of one. Perhaps in the future I'll update this post to go into further detail._
We derive `apply` function shown above from `bind` and `return` by threading `x` and `f` into the context through `bind` (as `y` and `g`, respectively), thus "stripping off" the context in the body of the lambda, then applying `g` to `y` to obtain a fresh `'b`, and finally passing that `'b` to `M.return`, thus producing a `'b M.t`, which of course is also an `'a t`, since `type 'a t = 'a M.t`[^with-type].
Monads have their own laws of course, but while a lawful monad is guaranteed to entail a lawful applicative--- as we can see by the signatures of our functors--- the functors aren't guaranteed to produce the _desired_ applicative for a particular input. The arbitrary nature of what applicative implementation is considered "correct"[^correct] means you don't _per se_ get the applicative you want when deriving an instance; rather, you get the version that accords with the monad, which is _probably_ what you want, but perhaps not. Furthermore, because `ApplicativeOfMonad` operates on a generic applicative and thus cannot make use of any peculiar structure in its argument, even a result that behaves "correctly" is likely to have worse performance than a decent handwritten version.
[^with-type]: In regards to the `with type = ...` syntax, there is a subtlety of the OCaml module system that if a module is defined with a particular `module type` (a.k.a. signature) attached--- for example, `module M : S = struct ...`--- all the types that are abstract in the signature `S` will _also_ be abstract in the module `M` 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, because both types are abstract, i.e. the underlying type is not available. To fix this, we can explicitly expose the equality by using the `with type` construct. In the above example, `Functor with type 'a t = 'a M.t` exposes the equality of `'a t` and `'a M.t`, so that functions defined as expecting arguments of `'a t` can accept `'a M.t`, and _vice versa_, etc.
[^falsehood]: Unsurprisingly, that's a lie. Isn't it always? You have to buy a monad first.
[^pipe-last]: This idea is that to harmonize with OCaml's automatic currying, parameters to which a function is more likely to be "partially applied" should be earlier in its parameter list. This cuts down on syntactic noise; particularly, pipes which apply to the _last_ argument (see?) don't require shuffling-about of the parameter order, e.g. `xs |> List.map f` rather than `xs |> (fun xs -> List.map xs f)`. Jane Street will tell you that [labels](https://ocaml.org/docs/labels) can [address](https://opensource.janestreet.com/base/) the issue best, but to my eyes, `:` and `~` were never meant to spend so much time that close to one another.
[^makes-sense]: It makes sense then, that having a monad nets you an applicative functor--- how can one talk about composition without having application first, which is needed to consider function-like objects at all?
[^other-functor]: A functor, in OCaml parlance, is distinct from anything called a "functor" elsewhere, being essentially a function from modules to modules. This can indeed become confusing. 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 to think of them that way is still basically correct. See [1ML](https://people.mpi-sws.org/~rossberg/1ml/1ml-jfp-draft.pdf) if interested in an OCaml-like language without such a stratification.
[^low-effort]: On the other hand, the derivations here can usually be performed rather mechanically, with little insight, by following the types in much the same way one might mechanically infer a direct proof in sentential logic, making them fairly low-effort and so still possibly not a waste of time.
[^correct]: Assuming, of course, that you admit some definition of correct as roughly "making sense in context" or "being broadly useful".
[^legis]: There are [laws about these sorts of things](https://hackage.haskell.org/package/base-4.14.1.0/docs/Control-Applicative.html), you know.
[^unique-functor]: This is true is a [precise sense](https://mail.haskell.org/pipermail/libraries/2011-February/015964.html).