https://siraben.dev/2020/02/20/free-monads.html siraben's musings [ ] About Me Free monads from scratch Feb 20, 2020 See the accompanying gist for the code. Haskellers love monads, and there's a good reason why. Without monads, Haskell wouldn't have much of an I/O system at all, as Simon Peyton-Jones described it, it was embarassing to note that the emperor lacked I/O at conferences. Nevertheless, Haskell could be considered the world's finest imperative language because of the way its type system forces one to separate purity and impurity, allowing the use of pure functions in impure code, but not vice versa. The next stepping stone on the road to Haskell proficiency is often learning monad transformers, so that effects can be combined. In other words, we want to write code like this, resembling an impure language. ticke n = do y <- recall -- read global state incr 5 -- modify global state z <- recall if z > n then raise "too big" -- throw exception else return y The corresponding imperative code might be: function ticke() { const y = getState(); incr(5); const z = getState(); if (z > n) { throw "too big"; } else { return y; } } But this blog post is not about monad transformers, it's about another idea that's less well-known, free monads, a neat way to combine effects with less boilerplate, and has been applied in works such as Extensible Effects and Polysemy. Free monads are relatively easy to construct and explain and can help set the ground for fancier, more efficient effect systems. This blog post assumes a working knowledge of Haskell, typeclasses, and some category theory. What is a free object? A free object is a construction that obeys the axioms for that object, generated from something simpler. A canonical example of a free object is a free monoid. Recall that a monoid is a set \(S\) together with a binary operation \(\cdot\) and an element \(e\in S\) such that \(a\cdot(b\cdot c)=(a\cdot b)\cdot c\) for all \(a,b,c\) and \(e\cdot a=a\cdot e=a\) for all \(a\). So, given a set \(S = \{a, b, c, d\}\), what is the free monoid over it? It's simply the language \(\{a, b, c, d\}*\), giving us strings like \(e\), \(aa\), \(abc\), \(acdbcd\) and so on. The only thing we can do with these objects is treat them according to the axioms they obey, in other words, we can only concatenate them and nothing more. People who have written interpreters may notice that free objects are like valid ASTs of a particular programming language. The axioms let us perform some manipulations, for instance, if we create a free group, we know we can rewrite \(a\cdot a^{-1}\) to \(e\), because that's one of the group axioms. However, we would be unable to reduce something like \(2+3\) because we don't have an interpretation for it. This will come in later when we implement interpreters for effects. Enough of this abstract algebra, let's see some code! Coproducts of functors infixr :+: data (f :+: g) r = Inl (f r) | Inr (g r) deriving (Functor) :+: is a type operator, i.e. it takes two type constructors f :: * -> * and g :: * -> * and a type r :: *, and producing a new type (f :+: g) r :: *. To construct a value of this type, we the Inl and Inr constructors. This resembles the Either type, but over higher kinded types f and g. Categorically, this is the coproduct construction in the functor category. Now the main data type: data Term f a = Pure a | Impure (f (Term f a)) We can read Term f a as a term of our language generated by f, having a final value of type a, here are some examples. l> Pure 3 Pure 3 :: Term f Integer l> Impure (Just (Pure 3)) Impure (Just (Pure 3)) :: Term Maybe Integer l> Impure Nothing Impure Nothing :: Term Maybe a But generated how? Notice that the argument to Impure has type f (Term f a), but we're showing how to construct a term of type Term f a in the data declaration, so this is like fixpoints of functions, with Pure as the "base case". In the case that f happens to be a functor, Term is what is known as a fixpoint of a functor, as seen in papers such as Data types a la carte by Swierstra. Free Monads It gets better. If we know f is a functor, we know that it must have fmap, even better, we can write the Functor, Applicative and Monad instances for Term f! instance Functor f => Functor (Term f) where fmap f (Pure x) = Pure $ f x fmap f (Impure t) = Impure $ fmap (fmap f) t instance Functor f => Applicative (Term f) where pure = Pure Pure f <*> Pure x = Pure $ f x Pure f <*> Impure b = Impure $ fmap (fmap f) b Impure fx <*> a = Impure $ fmap (<*> a) fx instance Functor f => Monad (Term f) where return = pure Pure x >>= f = f x Impure t >>= f = Impure $ fmap (>>= f) t At first sight this looks scary, but in fact it isn't at all, here's the same code with only the last line in each instance declaration shown. instance Functor f => Functor (Term f) where -- ... fmap f (Impure t) = Impure $ fmap (fmap f) t instance Functor f => Applicative (Term f) where -- ... Impure fx <*> a = Impure $ fmap (<*> a) fx instance Functor f => Monad (Term f) where -- ... Impure t >>= f = Impure $ fmap (>>= f) t Notice how we're implementing >>= with >>= on the right, and <*> with <*>, but applying it via fmap? It seems like an impossible trick at first, we don't even know f forms a monad! But we do know some laws about applicatives and monads. fmap f (pure x) = pure (f x) pure f <*> pure x = pure (f x) pure x >>= f = f x Believe it or not, this is exactly the code we need to implement the fmap, <*> and >>= operators for Term f! Perhaps the only thing left to explain is the implementation of <*> in the case that the first argument is pure and the second argument is impure, left as an exercise. Pure f <*> Impure b = Impure $ fmap (fmap f) b We're quite close now, just one more class and a couple of instances and we'll have the core for our free monad effects library. class (Functor sub, Functor sup) => sub :<: sup where inj :: sub a -> sup a sub and sup are functors, and inj is the natural transformation that turns a sub into a sup. Intuitively we can think of sup as allowing an embedding of sub into it, but not necessarily the other way around. Now that we're in the functor category, we know there is an identity natural transformation for every functor into itself, so there must be an embedding of every functor into itself. instance Functor f => f :<: f where inj = id What about the relation between f and f :+: g? Now that we're talking category theory, f :+: g is really a coproduct of f and g in the functor category. So indeed there is a morphism from f to f :+: g, the Inl morphism. instance (Functor f, Functor g) => f :<: (f :+: g) where inj = Inl Finally, we want to be able to extend an existing embedding. Let's say we are given functors f, g and h, and know that f :<: g. It stands to reason that if f already has an embedding into g, it also has an embedding into whatever g can embed into. In particular, g can embed into h :+: g. Therefore, f can be embedded into h :+: g as well. First we embed f into g via inj, then we go from g to h :+: g by Inr. inj and Inr are natural transformations, so we can compose them to get a natural transformation from f to h :+: g. instance (Functor f, Functor g, Functor h, f :<: g) => f :<: (h :+: g) where inj = Inr . inj First, we're going to want to convert a Term f a into an a, i.e. escaping out of the Term monad. We can extract such an a by pattern matching on Pure a. It now remains to settle on an appropriate functor f. We don't want to handle the Impure case, because that means we have some function of type f a -> a, which may not exist (e.g. [], IO, Maybe). Since Impure should not happen, f (Term f a) must not happen either, which means a -> f a should not exist! A functor f with no way of getting from a -> f a nor f a -> a? This forces our choice of f to be the Void functor, which has no constructors. data Void t deriving (Functor) efRun :: Term Void a -> a efRun (Pure a) = a And that's it. While it looks like boilerplate, we can more or less mechanically write out the instances, thanks to universal objects, and notions from category theory. To really illustrate the power of this, we're going to see a series of increasingly ambitious examples of effects. A stateful calculator Let's implement a simple calculator with a single Int register. We define the operations of this calculator separately; Incr and Reader. * Incr i t increments the state by i and returns t * Reader f extracts the state and runs f on it * Mem i represents the state having value i data Incr t = Incr Int t deriving (Functor) data Reader t = Reader (Int -> t) deriving (Functor) data Mem = Mem Int deriving (Show) Given the commands, we need to define their denotation, i.e. their meaning. This is given by the efRunCalc function. If the command is Pure x, just return x along with the state. efRunCalc :: Functor r => Mem -> Term (Incr :+: (Reader :+: r)) a -> Term r (a, Mem) efRunCalc s (Pure x) = return (x, s) If the command is Incr k r, modify the state by k and continue with r. The slight twist is that we need to pattern match with Inl, because to extract Incr from (Incr :+: (Reader :+: r)). To extract Reader from (Incr :+: (Reader :+: r)) we have to perform Inl followed by Inr. Finally, to handle r, we fmap (efRunCalc s) over t. efRunCalc (Mem s) (Impure (Inl (Incr k r))) = efRunCalc (Mem (s + k)) r efRunCalc (Mem s) (Impure (Inr (Inl (Reader r)))) = efRunCalc (Mem s) (r s) efRunCalc s (Impure (Inr (Inr t))) = Impure (efRunCalc s <$> t) We'll also define a couple of helper functions, incr and recall can be thought of the user-facing functions for calculator effects. inject :: (g :<: f) => g (Term f a) -> Term f a inject = Impure . inj incr :: (Incr :<: f) => Int -> Term f () incr i = inject (Incr i (Pure ())) recall :: (Reader :<: f) => Term f Int recall = inject (Reader Pure) Now, we can combine our Incr and Reader effects in a single monad. tick :: (Incr :<: f, Reader :<: f) => Term f Int tick = do y <- recall incr 1 return y What you see in the code examples is all there is, no monad transformers needed. We can combine effects freely. When we interpret effects, we handle them one by one. l> tick & efRunCalc (Mem 4) & efRun (4,Mem 5) Adding Exceptions Suppose now we want to add a raise command to our calculator, the Exc effect. This is done separately. A pattern arises for making new effects, we define our type, our user-facing functions and an interpreter for our effect. data Exc e t = Exc e deriving Functor raise :: (Exc e :<: f) => e -> Term f a raise e = inject (Exc e) efRunExc :: Functor r => Term (Exc e :+: r) a -> Term r (Either e a) efRunExc (Pure x) = return (Right x) efRunExc (Impure (Inl (Exc e))) = return (Left e) efRunExc (Impure (Inr t)) = Impure (efRunExc <$> t) Due to our coproduct construction, Exc is separate from the other effects. ticke uses all the effects we have seen so far. ticke :: (Exc String :<: f, Incr :<: f, Reader :<: f) => Int -> Term f Int ticke n = do y <- recall incr 5 z <- recall if z > n then raise "too big" else return y efRunExcString :: Functor r => Term (Exc String :+: r) a -> Term r (Either String a) efRunExcString = efRunExc The reason why we need efRunExcString is that we need to be explicit about handling the Exc String effect, otherwise we get a type error about no instances for (Exc String :<: Void). It's really a type inference failure, because Haskell could not infer the instance at the call-site (this is a problem effect libraries attempt to address). Transactional memory for free We can also show that the order in which effects are handled makes a difference. For instance, in the first line below we handle the exception first then the state after (so the state persists even though an exception is thrown), and in the second line the state is handled first followed by the exception, which means the state is discarded when the exception is thrown. l> ticke 1 & efRunExcString & efRunCalc (Mem 0) & efRun (Left "too big",Mem 5) l> ticke 1 & efRunCalc (Mem 0) & efRunExcString & efRun Left "too big" Think of the latter case as a sort of "transactional" style whereby an action must fully succeed or fail and the intermediate state at the point of failure is impossible to access. For our final example, we generalize the state to an arbitrary type s, and write an imperative program to sum the first n numbers. -- Enable the ConstraintKind language extension for this data Writer s t = Put s t deriving Functor data Reader s t = Get (s -> t) deriving Functor type StEff s r = (Reader s :<: r, Writer s :<: r) efRunSt :: Functor r => State s -> Term (St s r) a -> Term r (a, s) efRunSt (State s) (Pure x) = return (x, s) efRunSt (State s) (Impure (Inl (Put k r))) = efRunSt (State k) r efRunSt (State s) (Impure (Inr (Inl (Get r)))) = efRunSt (State s) (r s) efRunSt s (Impure (Inr (Inr t))) = Impure (efRunSt s <$> t) put :: (Writer s :<: f) => s -> Term f () put s = inject (Put s (Pure ())) get :: (Reader s :<: f) => Term f s get = inject (Get Pure) sumN :: (StEff (Integer, Integer) f) => Term f () sumN = do (acc, n) <- get if n == 0 then return () else do { put (acc + n, n - 1); sumN } sumNEx :: ((), (Integer, Integer)) sumNEx = sumN & efRunSt (State (0,10)) & efRun Run the code shown in this post by downloading the gist. Conclusion and Further Reading I hope this post was illuminating in understanding what free monads are and their implementation. There's quite a lot of literature on the subject, and the various effect libraries in use are worth checking out, because they address problems we weren't able to handle in our from-scratch implementation, reducing boilerplate even further, creating better error messages, among other things. * Data types a la carte + The paper by Swierstra in which he presents a solution to the expression problem, that is, extending a data type without recompiling existing code while retaining type safety. Data types a la carte expresses effects as algebras and interpretation as a fold over that algebra. * Extensible Effects vs Data types a la Carte + While Swierstra's construction is notable, Oleg Kiselyov demonstrates that the algebra construction is unable to handle the addition of new effects, in other words, it was not an extensible system. Provides some good precautions on using category theory as a design tool. siraben's musings * siraben's musings * [email protected] * siraben Writing proofs and programs.