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.
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 functors1, applicative functors, and monads respectively. The only thing of note is that I’ve written the functions in pipe-last2 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?
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 produce an instance of a 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 implementation3. 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 composition4.
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.t5.
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”6 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.