In a recent post, I casually described Prompt monads as free monads. This is one of those facts that is probably well-known, but which I’ve never seen explicitly stated anywhere, so I figured I’d do so here.
I’m going to assume some basic knowledge of category theory here: specifically, the definitions of category and functor. All the rest I’ll explain as we go along. If that’s not your cup of tea, or if the fact that Prompt
is free is already obvious, feel free to skip ahead.
This document is a literate Haskell file. You should be able to copy it directly out of your browser, save it as a file called “FreePrompt.lhs”, and load it into GHCi. Alternately, you can download the my original lhs+markdown file.
> {-# LANGUAGE RankNTypes, GADTs, TypeOperators #-}
>
> module FreePrompt where
>
> import Control.Monad
> import Control.Monad.Cont
> import Control.Monad.Reader
Let’s start by defining two categories. The first, I, is the category of indexed types and type-preserving functions. We'll write f :-> g
for an index-preserving function from f
to g
.
> type f :-> g = forall i. f i -> g i
The second, M, is the category of Haskell monads—or, more accurately, the category of instances of the Monad
class. Its arrows are monad morphisms, which are index-preserving functions that respect the Monad
operations. That is, if f :: m :-> n
is a monad morphism from m
to n
, then we have
f (return a) = return a
f m >>= f . g = f (m >>= g)
for any a
, m
, and g
of the appropriate types.
Since every instance of Monad
is an indexed type (in the sense that it takes a single parameter), and since every monad morphism is an index-preserving function, we can say that M is a subcategory of I. This implies the existence of a functor U : M → I which simply maps things to themselves. This is known as a forgetful functor, because it discards the extra structure in M.
Now let’s talk about Prompt
. Here’s one basic definition:
data Prompt p a
= Done a
| forall i. Prompt (p i) (i -> Prompt p a)
prompt :: p a -> Prompt p a
prompt p = Prompt p Done
Essentially, a computation of type Prompt p a
is either a pure value, or a prompt and a continuation.
While simple, this particular implementation has performance problems, so we’ll use its Church encoding:
> newtype Prompt p a
> = P (forall b. (forall i. p i -> (i -> b) -> b) -> (a -> b) -> b)
>
> unP (P f) = f
>
> prompt :: p a -> Prompt p a
> prompt p = P (\c -> c p)
We’ll also provide a simple way to run computations:
> run :: Monad m => (p :-> m) -> Prompt p a -> m a
> run f m = unP m (\p k -> f p >>= k) return
The Monad
instance is what interests us here.
> instance Monad (Prompt p) where
> return x = P (\c k -> k x)
> m >>= f = P (\c k -> unP m c (\a -> unP (f a) c k))
Notice that Prompt p
is a monad for any indexed type p
. In other words, it maps the objects of I to M. We can similarly define
> pmap :: (p :-> q) -> (Prompt p :-> Prompt q)
> pmap f m = P (\c k -> unP m (c . f) k)
which maps index-preserving functions to monad morphisms.1 This means we can define a functor P : I → M.
Now we’re going to argue that P is the left adjoint of U. There are a few ways of doing this, including showing an isomorphism between index-preserving functions f : T → U M and monad morphisms g : P T → M, but I’m going to focus on defining the unit and counit.
The unit, η : 1 ⇒ PU, gives a family of index-preserving functions. The counit, ε : UP ⇒ 1, gives a family of monad morphisms. In Haskell, these correspond to the types,
unit :: p :-> Prompt p
counit :: (Monad m) => Prompt m :-> m
with the additional requirement that counit
is a monad morphism. unit
is pretty clearly the same thing as prompt
, and we’ll define counit
as run id
.
Next, we should show that run id
is a monad morphism. In fact, run f
is a monad morphism for any f
. The proof that run f (return a) = return a
is simple, and for the proof that run f (m >>= g) = run f m >>= run f . g
, we only need to consider the case where m = prompt p
:
run f (prompt p >>= g)
= unP (prompt p >>= g) (\p k -> f p >>= k) return
= unP (prompt p) (\p k -> f p >>= k)
(\a -> unP (g a) (\p k -> f p >>= k) return)
= f p >>= run f . g
run f (prompt p) >>= run f . g
= unP (prompt p) (\p k -> f p >>= k) return >>= run f . g
= f p >>= return >>= run f . g
= f p >>= run f . g
Implications
There are two interesting implications to the fact that P is a left adjoint of U. First, since U is a forgetful functor, P is free. In other words, Prompt p
is simplest monad that can be derived from a type constructor p
.
Second, PU is a monad in I.2 We already have the unit, η, and we can define μ using ε.
μ = UεP : UPUP ⇒ UP
Now, we’ve seen monads in I before; Conor McBride described them in “Kleisli Arrows of Outrageous Fortune”.
For the sake of making this complete, here are the definitions of IFunctor
and IMonad
again:
> class IFunctor f where
> imap :: (p :-> q) -> (f p :-> f q)
>
> class IFunctor f => IMonad f where
> iskip :: p :-> f p
> iextend :: (p :-> f q) -> (f p :-> f q)
>
> (?>=) :: IMonad f => f p i -> (p :-> f q) -> f q i
> m ?>= f = iextend f m
It should be pretty obvious that imap
is just pmap
and iskip
is prompt
. iextend
could be defined as \f -> run id . pmap f
, but we’ll simplify it.
> instance IFunctor Prompt where
> imap = pmap
>
> instance IMonad Prompt where
> iskip = prompt
> iextend f m = P (\c -> unP m (\p -> unP (f p) c))
Note that, since run id
and pmap f
are monad morphisms, iextend f
is a monad morphism for any function f
.
Components
So, is this good for anything? Well, it turns out that functions of the type p :-> Prompt q
are a pretty good approximation of the components Johan Granström describes in his paper “A new paradigm for component-based development” (PDF).
The basic idea is that a computation m :: Prompt p a
may interact with an external “world” through the interface p
. A component f :: p :-> Prompt q
provides an implementation of p
in terms of another interface, q
.
Coming up with examples that are self-contained and interesting is difficult, so I’ll give part of a UTF-8 converter I wrote using this style. It was part of an exercise in making iteratee-like components. Essentially, an iteratee uses the Stream e
interface to request elements of type e
.
> data Chunk e = Chunk e | EOS
>
> data Stream e i where
> SRead :: Stream e (Chunk e)
When I was writing my UTF-8 converter, I occasionally wanted to be able to read the next byte in the stream only if it met certain criteria. Otherwise, I wanted it to stay in the stream for later. This could have been done by adding local state to the converter, but since most stream providers will offer some lookahead, I figured my converter could use a variation I called “guarded streams”.
> data GStream e i where
> GReadAny :: GStream e (Chunk e)
> GReadOnly :: (e -> Bool) -> GStream e (Maybe e)
The idea is that GReadOnly f
provides a test, f
. If the next element of the stream does not satisfy f
or is the end-of-stream, the world should return Nothing
and leave the next element or EOS for subsequent reads.3
As a very simple example of a component using GStream
, here’s one that collects runs of a character.
> charRuns :: Stream (Char, Int) :-> Prompt (GStream Char)
> charRuns SRead = do
> ch <- prompt GReadAny
> case ch of
> Chunk c -> collect c 1
> EOS -> return EOS
> where
> collect c n = do
> mc <- prompt (GReadOnly (== c))
> case mc of
> Nothing -> return (Chunk (c,n))
> Just _ -> collect c (n+1)
This reads one character, then requests only additional characters equal to the first one. If the input is an “a” followed by a “b”, the GReadOnly
will return Nothing
and save the “b” for the future.
To show this in action, we’ll provide a generic consumer:
> collect :: Prompt (Stream e) [e]
> collect = do
> ch <- prompt SRead
> case ch of
> Chunk e -> liftM (e:) collect
> EOS -> return []
And using some interpreters defined below, we can see how it works:
*FreePrompt> stateful1 gstream "aaabcc" (collect >>= charRuns) [('a',3),('b',1),('c',2)]
The control flow here is more complicated than the familiar Haskell monads. In collect ?>= charRuns
, control passes from collect
to charRuns
whenever collect
invokes prompt
, but it returns to collect
once charRuns
produces an answer. This can be understood by looking at the monad laws and remembering that ?>= f
is a monad morphism.
We have:
(prompt p >>= f) ?>= g
= (prompt p ?>= g) >>= \x -> f x ?>= g
= g p >>= \x -> f x ?>= g
Essentially, iextend
gives us a way to compose subroutines.
Now, for a more complex component. charRuns
requires a guarded stream, but what if our stream provider only supports unguarded streams? Well, we can implement GStream
using an unguarded stream and some state. Since components don’t have state that persists across invocations, we’ll add the state to our interface.
Here’s the interface for mutable state:
> data St s i where
> Get :: St s s
> Put :: s -> St s ()
We can combine Stream e
and St s
by using the lifted sum from before.
> data (p :\/ q) i = L (p i) | R (q i)
And here’s the component:
> guardStream ::
> GStream e :-> Prompt (St (Maybe (Chunk e)) :\/ Stream e)
> guardStream GReadAny = do
> mch <- prompt (L Get)
> case mch of
> Nothing -> prompt (R SRead)
> Just ch -> do
> prompt (L (Put Nothing))
> return ch
> guardStream (GReadOnly f) = do
> mch <- prompt (L Get)
> case mch of
> Nothing -> do
> ch <- prompt (R SRead)
> case ch of
> Chunk e | f e -> return (Just e)
> _ -> do
> prompt (L (Put (Just ch)))
> return Nothing
> Just ch -> do
> case ch of
> Chunk e | f e -> do
> prompt (L (Put Nothing))
> return (Just e)
> _ -> return Nothing
We’ll combine two interpreters for the two interfaces
> streamState s
> = stateful stream s . lstateful state Nothing
*FreePrompt> let op = collect ?>= charRuns ?>= guardStream *FreePrompt> streamState "abba" op [('a',1),('b',2),('a',1)]
Note that the two interfaces, St s
and Stream e
are independent. If we had some other component c :: Stream e :-> Prompt Q
, we could easily connect it to guardStream
by using \/
or some similar function.
> (f \/ g) (L p) = f p
> (f \/ g) (R q) = g q
>
> iright :: IMonad m => (p :-> m q) -> ((r :\/ p) :-> m (r :\/ q))
> iright f = (iskip . L) \/ (imap R . f)
Generators
Prompt
is closely related to the ICont
monad I discussed previously:
> newtype ICont q p i = ICont { unICont :: (p :-> q) -> q i }
>
> instance IFunctor (ICont q) where
> imap f m = ICont (\k -> unICont m (k . f))
>
> instance IMonad (ICont q) where
> iskip x = ICont (\k -> k x)
> iextend f m = ICont (\k -> unICont m (\p -> unICont (f p) k))
When q
is a continuation monad, they are (almost) interconvertible.
> to :: Prompt p a -> ICont (Cont b) p a
> to m = ICont (\c -> cont (unP m (runCont . c)))
>
> from :: (forall b. ICont (Cont b) p a) -> Prompt p a
> from m = P (\c -> runCont (unICont m (cont . c)))
Note that from
requires the Cont b
to be polymorphic in b
. This indicates that Prompt
is weaker than ICont (Cont b)
, in the sense that it only has access to undelimited continuations.
This near-interconvertibility suggests that ICont
can have an instance of Monad
as well, and it turns out it can when the return type is any monad.
> instance Monad q => Monad (ICont q p) where
> return x = ICont (\_ -> return x)
> m >>= f = ICont (\k -> unICont m k >>= \x -> unICont (f x) k)
And, in fact, ICont
and Prompt
are also interconvertible when ICont
is polymorphic over any Monad
:
> to' :: Monad m => Prompt p a -> ICont m p a
> to' m = ICont (\k -> run k m)
>
> from' :: (forall m. Monad m => ICont m p a) -> Prompt p a
> from' m = unICont m prompt
This suggests an alternative implementation of Prompt
:
> newtype Prompt' p a = P' (forall m. Monad m => (p :-> m) -> m a)
ICont
is very similar to the generator type discussed in “Lazy v. Yield: Incremental, Linear Pretty-printing” by Oleg Kiselyov, Simon Peyton-Jones, and Amr Sabry:
> type GenT e m = ReaderT (e -> m ()) m
We can define a simple interface for generators,
> data Sink e i where Send :: e -> Sink e ()
and now ICont m (Sink e)
is isomorphic to GenT e m
.
> toGen :: ICont m (Sink e) :-> GenT e m
> toGen m = ReaderT (\f -> unICont m (\(Send e) -> f e))
>
> fromGen :: GenT e m :-> ICont m (Sink e)
> fromGen m = ICont (\k -> runReaderT m (k . Send))
In their paper, Kiselyov and the others contrast their simple generators with iteratees, noting that the latter effectively require “first-class, multi-shot delimited continuations.” Of course, GenT
can’t prevent the use of delimited continuations, unless it fixes the monad m
—at which point it is restricted to the effects that m
can express.
Similarly, Prompt
and Prompt'
are polymorphic in their effects, while ICont m
is limited to whatever effects m
can express. What’s interesting is that it doesn’t really matter which one you choose. If you go back to charRuns
and guardStream
and replace all the occurrences of prompt
with iskip
, the result is polymorphic over any IMonad
. That’s because the only operations Prompt
provides are those in Monad
and IMonad
—but that’s basically all you need.
Interpreters
A small framework for interpreting stateful effects in Prompt
.
> stateful :: (forall i. p i -> s -> (i,s))
> -> s -> Prompt p a -> a
> stateful op s m = unP m (\p k -> uncurry k . op p) const s
>
> lstateful :: (forall i. p i -> s -> (i,s))
> -> s -> Prompt (p :\/ q) a -> Prompt q a
> lstateful op s m = unP m
> ((\p k -> uncurry k . op p) \/ pass)
> (\a s -> return a)
> s
> where
> pass q k s = prompt q >>= flip k s
>
> state :: St s i -> s -> (i,s)
> state Get s = (s, s)
> state (Put s) _ = ((),s)
>
> stream :: Stream e i -> [e] -> (i,[e])
> stream SRead [] = (EOS, [])
> stream SRead (e:es) = (Chunk e, es)
>
> gstream :: GStream e i -> [e] -> (i,[e])
> gstream GReadAny [] = (EOS, [])
> gstream GReadAny (e:es) = (Chunk e, es)
> gstream (GReadOnly f) (e:es) | f e = (Just e, es)
> gstream (GReadOnly f) es = (Nothing, es)
Proof that
pmap t
is a monad morphism:
↩pmap t (m >>= f) = P (\c k -> unP (m >>= f) (c . t) k) = P (\c k -> unP m (c . t) (\a -> unP (f a) (c . t) k)) pmap t m >>= pmap t . f = P (\c k -> unP (pmap t m) c (\a -> unP (pmap t (f a)) c k)) = P (\c k -> unP (pmap t m) c (\a -> unP (f a) (c . t) k)) = P (\c k -> unP m (c . t) (\a -> unP (f a) (c . t) k))
Also, UP is a comonad in M.↩
In the real implementation,
Chunk
also has the capacity to report errors, so it isn’t isomorphic toMaybe
.↩