pages/acl.cool/site/draft/derive-appfun.dj
2025-07-01 00:34:28 -04:00

110 lines
No EOL
8.6 KiB
Text

# Functors and Applicatives, Gratis[^falsehood]
It's usually possible to derive implementations of general structures from those of more specific ones; here, `Applicative` from `Monad` and `Functor` from `Applicative`. This is how to do it, and why not to.
```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 somewhat more interesting. Looking at the implementation of `map` in terms of `pure` and `apply`, we can see that we have the function `f` put into an empty context and then applied to `x`. Since we can't know more about the particular applicative functor given, this is the only way to obtain a new instance of its backing type `('a -> 'b) t`, so there aren't any real options here in the way of implementation[^unique-functor]. Still, the meaning in terms of monads and/or effects is worth contemplating; 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 our problems arise. Because it turns out that there are multiple ways to implement the derivation functor--- also multiple ways to implement a particular monad or applicative--- it becomes hard to predict whether a derived implementation is the expected one without resorting to _ad hoc_ testing, testing that rather defeats the point of "gratis"[^low-effort]. The `apply` function, shown above, is derived 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].
To explore concretely how deriving instances can go wrong, consider the following `EitherMonad`.
```ocaml
type ('a, 'b) either = A of 'a | B of 'b
module EitherMonad (T : sig type t end) : Monad with type 'a t = ('a, T.t) either = struct
return x = [x]
let rec bind (f : 'a -> 'b list) : 'a list -> 'b list = function
| [] -> []
| x :: xs -> f x @ bind f xs
end
```
This has the following derived `Applicative`.
```ocaml
derived app for bar monad
```
And then, here's a lawful[^legis] implementation of `Applicative` for `bar` which is _not_ the one produced by `ApplicativeOfMonad (BarMonad)`.
```ocaml
lawful other bar
```
Just to be sure, let's check that this new instance satisfies the required properties, i.e. that
1. `apply (pure Fun.id) x` = `x`
1. `apply (apply (apply (pure Fun.compose) f) g) x` = `apply f (apply g x)`
1. `apply (pure f) (pure x)` = `pure (f x)`
1. `apply f (pure x)` = `apply (pure (fun g -> g x)) f`
for `BarApplicative'` just as for `ApplicativeOfMonad (BarMonad)`.
{% these are identity, composition, homomorphism, and interchange %}
Monads have their own laws of course, but while a lawful monad is guaranteed to entail a lawful applicative, as we can see, it isn't guaranteed to produce the _desired_ applicative when given as input to a particular derivation functor. The alternate definition above may or may not be a useful one, but the point is that 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. The nice thing about OCaml here, as opposed to Haskell with its typeclasses, is that there's no barrier to having multiple implementation of the `Applicative` signature, so it's easy to implement a different instance without ambiguity. Furthermore, because `ApplicativeOfMonad` operates on a generic applicative and thus cannot make use of any peculiar structure in its argument, even a result that does behave as desired may be less performant in code than a decent handwritten version--- compare such implementations for *FooMonad*.
```ocaml
foo monad stuff
```
[^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.
[^1ml]: See [1ML](https://people.mpi-sws.org/~rossberg/1ml/1ml-jfp-draft.pdf) for an OCaml-like language without this stratification.
[^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).