ZedneWeb
Punny titles a specialty

Prompt Monads are Free

Friday, June 7, 2013, at 10:18 PM

Summary: A brief look at Prompt monads, showing that they are free monads, that Prompt is a monad over indexed types, and how it can be used to build composable components.

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
>

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 : MI 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 : IM.

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 : TU M and monad morphisms g : P TM, 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 : UPUPUP

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)

1. 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))
2. Also, UP is a comonad in M.

3. In the real implementation, Chunk also has the capacity to report errors, so it isn’t isomorphic to Maybe.