Monads for Functional Programming

Reference: Wadler, Philip. "Monads for functional programming." Advanced Functional Programming (1995): 24-52.

0. Abstract

The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.

1. Introduction

  • Pure Language: such as Miranda and Haskell, are easier to reason about and may benefit from lazy evaluation.
  • Impure Languages: such as Scheme** and *Standard ML, offer efficiency benefits and sometimes make possible a more compact mode of expression.
  • Recent advances in the areas of type theory and category theory, have suggested the use of monads to integrate impure effects into pure functional languages.

2. Evaluating Monads

  • One advantage of pure functional languages: all flow of data is made explicit. All data in and all data out are rendered manifest and accessible, providing a maximum of flexibility;
  • However, the essence of an algorithm can become buried under the plumbing required to carry data from its point of creation to its point of use.

2.1 Variation Zero: the Basic Evaluator

data Term = Con Int | Div Term Term

eval :: Term -> Int
eval (Con a) = a
eval (Div t u) = (eval t) / (eval u)

2.2 Variation One: Exceptions

Goal: add error checking

data M a = Raise Exception | Return a
type Exception = String

eval :: Term -> M Int
eval (Con a) = Return a
eval (Div t u) = case eval t of
                    Raise e -> Raise e
                    Return a ->
                        case eval u of
                            Raise e -> Raise e
                            Return b ->
                                if b == 0
                                    then Raise "divide by zero"
                                    else Return (a / b)

2.3 Variation Two: State

Goal: count the number of divisions performed during evaluation

type M a = State -> (a, State)
type State = Int

eval :: Term -> M Int
eval (Con a) x = (a, x)
eval (Div t u) x = let (a, y) = eval t x in
                   let (b, z) = eval u y in
                   (a / b, z + 1)

2.4 Variation Three: Output

Goal: display a trace of execution

type M a = (Output, a)
type Output = String

eval :: Term -> M Int
eval (Con a) = (line (Con a) a, a)
eval (Div t u) = let (x, a) = eval t in
                 let (y, b) = eval u in
                 (x ++ y ++ line (Div t u)(a / b), a / b)

line :: Term -> Int -> Output
line t a = "eval(" ++ show t ++ ") <=" ++ show a ++ "\n"

2.5 A Monadic Evaluator

Introducing Monad

  • In general, by introducing monad, a function of type a->b is replaced by a function of type a->M b. This can be read as a function that accepts an argument of type a and returns a result of type b, with a possible additional effect captured by M.
  • Two sorts of operations are required on the type M: (1) a way to turn a value into the computation that returns that value and does nothing else unit :: a -> M a (2) a way to apply a function of type a a -> M b to a computation of type M a. It is convenient to write these in an order where the argument comes before the function (*) :: M a -> (a -> M b) -> M b
  • A monad is a triple (M, unit, *) consisting of a type constructor M and two operations of the given polymorphic types(these operations must satisfy three laws given in Section 3).

Lambda Calculus of Monad

We will often write expressions in the form

where m and n are expressions, and a is a variable. The form is a lambda expression, with the scope of the bound variable a being the expression n. The above can be read as follows: perform computation m, bind a to the resulting value, and then perform computation n. The above is analogous to the expression let a = m in n.

eval :: Term -> M Int
eval (Con a) = unit a
eval (Div t u) = eval t * \a -> eval u * \b -> unit (a / b)

2.6 Variation Zero, Revisited: The Basic Evaluator

Simplest Monad(identity monad): a computation is no different from a value. M is the identity function on types, unit is the identity function, and * is just application. Taking these in the monadic evaluator of Section 2.5 and simplifying yields the basic evaluator of Section 2.1.

type M a = a
unit :: a -> I a
unit a = a
(*) :: M a -> (a -> M b) -> M b
a * k = k a

2.7 Variation One, Revisited: Exceptions

data M a = Raise Exception | Return a
type Exception = String

unit :: a -> M a
unit a = Return a

(*) :: M a -> (a -> M b) -> M b
m * k = case m of
            Raise e -> Raise e
            Return a -> k a

raise :: Exception -> M a
raise e = Raise e

Replace unit (a / b) by

if b == 0
    then raise "divide by zero"
    else unit (a / b)

This evaluator is equivalent to the evaluator with exceptions of Section 2.2.

2.8 Variation Two, Revisited: State

type M a = State -> (a, State)
type State = Int

unit :: a -> M a
unit a = \x -> (a, x)

(*) :: M a -> (a -> M b) -> M b
m * k = \x let (a, y) = m x in
           let (b, z) = k a y in
           (b, z)

tick :: M ()
tick = \x -> ((), x + 1)

Replace unit (a / b) by

tick * (\x -> unit (a / b))

This evaluator is equivalent to the evaluator with exceptions of Section 2.3.

2.9 Variation Three, Revisited: Output

type M a = (Output, a)
type Output = String

unit :: a -> M a
unit a = ("", a)

(*) :: M a -> (a -> M b) -> M b
m * k = let (x, a) = m in
        let (y, b) = k a in
        (x ++ y, b)

out :: Output -> M ()
out x = (x, ())

With some modifications, this evaluator can be equivalent to the evaluator with exceptions of Section 2.4.

3. Monad Laws

  • Left unit. Compute the value a, bind b to the result, and compute n. The result is the same as n with value a substituted for variable b.
  • Right unit. Compute m, bind the result to a, and return a. The result is the same as m.
  • Associate. Compute m, bind the result to a, compute n, bind the result to b, compute o. The order of parentheses in such a computation is irrelevant. The scope of the variable a includes o on the left but excludes o on the right, so this law is valid only when a does not appear free in o.

A binary operation with left and right unit that is associative is called a monoid. A monad differs from a monoid in that the right operand involves a binding operation.

map :: (a -> b) -> (M a -> M b)
map f m = m * \a -> unit (f a)

join :: M (M a) -> M a
join z = z * \m -> m

4. State

4.1 Arrays

Let Arr be the type of arrays taking indexes of type Ix and yielding values of type Val. The key operations on this type are

newarray :: Val -> Arr
index :: Ix -> Arr -> Val
update :: Ix -> Val -> Arr -> Arr
  • Single Threaded: An array satisfying the property that there are no other pointers to an array extant.
  • In order for this to work, the update operation must evaluate the new value before placing it in the array. Otherwise, the array may contain a closure that itself contains a pointer to the array, violating the single threading property.
  • In semantic terms, one says that update is strict in all three of its arguments.

4.2 Array Transformers

type M a = State -> (a, State)
type State = Arr

unit :: a -> M a
unit a = \x -> (a, x)

(*) :: M a -> (a -> M b) -> M b
m * k = \x -> let (a, y) = m x in
              let (b, z) = k a y in
              (b, z)

block :: Val -> M a -> a
block v m = let (a, x) = m (newarray v) in a

fetch :: Ix -> M Val
fetch i = \x -> (index i x, x)

assign :: Ix -> Val -> M ()
assign i v = \x -> ((), update i v x)

4.3 Array Readers

type M' a = State -> a
type State = Arr

unit' :: a -> M' a
unit' a = \x -> a

(*') :: M' a -> (a -> M' b) -> M' b
m *' k = \x -> let a = m x in k a x

fetch' :: Ix -> M' Val
fetch' i = \x -> index i x

coerce :: M' a -> M a
coerce m = \x -> let a = m x in (a, x)

A monad morphism from a monad M’ to a monad M is a function h :: M’ a -> M a that preserves the monad structure:

5. Parsers

5.1 Lists

Lists form a monad:

unit :: a -> [a]
unit a = [a]

(*) :: [a] -> (a -> [b]) -> [b]
[] * k = []
(a : x) * k = k a ++ (x * k)

5.2 Representing Parsers

type M a = State -> [(a, State)]
type State = String

data Term = Con Int | Div Term Term

term :: M Term

A parser m is unambiguous if for every input x the list of possible parses m x is either empty or has exactly one item.

5.3 Parsing an Item

item :: M Char
item [] = []
item (a:x) = [(a, x)]

Clearly, item is unambiguous.

5.4 Sequencing

unit :: a -> M a
unit a x = [(a, x)]

(*) :: M a -> (a -> M b) -> M b
(m * k) x = [(b, z) |(a, y) <- m x, (b, z) <- k a y]

if m is unambiguous and k a is unambiguous for every a, them m * k is also unambiguous.

5.5 Alternation

zero :: M a
zero x = []

() :: M a -> M a -> M a
(m  n) x = m x ++ n x

5.6 Filtering

() :: M a -> (a -> Bool) -> M a
m  p = m * \a -> if p a then unit x else zero

5.7 Iteration

iterate :: M a -> M [a]
iterate m = (m * \a -> iterate (m * \x -> unit (a : x))) + unit []

5.8 Biased Choice

bias :: M a -> M a -> M a
(m bias' n) x = if m x /= [] then m x else n x

reiterate :: M a -> M [a]
reiterate m = (m * \a -> reiterate (m * \x -> unit (a : x))) bias' unit []

5.9 A Parser for Terms

Parser1

5.10 Left Recursion

Parser2

Any attempt to apply term results in an infinite loop, as the problem is that the first step of term to apply term, leading to an infinite regress, which is called the left recursion problem. It is a difficulty for all recursive descent parsers, functional or otherwise.

New Parser

Parser3

In general, the left-recursive definition

can be rewritten as

where

closure :: (a -> M a) -> (a -> M a)
closure k a = (k a * closure k)  unit a

5.11 Improving Laziness

guarantee :: M a -> M a
guarantee m x = let u = m x in (fst (head u), snd (head u)) : tail u

reiterate :: M a -> M [a]
reiterate m = guarantee ((m * \a -> reiterate (m * \x -> unit (a : x))) bias' unit [])

This ensures that reiterate m and all of its recursive calls return a list with at least one answer. As a result, the behavior under lazy evaluation is much improved.

Written on December 7, 2016