Modular and extensible effects in Haskell

Monadic effects

What is a monad?

Type constructor with unit (return) and bind (>>=),

class Monad (m :: * -> *) where
  return :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b

satisfying the following laws:

return x >>= f == f x
m >>= return == m
(m >>= f) >>= g == m >>= (\ x -> f x >>= g)

Computational effects can be modelled as monads

• Example 1: State Int

increment :: State Int ()
increment = do
  x <- get
  put $ x+1

• Example 2: IO

main :: IO ()
main = do
  putStrLn $ "What is your name?"
  x <- getLine
  putStrLn $ "Hello, " ++ x ++ "!"

More than one monad?

• The underlying functors compose!

  State s (Maybe (IO a))

• How to deal with these "stacks" in a uniform way?

Monad transformers

Monads with a "hole" for another monad

Values in the inner monad can be lifted to the outer

class MonadTrans (f :: (* -> *) -> * -> *) where
  lift :: Monad m => m a -> t m a

lift must respect return and >>=

lift . return = return
lift (m >>= f) = lift m >>= (lift . f)

Monad transformers

Examples

newtype MaybeT m a = MaybeT {runMaybeT :: m (Maybe a)}

instance MonadTrans MaybeT where
  lift = MaybeT . liftM Just

type Maybe a = MaybeT Identity a

newtype StateT s m a = StateT {runStateT :: s -> m (a, s)}

instance MonadTrans (StateT s) where
  lift m = StateT $ \ s -> do
    a <- m
    return (a, s)

type State s a = StateT s Identity a

Order is relevant!

We have

StateT s Maybe a ≠ MaybeT (State s) a

because

s -> Maybe (s , a) ≠ s -> (s , Maybe a)

Monadic programming: software engineering concerns

Issue 1: modularity

Monolithic effects

data TheMonadOfMyApp a =
  TheMonadOfMyApp (MyState -> (IO (MyLog , MyState , a)))

instance Monad TheMonadOfMyApp where
  ...

justSayHello :: TheMonadOfMyApp ()
justSayHello = TheMonadOfMyApp $ \ db -> do
  putStrLn $ "Hello!"
  return ("Just said hello!" , db , ())

main :: IO ()
main = runTheMonadOfMyApp initialState $ do
  justSayHello
  ...

Issue 1: modularity

We would prefer

justSayHello :: StdOutput ()
justSayHello = putStrLn "Hello!"

or

justSayHello :: StdOutput m => m ()
justSayHello = putStrLn "Hello!"

Issue 2: extensibility

It should also be easy to add a new effect to our "vocabulary"

There should be no need to

• change the types of previous code
• relate the new effect to the previously defined effects

Thesis

Use type classes to capture monadic interfaces

Monad Transformer Library

standard monad transformers

+

type classes with their abstract interfaces

See Jones 1995

Example: MonadState

increment :: State Int ()
increment = do
  x <- get
  put $ x+1

becomes

increment :: MonadState Int m => m ()
increment = do
  x <- get
  put $ x+1

Example: MonadIO

main :: IO ()
main = do
  putStrLn $ "What is your name?"
  x <- getLine
  putStrLn $ "Hello, " ++ x ++ "!"

becomes

main :: MonadIO m => m ()
main = do
  putStrLn $ "What is your name?"
  x <- getLine
  putStrLn $ "Hello, " ++ x ++ "!"

Problem: Cannot have many State s in the stack

Due to functional dependency!

class Monad m => MonadState s m | m -> s where
  get :: m s
  put :: s -> m ()

If you omit | m -> s, you need OverlappingInstances

Same for MonadReader and MonadWriter.

Problem: Order

• The order of effects counts!
• However, we cannot constrain the order of the abstract ones.
• How to read program?

program :: (MonadError () m , MonadState s m) => m ()

Problem: Poor extensibility

To add the (n+1)-th monad transformer,

we must give n instances.

lift is extremely ad hoc!

Antithesis

Represent effectful programs as modular syntax

Handlers interpret syntax as monads

Free Monad

A datatype parameterised by a f :: * -> * operator

data Free f a =
    Return a
  | Free (f (Free f a))

When f is a Functor, Free f is a Monad !

instance Functor f => Monad (Free f) where
  return = Return
  (Return a) >>= f = f a
  (Free  xs) >>= f = Free (fmap (>>= f) xs)

We use Free a as a generic representation for monadic computations

What is Free f?

• Example: Take f = Arithmetics

  data Arithmetics a =
      Val Int
    | Plus a a
    deriving Functor
  

• Free Arithmetics x represents expressions made from
  • integer values
  • binary operator +
  • variables from the set x

What is Free f?

Take Vars as the type of two "variables" x and y

data Vars = varX | varY

x + (2 + y) is captured by

Free (Plus (return varX)
           (Free (Plus (Val 2)
                       (return varY))))

Monadic operations:

• return x is an occurrence of variable x
• >>= is substitution

Datatypes à la carte [W. Swierstra, 2008]

A simple notion of subtyping between functors:

data (f :+: g) e = Inl (f e) | Inr (g e)

class (Functor sub, Functor sup) => (:<:) sub sup where
  inj :: sub a -> sup a

instance (Functor f, Functor g, Functor h, f :<: g) => f :<: (g :+: h) where
  inj = Inl

instance (Functor f, Functor g, Functor h, f :<: h) => f :<: (g :+: h) where
  inj = Inr

Not real Haskell: original version has restrictions

See also Wadler 2008 (blog), Bahr 2014 (slides)

Handlers

• Take m as the target monad

• A handler for the effect f is a function of type:

  forall a. f (m a) -> m a

• Let's fix m = IO as target

class Functor f => Handler f where
  handler :: forall a. f (IO a) -> IO a

Example: Teletype + FileSystem

Effects

data Teletype a =
    GetChar (Char -> a)
  | PutChar Char a
  deriving Functor

data FileSystem a =
    ReadFile  FilePath (String -> a)
  | WriteFile FilePath String a
  deriving Functor

Primitives

getChar   :: Teletype   :<: f => Free f Char
putChar   :: Teletype   :<: f => Char -> Free f ()
readFile  :: FileSystem :<: f => FilePath -> Free f String
writeFile :: FileSystem :<: f => FilePath -> String -> Free f ()

getChar = GetChar Return
putChar c = PutChar c $ Return ()
readFile fp = ReadFile fp Return
writeFile fp s = WriteFile fp s $ Return ()

Example: Teletype + FileSystem

Example program: UNIX cat

cat :: FilePath -> Free (Teletype :+: FileSystem) ()
cat fp = readFile fp >>= mapM_ putChar

(Alternative type for the same program)

cat :: (Teletype :<: f , FileSystem :<: f) => FilePath -> Free f ()

Example: Teletype + FileSystem

Handlers

instance Handler Teletype where
  handler (GetChar   f) = Prelude.getChar >>= f
  handler (PutChar c m) = Prelude.putChar x >> m

instance Handle FileSystem where
  handler (ReadFile  fp   f) = Prelude.readFile fp >>= f
  handler (WriteFile fp s m) = Prelude.writeFile fp s >> m

Modularity!

Handler for the sum of two effects, given the single handlers

instance (Handler f, Handler g) => Handler (f :+: g) where
  handler (Inl x) = handler x
  handler (Inr y) = handler y

A generic evaluator for effectful programs

handle :: Handler f => Free f a -> IO a
handle (Return a) = return a
handle (Pure  xs) = handle (fmap handle xs)

Example: running the cat program in the IO monad

main :: IO ()
main = handle cat

Extensibility?

Easy to define a new effect!

However, extending the target monad is not considered.

E.g.: with IO as target monad, how to interpret State s?

data State s a =
    Get (s -> State s a)
  | Put s (State s a)

Without unsafe tricks, IO a cannot manage a state of type s!

Left-nested applications of ++

Intuitively,

(xs ++ ys) ++ zs takes |xs| + (|xs| + |ys|) steps

while

xs ++ (ys ++ zs) takes |xs| + |ys| steps.

Consequence: reverse via ++ is \(O(n^2)\) instead of \(O(n)\).

Left-nested applications of Free.>>=

Similarly, for Free

(m >>= f) >>= g

is slower than

m >>= (\ x -> f x >>= g)

[Voigtländer 2008] shows examples of affected algorithms.

Higher-order free-monadic programs become problematic!

Solutions

• Unimo [Chuan-kai Lin 2006]
• Codensity [Voigtländer 2008]
• Continuation [KammarLindleyOury 2013]
• Freer [KiselyovIshii 2015]
• …

(details)

Synthesis

Use type classes and type families to capture monadic interfaces

Modularity

• Type families and constraint kinds allow "microeffects":

class Monad m => Get a m where
  get :: m a

class Monad m => Put a m where
  put :: a -> m ()

type family State (a :: *) (m :: * -> *) :: Constraint
type instance State a m = (Get a m , Put a m)

class Monad m => Input m where
  input :: m String
class Monad m => Output m where
  output :: String -> m ()

type family InputOutput (m :: * -> *) :: Constraint
type instance InputOutput m = (Input m , Output m)

• Doing this with a class definition seems to require

UndecidableInstances

• Not sure about where to mention laws, though!

Modularity

Example usage:

inputAmount :: Input m => m (Maybe Amount)
inputAmount = liftM readMaybe input

deposit :: (InputOutput m , Put Amount m) => m ()
deposit = do
  x <- untilJust $ do
    output "Enter the amount you want to store:"
    inputAmount
  put x
  output "Goodbye!"

An interesting library

• monad-classes by Roman Cheplyaka
• blog
• code
• Used in production at Signal Vine
• No theoretical treatment (yet)
• Similar: extensible-transformers

monad-classes: Extensibility

• Finding a transformer in a stack, with type families

type family Find (t :: (* -> *) -> (* -> *)) (m :: * -> *) :: Nat where
  Find t (t m) = Zero
  Find t (p m) = Suc (Find t m)

monad-classes: Extensibility

• Example: lifting Reader's ask to any transformer stack

class Monad m => MonadReaderN (n :: Nat) r m where
  askN :: Proxy n -> m r

instance Monad m => MonadReaderN Zero r (ReaderT r m) where
  askN _ = Trans.ask

instance (MonadTrans t, Monad (t m), MonadReaderN n r m, Monad m) =>
         MonadReaderN (Suc n) r (t m) where
  askN _ = lift $ askN (Proxy :: Proxy n)

type MonadReader r m = MonadReaderN (Find (ReaderT r) m) r m

ask :: forall m r . MonadReader r m => m r
ask = askN (Proxy :: Proxy (Find (ReaderT r) m))

monad-classes: Extensibility

• Quadratic number of instances, no more!
• No functional dependencies -> may have several State s
• You can use newtypes for s to distinguish their roles

monad-classes: CanDo

type family CanDo (m :: (* -> *)) (eff :: k) :: Bool

• Allows the lifting to be independent of specific transformers
• We can lift to effects which are more general than those requested
• e.g.: StateT generalises both ReaderT and WriterT
• See http://ro-che.info/ for more.

Why is this a synthesis?

• Consider the syntactic constructions

  Free, Operational, Unimo, Freer …

• You might want to use them for your project!
• However, have your syntax instantiate the abstract interfaces:

instance (Teletype :<: f) => Input (Free f) where
  input = getChar
instance (Teletype :<: f) => Output (Free f) where
  output = putChar
instance (FileSystem :<: f) => ReadFile (Free f) where
  readFile = FileSystem.readFile
instance (FileSystem :<: f) => WriteFile (Free f) where
  writeFile = FileSystem.writeFile

Why is this a synthesis?

• Then, write programs with abstract types

cat :: (Output m , ReadFile m) => FilePath -> m ()
cat fp = readFile fp >>= mapM_ output

• Pick a concrete representation only at the very end

main :: IO ()
main = handle cat

(Remember that handle :: Handler f => Free f a -> IO a)

Warning!

• I did not test this
• It probably needs more annotations
• It might prevent some optimisations

Conclusions

Datatypes à la Carte, Handlers in Action, Freer…

• Important connections with theory
• Performance oddities not unlikely
  • freemonad-benchmark
  • [KiselyovIshii 2015]
• Still, free-monadic code can be analysed by other programs
  • optimising interpreters or compilers!
  • e.g.: Haxl

MTL, monad-classes, (finally-tagless), …

• Monad stacks are inevitable in Haskell
• Maybe also monad transformer stacks
• People will use their own
  • HisApp x y
  • TheirFramework a b c d
• Better make an effort to keep effects abstract

Gang of Four, 1995

"Program to an 'interface', not an 'implementation'."

QA

Grazie!

More …

… on monad transformers

Monatron

• solves some problems
• requires more structure:

class MonadT t where
  lift    :: Monad m => m a -> t m a
  treturn :: Monad m => a -> t m a
  tbind   :: Monad m => t m a -> (a -> t m b) -> t m b

… on "free" effects

Effects, syntactically

The syntactic State monad

data State s x =
    Return x
  | Get (s -> State s x)
  | Put s (State s x)

instance Monad State where
  return = Return
  (Get k  ) >>= f = Get (\ s -> k s >>= f)
  (Put s x) >>= f = Put s (x >>= f)

handle :: State s x -> s -> (s , x)
handle (Return x  ) s = (s , x)
handle (Get    f  ) s = handle (f s) s
handle (Put    s x) _ = handle

Effects, syntactically

Programs in the syntactic State monad

get :: State s s
get = Get (\ s -> Return s)

put :: State s ()
put s = Put s (Return ())

increment :: State Int ()
increment = get >>= put . (+1)

Problem: syntactic State is not modular!

We need a more generic representation

… on faster free monadic computations

Alternative free monad: Operational

data Operational f a where
    Return :: a -> Operational f a
    Then   :: forall a. f a -> (a -> Operational f b) -> Operational f b

By Parametricity, Operational f a is isomorphic to Free f a

1. Unimo [Chuan-kai Lin 2006]

data Unimo f a =
    Return a
  | Free (f (Free f a))
  | forall b. Bind (Unimo f b) (b -> Unimo f a)

• Not really a monad
  • You must restrict observations
  • See also Uustalu 2012, Jaskelioff 2015
• Easy to use and understand
• (The operational package adds Bind internally)

2. Codensity [Voigtländer 2008]

• Codensity transformation

newtype Codensity f a = Codensity (forall r. (a -> f r) -> f r)

• Yoneda lemma implies this isomorphism:

rep :: Monad m => Codensity m a -> m a
abs :: Monad m => m a -> Codensity m a

• If you use Codensity (Free f) instead of Free f:

  (m >>= f) >>= g reduces to (almost) m >>= \ x -> f x >>= g

  before m, f and g are evaluated!

• Related to CPS transformation

6. Continuation [KammarLindleyOury 2013]

• One of three alternative representations for "Handlers in Action"
• Ad-hoc continuation monad
• No recursive datatypes, no tags
• If I understood correctly, similar to "Going to Church"
• More extensible than Datatypes à la Carte
• Template Haskell 😟

9. Freer [KiselyovIshii 2015]

• Based on Operational
• No :+: and :<:, but
  • Union r v :: *
    • where r is a type-level list of "effect labels"
    • and v is the type of "variables"
  • Member f r :: Constraint
• Precedence between handlers counts!
  • No functor algebras
  • Each handler relays on the next
  • Easier to extend target monad!

9. Freer [KiselyovIshii 2015]

• Interesting optimisation [KiselyovVanDerPloeg 2014]

  Recall Operational:

  data Operational f a where
    Return :: a -> Operational f a
    Then :: forall a. f a -> (a -> Operational f b) -> Operational f b
  

  In Freer, (a -> Operational f b) is "reified" as an efficient heterogeneous sequence of continuations (fast append!)

• No algebras -> more extensible than Datatypes à la Carte