Sunday, August 10, 2014

managed-1.0.0: A monad for managed resources

I'm splitting off the Managed type from the mvc library into its own stand-alone library. I've wanted to use this type outside of mvc for some time now, because it's an incredibly useful Applicative that I find myself reaching for in my own code whenever I need to acquire resources.

If you're not familiar with the Managed type, it's simple:

-- The real implementation uses smart constructors
newtype Managed a =
    Managed { with :: forall r . (a -> IO r) -> IO r }

-- It's a `Functor`/`Applicative`/`Monad`
instance Functor     Managed where ...
instance Applicative Managed where ...
instance Monad       Managed where ...

-- ... and also implements `MonadIO`
instance MonadIO Managed where ...

Here's an example of mixing the Managed monad with pipes to copy one file to another:

import Control.Monad.Managed
import System.IO
import Pipes
import qualified Pipes.Prelude as Pipes

main = runManaged $ do
    hIn  <- managed (withFile "in.txt" ReadMode)
    hOut <- managed (withFile "out.txt" WriteMode)
    liftIO $ runEffect $
        Pipes.fromHandle hIn >-> Pipes.toHandle hOut

However, this is not much more concise than the equivalent callback-based version. The real value of the Managed type is its Applicative instance, which you can use to lift operations from values that it wraps.

Equational reasoning

My previous post on equational reasoning at scale describes how you can use Applicatives to automatically extend Monoids while preserving the Monoid operations. The Managed Applicative is no different and provides the following type class instance that automatically lifts Monoid operations:

instance Monoid a => Monoid (Managed a)

Therefore, you can treat the Managed Applicative as yet another useful building block in your Monoid tool box.

However, Applicatives can do more than extend Monoids; they can extend Categorys, too. Given any Category, if you extend it with an Applicative you can automatically derive a new Category. Here's the general solution:

import Control.Applicative
import Control.Category 
import Prelude hiding ((.), id)

newtype Extend f c a b = Extend (f (c a b))

instance (Applicative f, Category c)
  => Category (Extend f c) where
    id = Extend (pure id)

    Extend f . Extend g = Extend (liftA2 (.) f g)

So let's take advantage of this fact to extend one of the pipes categories with simple resource management. All we have to do is wrap the pull-based pipes category in a bona-fide Category instance:

import Pipes

newtype Pull m a b = Pull (Pipe a b m ()) 

instance Monad m => Category (Pull m) where
    id = Pull cat

    Pull p1 . Pull p2 = Pull (p1 <-< p2)

Now we can automatically define resource-managed pipes by Extending them with the Managed Applicative:

import Control.Monad.Managed
import qualified Pipes.Prelude as Pipes
import System.IO

fromFile :: FilePath -> Extend Managed (Pull IO) () String
fromFile filePath = Extend $ do
    handle <- managed (withFile filePath ReadMode)
    return (Pull (Pipes.fromHandle handle))

toFile :: FilePath -> Extend Managed (Pull IO) String X
toFile filePath = Extend $ do
    handle <- managed (withFile filePath WriteMode)
    return (Pull (Pipes.toHandle handle))

All we need is a way to run Extended pipes and then we're good to go:

runPipeline :: Extend Managed (Pull IO) () X -> IO ()
runPipeline (Extend mp) = runManaged $ do
    Pull p <- mp
    liftIO $ runEffect (return () >~ p)

If we compose and run these Extended pipes they just "do the right thing":

main :: IO ()
main = runPipeline (fromFile "in.txt" >>> toFile "out.txt")

Let's check it out:

$ cat in.txt
1
2
3
$ ./example
$ cat out.txt
1
2
3

We can even reuse existing pipes, too:

reuse :: Monad m => Pipe a b m () -> Extend Managed (Pull m) a b
reuse = Extend . pure . Pull

main = runPipeline $
    fromFile "in.txt" >>> reuse (Pipes.take 2) >>> toFile "out.txt"

... and reuse does the right thing:

$ ./example
$ cat out.txt
1
2

What does it mean for reuse to "do the right thing"? Well, we can specify the correctness conditions for reuse as the following functor laws:

reuse (p1 >-> p2) = reuse p1 >>> reuse p2

reuse cat = id

These two laws enforce that reuse is "well-behaved" in a rigorous sense.

This is just one example of how you can use the Managed type to extend an existing Category. As an exercise, try to take other categories and extend them this way and see what surprising new connectable components you can create.

Conclusion

Experts will recognize that Managed is a special case of Codensity or ContT. The reason for defining a separate type is:

  • simpler inferred types,
  • additional type class instances, and:
  • a more beginner-friendly name.

Managed is closely related in spirit to the Resource monad, which is now part of resourcet. The main difference between the two is:

  • Resource preserves the open and close operations
  • Managed works for arbitrary callbacks, even unrelated to resources

This is why I view the them as complementary Monads.

Like all Applicatives, the Managed type is deceptively simple. This type does not do much in isolation, but it grows in power the more you compose it with other Applicatives to generate new Applicatives.

Sunday, July 20, 2014

Equational reasoning at scale

Haskell programmers care about the correctness of their software and they specify correctness conditions in the form of equations that their code must satisfy. They can then verify the correctness of these equations using equational reasoning to prove that the abstractions they build are sound. To an outsider this might seem like a futile, academic exercise: proving the correctness of small abstractions is difficult, so what hope do we have to prove larger abstractions correct? This post explains how to do precisely that: scale proofs to large and complex abstractions.

Purely functional programming uses composition to scale programs, meaning that:

  • We build small components that we can verify correct in isolation
  • We compose smaller components into larger components

If you saw "components" and thought "functions", think again! We can compose things that do not even remotely resemble functions, such as proofs! In fact, Haskell programmers prove large-scale properties exactly the same way we build large-scale programs:

  • We build small proofs that we can verify correct in isolation
  • We compose smaller proofs into larger proofs

The following sections illustrate in detail how this works in practice, using Monoids as the running example. We will prove the Monoid laws for simple types and work our way up to proving the Monoid laws for much more complex types. Along the way we'll learn how to keep the proof complexity flat as the types grow in size.

Monoids

Haskell's Prelude provides the following Monoid type class:

class Monoid m where
    mempty  :: m
    mappend :: m -> m -> m

-- An infix operator equivalent to `mappend`
(<>) :: Monoid m => m -> m -> m
x <> y = mappend x y

... and all Monoid instances must obey the following two laws:

mempty <> x = x                -- Left identity

x <> mempty = x                -- Right identity

(x <> y) <> z = x <> (y <> z)  -- Associativity

For example, Ints form a Monoid:

-- See "Appendix A" for some caveats
instance Monoid Int where
    mempty  =  0
    mappend = (+)

... and the Monoid laws for Ints are just the laws of addition:

0 + x = x

x + 0 = x

(x + y) + z = x + (y + z)

Now we can use (<>) and mempty instead of (+) and 0:

>>> 4 <> 2
6
>>> 5 <> mempty <> 5
10

This appears useless at first glance. We already have (+) and 0, so why are we using the Monoid operations?

Extending Monoids

Well, what if I want to combine things other than Ints, like pairs of Ints. I want to be able to write code like this:

>>> (1, 2) <> (3, 4)
(4, 6)

Well, that seems mildly interesting. Let's try to define a Monoid instance for pairs of Ints:

instance Monoid (Int, Int) where
    mempty = (0, 0)
    mappend (x1, y1) (x2, y2) = (x1 + x2, y1 + y2)

Now my wish is true and I can "add" binary tuples together using (<>) and mempty:

>>> (1, 2) <> (3, 4)
(4, 6)
>>> (1, 2) <> (3, mempty) <> (mempty, 4)
(4, 6)
>>> (1, 2) <> mempty <> (3, 4)
(4, 6)

However, I still haven't proven that this new Monoid instance obeys the Monoid laws. Fortunately, this is a very simple proof.

I'll begin with the first Monoid law, which requires that:

mempty <> x = x

We will begin from the left-hand side of the equation and try to arrive at the right-hand side by substituting equals-for-equals (a.k.a. "equational reasoning"):

-- Left-hand side of the equation
mempty <> x

-- x <> y = mappend x y
= mappend mempty x

-- `mempty = (0, 0)`
= mappend (0, 0) x

-- Define: x = (xL, xR), since `x` is a tuple
= mappend (0, 0) (xL, xR)

-- mappend (x1, y1) (x2, y2) = (x1 + x2, y1 + y2)
= (0 + xL, 0 + xR)

-- 0 + x = x
= (xL, xR)

-- x = (xL, xR)
= x

The proof for the second Monoid law is symmetric

-- Left-hand side of the equation
= x <> mempty

-- x <> y = mappend x y
= mappend x mempty

-- mempty = (0, 0)
= mappend x (0, 0)

-- Define: x = (xL, xR), since `x` is a tuple
= mappend (xL, xR) (0, 0)

-- mappend (x1, y1) (x2, y2) = (x1 + x2, y1 + y2)
= (xL + 0, xR + 0)

-- x + 0 = x
= (xL, xR)

-- x = (xL, xR)
= x

The third Monoid law requires that (<>) is associative:

(x <> y) <> z = x <> (y <> z)

Again I'll begin from the left side of the equation:

-- Left-hand side
(x <> y) <> z

-- x <> y = mappend x y
= mappend (mappend x y) z

-- x = (xL, xR)
-- y = (yL, yR)
-- z = (zL, zR)
= mappend (mappend (xL, xR) (yL, yR)) (zL, zR)

-- mappend (x1, y1) (x2 , y2) = (x1 + x2, y1 + y2)
= mappend (xL + yL, xR + yR) (zL, zR)

-- mappend (x1, y1) (x2 , y2) = (x1 + x2, y1 + y2)
= mappend ((xL + yL) + zL, (xR + yR) + zR)

-- (x + y) + z = x + (y + z)
= mappend (xL + (yL + zL), xR + (yR + zR))

-- mappend (x1, y1) (x2, y2) = (x1 + x2, y1 + y2)
= mappend (xL, xR) (yL + zL, yR + zR)

-- mappend (x1, y1) (x2, y2) = (x1 + x2, y1 + y2)
= mappend (xL, xR) (mappend (yL, yR) (zL, zR))

-- x = (xL, xR)
-- y = (yL, yR)
-- z = (zL, zR)
= mappend x (mappend y z)

-- x <> y = mappend x y
= x <> (y <> z)

That completes the proof of the three Monoid laws, but I'm not satisfied with these proofs.

Generalizing proofs

I don't like the above proofs because they are disposable, meaning that I cannot reuse them to prove other properties of interest. I'm a programmer, so I loathe busy work and unnecessary repetition, both for code and proofs. I would like to find a way to generalize the above proofs so that I can use them in more places.

We improve proof reuse in the same way that we improve code reuse. To see why, consider the following sort function:

sort :: [Int] -> [Int]

This sort function is disposable because it only works on Ints. For example, I cannot use the above function to sort a list of Doubles.

Fortunately, programming languages with generics let us generalize sort by parametrizing sort on the element type of the list:

sort :: Ord a => [a] -> [a]

That type says that we can call sort on any list of as, so long as the type a implements the Ord type class (a comparison interface). This works because sort doesn't really care whether or not the elements are Ints; sort only cares if they are comparable.

Similarly, we can make the proof more "generic". If we inspect the proof closely, we will notice that we don't really care whether or not the tuple contains Ints. The only Int-specific properties we use in our proof are:

0 + x = x

x + 0 = x

(x + y) + z = x + (y + z)

However, these properties hold true for all Monoids, not just Ints. Therefore, we can generalize our Monoid instance for tuples by parametrizing it on the type of each field of the tuple:

instance (Monoid a, Monoid b) => Monoid (a, b) where
    mempty = (mempty, mempty)

    mappend (x1, y1) (x2, y2) = (mappend x1 x2, mappend y1 y2)

The above Monoid instance says that we can combine tuples so long as we can combine their individual fields. Our original Monoid instance was just a special case of this instance where both the a and b types are Ints.

Note: The mempty and mappend on the left-hand side of each equation are for tuples. The memptys and mappends on the right-hand side of each equation are for the types a and b. Haskell overloads type class methods like mempty and mappend to work on any type that implements the Monoid type class, and the compiler distinguishes them by their inferred types.

We can similarly generalize our original proofs, too, by just replacing the Int-specific parts with their more general Monoid counterparts.

Here is the generalized proof of the left identity law:

-- Left-hand side of the equation
mempty <> x

-- x <> y = mappend x y
= mappend mempty x

-- `mempty = (mempty, mempty)`
= mappend (mempty, mempty) x

-- Define: x = (xL, xR), since `x` is a tuple
= mappend (mempty, mempty) (xL, xR)

-- mappend (x1, y1) (x2, y2) = (mappend x1 x2, mappend y1 y2)
= (mappend mempty xL, mappend mempty xR)

-- Monoid law: mappend mempty x = x
= (xL, xR)

-- x = (xL, xR)
= x

... the right identity law:

-- Left-hand side of the equation
= x <> mempty

-- x <> y = mappend x y
= mappend x mempty

-- mempty = (mempty, mempty)
= mappend x (mempty, mempty)

-- Define: x = (xL, xR), since `x` is a tuple
= mappend (xL, xR) (mempty, mempty)

-- mappend (x1, y1) (x2, y2) = (mappend x1 x2, mappend y1 y2)
= (mappend xL mempty, mappend xR mempty)

-- Monoid law: mappend x mempty = x
= (xL, xR)

-- x = (xL, xR)
= x

... and the associativity law:

-- Left-hand side
(x <> y) <> z

-- x <> y = mappend x y
= mappend (mappend x y) z

-- x = (xL, xR)
-- y = (yL, yR)
-- z = (zL, zR)
= mappend (mappend (xL, xR) (yL, yR)) (zL, zR)

-- mappend (x1, y1) (x2 , y2) = (mappend x1 x2, mappend y1 y2)
= mappend (mappend xL yL, mappend xR yR) (zL, zR)

-- mappend (x1, y1) (x2 , y2) = (mappend x1 x2, mappend y1 y2)
= (mappend (mappend xL yL) zL, mappend (mappend xR yR) zR)

-- Monoid law: mappend (mappend x y) z = mappend x (mappend y z)
= (mappend xL (mappend yL zL), mappend xR (mappend yR zR))

-- mappend (x1, y1) (x2, y2) = (mappend x1 x2, mappend y1 y2)
= mappend (xL, xR) (mappend yL zL, mappend yR zR)

-- mappend (x1, y1) (x2, y2) = (mappend x1 x2, mappend y1 y2)
= mappend (xL, xR) (mappend (yL, yR) (zL, zR))

-- x = (xL, xR)
-- y = (yL, yR)
-- z = (zL, zR)
= mappend x (mappend y z)

-- x <> y = mappend x y
= x <> (y <> z)

This more general Monoid instance lets us stick any Monoids inside the tuple fields and we can still combine the tuples. For example, lists form a Monoid:

-- Exercise: Prove the monoid laws for lists
instance Monoid [a] where
    mempty = []

    mappend = (++)

... so we can stick lists inside the right field of each tuple and still combine them:

>>> (1, [2, 3]) <> (4, [5, 6])
(5, [2, 3, 5, 6])
>>> (1, [2, 3]) <> (4, mempty) <> (mempty, [5, 6])
(5, [2, 3, 5, 6])
>>> (1, [2, 3]) <> mempty <> (4, [5, 6])
(5, [2, 3, 5, 6])

Why, we can even stick yet another tuple inside the right field and still combine them:

>>> (1, (2, 3)) <> (4, (5, 6))
(5, (7, 9))

We can try even more exotic permutations and everything still "just works":

>>> ((1,[2, 3]), ([4, 5], 6)) <> ((7, [8, 9]), ([10, 11), 12)
((8, [2, 3, 8, 9]), ([4, 5, 10, 11], 18))

This is our first example of a "scalable proof". We began from three primitive building blocks:

  • Int is a Monoid
  • [a] is a Monoid
  • (a, b) is a Monoid if a is a Monoid and b is a Monoid

... and we connected those three building blocks to assemble a variety of new Monoid instances. No matter how many tuples we nest the result is still a Monoid and obeys the Monoid laws. We don't need to re-prove the Monoid laws every time we assemble a new permutation of these building blocks.

However, these building blocks are still pretty limited. What other useful things can we combine to build new Monoids?

IO

We're so used to thinking of Monoids as data, so let's define a new Monoid instance for something entirely un-data-like:

-- See "Appendix A" for some caveats
instance Monoid b => Monoid (IO b) where
    mempty = return mempty

    mappend io1 io2 = do
        a1 <- io1
        a2 <- io2
        return (mappend a1 a2)

The above instance says: "If a is a Monoid, then an IO action that returns an a is also a Monoid". Let's test this using the getLine function from the Prelude:

-- Read one line of input from stdin
getLine :: IO String

String is a Monoid, since a String is just a list of characters, so we should be able to mappend multiple getLine statements together. Let's see what happens:

>>> getLine  -- Reads one line of input
Hello<Enter>
"Hello"
>>> getLine <> getLine
ABC<Enter>
DEF<Enter>
"ABCDEF"
>>> getLine <> getLine <> getLine
1<Enter>
23<Enter>
456<Enter>
"123456"

Neat! When we combine multiple commands we combine their effects and their results.

Of course, we don't have to limit ourselves to reading strings. We can use readLn from the Prelude to read in anything that implements the Read type class:

-- Parse a `Read`able value from one line of stdin
readLn :: Read a => IO a

All we have to do is tell the compiler which type a we intend to Read by providing a type signature:

>>> readLn :: IO (Int, Int)
(1, 2)<Enter>
(1 ,2)
>>> readLn <> readLn :: IO (Int, Int)
(1,2)<Enter>
(3,4)<Enter>
(4,6)
>>> readLn <> readLn <> readLn :: IO (Int, Int)
(1,2)<Enter>
(3,4)<Enter>
(5,6)<Enter>
(9,12)

This works because:

  • Int is a Monoid
  • Therefore, (Int, Int) is a Monoid
  • Therefore, IO (Int, Int) is a Monoid

Or let's flip things around and nest IO actions inside of a tuple:

>>> let ios = (getLine, readLn) :: (IO String, IO (Int, Int))
>>> let (getLines, readLns) = ios <> ios <> ios
>>> getLines
1<Enter>
23<Enter>
456<Enter>
123456
>>> readLns
(1,2)<Enter>
(3,4)<Enter>
(5,6)<Enter>
(9,12)

We can very easily reason that the type (IO String, IO (Int, Int)) obeys the Monoid laws because:

  • String is a Monoid
  • If String is a Monoid then IO String is also a Monoid
  • Int is a Monoid
  • If Int is a Monoid, then (Int, Int) is also a `Monoid
  • If (Int, Int) is a Monoid, then IO (Int, Int) is also a Monoid
  • If IO String is a Monoid and IO (Int, Int) is a Monoid, then (IO String, IO (Int, Int)) is also a Monoid

However, we don't really have to reason about this at all. The compiler will automatically assemble the correct Monoid instance for us. The only thing we need to verify is that the primitive Monoid instances obey the Monoid laws, and then we can trust that any larger Monoid instance the compiler derives will also obey the Monoid laws.

The Unit Monoid

Haskell Prelude also provides the putStrLn function, which echoes a String to standard output with a newline:

putStrLn :: String -> IO ()

Is putStrLn combinable? There's only one way to find out!

>>> putStrLn "Hello" <> putStrLn "World"
Hello
World

Interesting, but why does that work? Well, let's look at the types of the commands we are combining:

putStrLn "Hello" :: IO ()
putStrLn "World" :: IO ()

Well, we said that IO b is a Monoid if b is a Monoid, and b in this case is () (pronounced "unit"), which you can think of as an "empty tuple". Therefore, () must form a Monoid of some sort, and if we dig into Data.Monoid, we will discover the following Monoid instance:

-- Exercise: Prove the monoid laws for `()`
instance Monoid () where
    mempty = ()

    mappend () () = ()

This says that empty tuples form a trivial Monoid, since there's only one possible value (ignoring bottom) for an empty tuple: (). Therefore, we can derive that IO () is a Monoid because () is a Monoid.

Functions

Alright, so we can combine putStrLn "Hello" with putStrLn "World", but can we combine naked putStrLn functions?

>>> (putStrLn <> putStrLn) "Hello"
Hello
Hello

Woah, how does that work?

We never wrote a Monoid instance for the type String -> IO (), yet somehow the compiler magically accepted the above code and produced a sensible result.

This works because of the following Monoid instance for functions:

instance Monoid b => Monoid (a -> b) where
    mempty = \_ -> mempty

    mappend f g = \a -> mappend (f a) (g a)

This says: "If b is a Monoid, then any function that returns a b is also a Monoid".

The compiler then deduced that:

  • () is a Monoid
  • If () is a Monoid, then IO () is also a Monoid
  • If IO () is a Monoid then String -> IO () is also a Monoid

The compiler is a trusted friend, deducing Monoid instances we never knew existed.

Monoid plugins

Now we have enough building blocks to assemble a non-trivial example. Let's build a key logger with a Monoid-based plugin system.

The central scaffold of our program is a simple main loop that echoes characters from standard input to standard output:

main = do
    hSetEcho stdin False
    forever $ do
        c <- getChar
        putChar c

However, we would like to intercept key strokes for nefarious purposes, so we will slightly modify this program to install a handler at the beginning of the program that we will invoke on every incoming character:

install :: IO (Char -> IO ())
install = ???

main = do
    hSetEcho stdin False
    handleChar <- install
    forever $ do
        c <- getChar
        handleChar c
        putChar c

Notice that the type of install is exactly the correct type to be a Monoid:

  • () is a Monoid
  • Therefore, IO () is also a Monoid
  • Therefore Char -> IO () is also a Monoid
  • Therefore IO (Char -> IO ()) is also a Monoid

Therefore, we can combine key logging plugins together using Monoid operations. Here is one such example:

type Plugin = IO (Char -> IO ())

logTo :: FilePath -> Plugin
logTo filePath = do
    handle <- openFile filePath WriteMode
    hSetBuffering handle NoBuffering
    return (hPutChar handle)

main = do
    hSetEcho stdin False
    handleChar <- logTo "file1.txt" <> logTo "file2.txt"
    forever $ do
        c <- getChar
        handleChar c
        putChar c

Now, every key stroke will be recorded to both file1.txt and file2.txt. Let's confirm that this works as expected:

$ ./logger
Test<Enter>
ABC<Enter>
42<Enter>
<Ctrl-C>
$ cat file1.txt
Test
ABC
42
$ cat file2.txt
Test
ABC
42

Try writing your own Plugins and mixing them in with (<>) to see what happens. "Appendix C" contains the complete code for this section so you can experiment with your own Plugins.

Applicatives

Notice that I never actually proved the Monoid laws for the following two Monoid instances:

instance Monoid b => Monoid (a -> b) where
    mempty = \_ -> mempty
    mappend f g = \a -> mappend (f a) (g a)

instance Monoid a => Monoid (IO a) where
    mempty = return mempty

    mappend io1 io2 = do
        a1 <- io1
        a2 <- io2
        return (mappend a1 a2)

The reason why is that they are both special cases of a more general pattern. We can detect the pattern if we rewrite both of them to use the pure and liftA2 functions from Control.Applicative:

import Control.Applicative (pure, liftA2)

instance Monoid b => Monoid (a -> b) where
    mempty = pure mempty

    mappend = liftA2 mappend

instance Monoid b => Monoid (IO b) where
    mempty = pure mempty

    mappend = liftA2 mappend

This works because both IO and functions implement the following Applicative interface:

class Functor f => Applicative f where
    pure  :: a -> f a
    (<*>) :: f (a -> b) -> f a -> f b

-- Lift a binary function over the functor `f`
liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftA2 f x y = (pure f <*> x) <*> y

... and all Applicative instances must obey several Applicative laws:

pure id <*> v = v

((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)

pure f <*> pure x = pure (f x)

u <*> pure x = pure (\f -> f y) <*> u

These laws may seem a bit adhoc, but this paper explains that you can reorganize the Applicative class to this equivalent type class:

class Functor f => Monoidal f where
    unit  :: f ()
    (#) :: f a -> f b -> f (a, b)

Then the corresponding laws become much more symmetric:

fmap snd (unit # x) = x                 -- Left identity

fmap fst (x # unit) = x                 -- Right identity

fmap assoc ((x # y) # z) = x # (y # z)  -- Associativity
  where
    assoc ((a, b), c) = (a, (b, c))

fmap (f *** g) (x # y) = fmap f x # fmap g y  -- Naturality
  where
    (f *** g) (a, b) = (f a, g b)

I personally prefer the Monoidal formulation, but you go to war with the army you have, so we will use the Applicative type class for this post.

All Applicatives possess a very powerful property: they can all automatically lift Monoid operations using the following instance:

instance (Applicative f, Monoid b) => Monoid (f b) where
    mempty = pure mempty

    mappend = liftA2 mappend

This says: "If f is an Applicative and b is a Monoid, then f b is also a Monoid." In other words, we can automatically extend any existing Monoid with some new feature f and get back a new Monoid.

Note: The above instance is bad Haskell because it overlaps with other type class instances. In practice we have to duplicate the above code once for each Applicative. Also, for some Applicatives we may want a different Monoid instance.

We can prove that the above instance obeys the Monoid laws without knowing anything about f and b, other than the fact that f obeys the Applicative laws and b obeys the Applicative laws. These proofs are a little long, so I've included them in Appendix B.

Both IO and functions implement the Applicative type class:

instance Applicative IO where
    pure = return

    iof <*> iox = do
        f <- iof
        x <- iox
        return (f x)

instance Applicative ((->) a) where
    pure x = \_ -> x

    kf <*> kx = \a ->
        let f = kf a
            x = kx a
        in  f x

This means that we can kill two birds with one stone. Every time we prove the Applicative laws for some functor F:

instance Applicative F where ...

... we automatically prove that the following Monoid instance is correct for free:

instance Monoid b => Monoid (F b) where
    mempty = pure mempty

    mappend = liftA2 mappend

In the interest of brevity, I will skip the proofs of the Applicative laws, but I may cover them in a subsequent post.

The beauty of Applicative Functors is that every new Applicative instance we discover adds a new building block to our Monoid toolbox, and Haskell programmers have already discovered lots of Applicative Functors.

Revisiting tuples

One of the very first Monoid instances we wrote was:

instance (Monoid a, Monoid b) => Monoid (a, b) where
    mempty = (mempty, mempty)

    mappend (x1, y1) (x2, y2) = (mappend x1 x2, mappend y1 y2)

Check this out:

instance (Monoid a, Monoid b) => Monoid (a, b) where
    mempty = pure mempty

    mappend = liftA2 mappend

This Monoid instance is yet another special case of the Applicative pattern we just covered!

This works because of the following Applicative instance in Control.Applicative:

instance Monoid a => Applicative ((,) a) where
    pure b = (mempty, b)

    (a1, f) <*> (a2, x) = (mappend a1 a2, f x)

This instance obeys the Applicative laws (proof omitted), so our Monoid instance for tuples is automatically correct, too.

Composing applicatives

In the very first section I wrote:

Haskell programmers prove large-scale properties exactly the same way we build large-scale programs:

  • We build small proofs that we can verify correct in isolation
  • We compose smaller proofs into larger proofs

I don't like to use the word compose lightly. In the context of category theory, compose has a very rigorous meaning, indicating composition of morphisms in some category. This final section will show that we can actually compose Monoid proofs in a very rigorous sense of the word.

We can define a category of Monoid proofs:

So in our Plugin example, we began on the proof that () was a Monoid and then composed three Applicative morphisms to prove that Plugin was a Monoid. I will use the following diagram to illustrate this:

+-----------------------+
|                       |
| Legend:  * = Object   |
|                       |
|          v            |
|          | = Morphism |
|          v            |
|                       |
+-----------------------+

* `()` is a `Monoid`

v
| IO
v

* `IO ()` is a `Monoid`

v
| ((->) String)
v

* `String -> IO ()` is a `Monoid`

v
| IO
v

* `IO (String -> IO ())` (i.e. `Plugin`) is a `Monoid`

Therefore, we were literally composing proofs together.

Conclusion

You can equationally reason at scale by decomposing larger proofs into smaller reusable proofs, the same way we decompose programs into smaller and more reusable components. There is no limit to how many proofs you can compose together, and therefore there is no limit to how complex of a program you can tame using equational reasoning.

This post only gave one example of composing proofs within Haskell. The more you learn the language, the more examples of composable proofs you will encounter. Another common example is automatically deriving Monad proofs by composing monad transformers.

As you learn Haskell, you will discover that the hard part is not proving things. Rather, the challenge is learning how to decompose proofs into smaller proofs and you can cultivate this skill by studying category theory and abstract algebra. These mathematical disciplines teach you how to extract common and reusable proofs and patterns from what appears to be disposable and idiosyncratic code.

Appendix A - Missing Monoid instances

These Monoid instance from this post do not actually appear in the Haskell standard library:

instance Monoid b => Monoid (IO b)

instance Monoid Int

The first instance was recently proposed here on the Glasgow Haskell Users mailing list. However, in the short term you can work around it by writing your own Monoid instances by hand just by inserting a sufficient number of pures and liftA2s.

For example, suppose we wanted to provide a Monoid instance for Plugin. We would just newtype Plugin and write:

newtype Plugin = Plugin { install :: IO (String -> IO ()) }

instance Monoid Plugin where
    mempty = Plugin (pure (pure (pure mempty)))

    mappend (Plugin p1) (Plugin p2) =
        Plugin (liftA2 (liftA2 (liftA2 mappend)) p1 p2)

This is what the compiler would have derived by hand.

Alternatively, you could define an orphan Monoid instance for IO, but this is generally frowned upon.

There is no default Monoid instance for Int because there are actually two possible instances to choose from:

-- Alternative #1
instance Monoid Int where
    mempty = 0

    mappend = (+)

-- Alternative #2
instance Monoid Int where
    mempty = 1

    mappend = (*)

So instead, Data.Monoid sidesteps the issue by providing two newtypes to distinguish which instance we prefer:

newtype Sum a = Sum { getSum :: a }

instance Num a => Monoid (Sum a)

newtype Product a = Product { getProduct :: a}

instance Num a => Monoid (Product a)

An even better solution is to use a semiring, which allows two Monoid instances to coexist for the same type. You can think of Haskell's Num class as an approximation of the semiring class:

class Num a where
    fromInteger :: Integer -> a

    (+) :: a -> a -> a

    (*) :: a -> a -> a

    -- ... and other operations unrelated to semirings

Note that we can also lift the Num class over the Applicative class, exactly the same way we lifted the Monoid class. Here's the code:

instance (Applicative f, Num a) => Num (f a) where
    fromInteger n = pure (fromInteger n)

    (+) = liftA2 (+)

    (*) = liftA2 (*)

    (-) = liftA2 (-)

    negate = fmap negate

    abs = fmap abs

    signum = fmap signum

This lifting guarantees that if a obeys the semiring laws then so will f a. Of course, you will have to specialize the above instance to every concrete Applicative because otherwise you will get overlapping instances.

Appendix B

These are the proofs to establish that the following Monoid instance obeys the Monoid laws:

instance (Applicative f, Monoid b) => Monoid (f b) where
    mempty = pure mempty

    mappend = liftA2 mappend

... meaning that if f obeys the Applicative laws and b obeys the Monoid laws, then f b also obeys the Monoid laws.

Proof of the left identity law:

mempty <> x

-- x <> y = mappend x y
= mappend mempty x

-- mappend = liftA2 mappend
= liftA2 mappend mempty x

-- mempty = pure mempty
= liftA2 mappend (pure mempty) x

-- liftA2 f x y = (pure f <*> x) <*> y
= (pure mappend <*> pure mempty) <*> x

-- Applicative law: pure f <*> pure x = pure (f x)
= pure (mappend mempty) <*> x

-- Eta conversion
= pure (\a -> mappend mempty a) <*> x

-- mappend mempty x = x
= pure (\a -> a) <*> x

-- id = \x -> x
= pure id <*> x

-- Applicative law: pure id <*> v = v
= x

Proof of the right identity law:

x <> mempty = x

-- x <> y = mappend x y
= mappend x mempty

-- mappend = liftA2 mappend
= liftA2 mappend x mempty

-- mempty = pure mempty
= liftA2 mappend x (pure mempty)

-- liftA2 f x y = (pure f <*> x) <*> y
= (pure mappend <*> x) <*> pure mempty

-- Applicative law: u <*> pure y = pure (\f -> f y) <*> u
= pure (\f -> f mempty) <*> (pure mappend <*> x)

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= ((pure (.) <*> pure (\f -> f mempty)) <*> pure mappend) <*> x

-- Applicative law: pure f <*> pure x = pure (f x)
= (pure ((.) (\f -> f mempty)) <*> pure mappend) <*> x

-- Applicative law : pure f <*> pure x = pure (f x)
= pure ((.) (\f -> f mempty) mappend) <*> x

-- `(.) f g` is just prefix notation for `f . g`
= pure ((\f -> f mempty) . mappend) <*> x

-- f . g = \x -> f (g x)
= pure (\x -> (\f -> f mempty) (mappend x)) <*> x

-- Apply the lambda
= pure (\x -> mappend x mempty) <*> x

-- Monoid law: mappend x mempty = x
= pure (\x -> x) <*> x

-- id = \x -> x
= pure id <*> x

-- Applicative law: pure id <*> v = v
= x

Proof of the associativity law:

(x <> y) <> z

-- x <> y = mappend x y
= mappend (mappend x y) z

-- mappend = liftA2 mappend
= liftA2 mappend (liftA2 mappend x y) z

-- liftA2 f x y = (pure f <*> x) <*> y
= (pure mappend <*> ((pure mappend <*> x) <*> y)) <*> z

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= (((pure (.) <*> pure mappend) <*> (pure mappend <*> x)) <*> y) <*> z

-- Applicative law: pure f <*> pure x = pure (f x)
= ((pure f <*> (pure mappend <*> x)) <*> y) <*> z
  where
    f = (.) mappend

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= ((((pure (.) <*> pure f) <*> pure mappend) <*> x) <*> y) <*> z
  where
    f = (.) mappend

-- Applicative law: pure f <*> pure x = pure (f x)
= (((pure f <*> pure mappend) <*> x) <*> y) <*> z
  where
    f = (.) ((.) mappend)

-- Applicative law: pure f <*> pure x = pure (f x)
= ((pure f <*> x) <*> y) <*> z
  where
    f = (.) ((.) mappend) mappend

-- (.) f g = f . g
= ((pure f <*> x) <*> y) <*> z
  where
    f = ((.) mappend) . mappend

-- Eta conversion
= ((pure f <*> x) <*> y) <*> z
  where
    f x = (((.) mappend) . mappend) x

-- (f . g) x = f (g x)
= ((pure f <*> x) <*> y) <*> z
  where
    f x = (.) mappend (mappend x)

-- (.) f g = f . g
= ((pure f <*> x) <*> y) <*> z
  where
    f x = mappend . (mappend x)

-- Eta conversion
= ((pure f <*> x) <*> y) <*> z
  where
    f x y = (mappend . (mappend x)) y

-- (f . g) x = f (g x)
= ((pure f <*> x) <*> y) <*> z
  where
    f x y = mappend (mappend x y)

-- Eta conversion
= ((pure f <*> x) <*> y) <*> z
  where
    f x y z = mappend (mappend x y) z

-- Monoid law: mappend (mappend x y) z = mappend x (mappend y z)
= ((pure f <*> x) <*> y) <*> z
  where
    f x y z = mappend x (mappend y z)

-- (f . g) x = f (g x)
= ((pure f <*> x) <*> y) <*> z
  where
    f x y z = (mappend x . mappend y) z

-- Eta conversion
= ((pure f <*> x) <*> y) <*> z
  where
    f x y = mappend x . mappend y

-- (.) f g = f . g
= ((pure f <*> x) <*> y) <*> z
  where
    f x y = (.) (mappend x) (mappend y)

-- (f . g) x = f
= ((pure f <*> x) <*> y) <*> z
  where
    f x y = (((.) . mappend) x) (mappend y)

-- (f . g) x = f (g x)
= ((pure f <*> x) <*> y) <*> z
  where
    f x y = ((((.) . mappend) x) . mappend) y

-- Eta conversion
= ((pure f <*> x) <*> y) <*> z
  where
    f x = (((.) . mappend) x) . mappend

-- (.) f g = f . g
= ((pure f <*> x) <*> y) <*> z
  where
    f x = (.) (((.) . mappend) x) mappend

-- Lambda abstraction
= ((pure f <*> x) <*> y) <*> z
  where
    f x = (\k -> k mappend) ((.) (((.) . mappend) x))

-- (f . g) x = f (g x)
= ((pure f <*> x) <*> y) <*> z
  where
    f x = (\k -> k mappend) (((.) . ((.) . mappend)) x)

-- Eta conversion
= ((pure f <*> x) <*> y) <*> z
  where
    f = (\k -> k mappend) . ((.) . ((.) . mappend))

-- (.) f g = f . g
= ((pure f <*> x) <*> y) <*> z
  where
    f = (.) (\k -> k mappend) ((.) . ((.) . mappend))

-- Applicative law: pure f <*> pure x = pure (f x)
= (((pure g <*> pure f) <*> x) <*> y) <*> z
  where
    g = (.) (\k -> k mappend)
    f = (.) . ((.) . mappend)

-- Applicative law: pure f <*> pure x = pure (f x)
= ((((pure (.) <*> pure (\k -> k mappend)) <*> pure f) <*> x) <*> y) <*> z
  where
    f = (.) . ((.) . mappend)

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= ((pure (\k -> k mappend) <*> (pure f <*> x)) <*> y) <*> z
  where
    f = (.) . ((.) . mappend)

-- u <*> pure y = pure (\k -> k y) <*> u
= (((pure f <*> x) <*> pure mappend) <*> y) <*> z
  where
    f = (.) . ((.) . mappend)


-- (.) f g = f . g
= (((pure f <*> x) <*> pure mappend) <*> y) <*> z
  where
    f = (.) (.) ((.) . mappend)

-- Applicative law: pure f <*> pure x = pure (f x)
= ((((pure g <*> pure f) <*> x) <*> pure mappend) <*> y) <*> z
  where
    g = (.) (.)
    f = (.) . mappend

-- Applicative law: pure f <*> pure x = pure (f x)
= (((((pure (.) <*> pure (.)) <*> pure f) <*> x) <*> pure mappend) <*> y) <*> z
  where
    f = (.) . mappend

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= (((pure (.) <*> (pure f <*> x)) <*> pure mappend) <*> y) <*> z
  where
    f = (.) . mappend

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= ((pure f <*> x) <*> (pure mappend <*> y)) <*> z
  where
    f = (.) . mappend

-- (.) f g = f . g
= ((pure f <*> x) <*> (pure mappend <*> y)) <*> z
  where
    f = (.) (.) mappend

-- Applicative law: pure f <*> pure x = pure (f x)
= (((pure f <*> pure mappend) <*> x) <*> (pure mappend <*> y)) <*> z
  where
    f = (.) (.)

-- Applicative law: pure f <*> pure x = pure (f x)
= ((((pure (.) <*> pure (.)) <*> pure mappend) <*> x) <*> (pure mappend <*> y)) <*> z

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= ((pure (.) <*> (pure mappend <*> x)) <*> (pure mappend <*> y)) <*> z

-- Applicative law: ((pure (.) <*> u) <*> v) <*> w = u <*> (v <*> w)
= (pure mappend <*> x) <*> ((pure mappend <*> y) <*> z)

-- liftA2 f x y = (pure f <*> x) <*> y
= liftA2 mappend x (liftA2 mappend y z)

-- mappend = liftA2 mappend
= mappend x (mappend y z)

-- x <> y = mappend x y
= x <> (y <> z)

Appendix C: Monoid key logging

Here is the complete program for a key logger with a Monoid-based plugin system:

import Control.Applicative (pure, liftA2)
import Control.Monad (forever)
import Data.Monoid
import System.IO

instance Monoid b => Monoid (IO b) where
    mempty = pure mempty

    mappend = liftA2 mappend

type Plugin = IO (Char -> IO ())

logTo :: FilePath -> Plugin
logTo filePath = do
    handle <- openFile filePath WriteMode
    hSetBuffering handle NoBuffering
    return (hPutChar handle)

main = do
    hSetEcho stdin False
    handleChar <- logTo "file1.txt" <> logTo "file2.txt"
    forever $ do
        c <- getChar
        handleChar c
        putChar c

Saturday, June 14, 2014

Spreadsheet-like programming in Haskell

What if I told you that a spreadsheet could be a library instead of an application? What would that even mean? How do we distill the logic behind spreadsheets into a reusable abstraction? My mvc-updates library answers this question by bringing spreadsheet-like programming to Haskell using an intuitive Applicative interface.

The central abstraction is an Applicative Updatable value, which is just a Fold sitting in front of a Managed Controller:

data Updatable a =
    forall e . On (Fold e a) (Managed (Controller e))

The Managed Controller originates from my mvc library and represents a resource-managed, concurrent source of values of type e. Using Monoid operations, you can interleave these concurrent resources together while simultaneously merging their resource management logic.

The Fold type originates from my foldl library and represents a reified left fold. Using Applicative operations, you can combine multiple folds together in such a way that they still pass over the data set just once without leaking space.

To build an Updatable value, just pair up a Fold with a Managed Controller:

import Control.Foldl (last, length)
import MVC
import MVC.Updates
import MVC.Prelude (stdinLines, tick)
import Prelude hiding (last, length)

-- Store the last line from standard input
lastLine :: Updatable (Maybe String)
lastLine = On last stdinLines

-- Increment every second
seconds :: Updatable Int
seconds = On length (tick 1.0)

What's amazing is that when you stick a Fold in front of a Controller, you get a new Applicative. This Applicative instance lets you combine multiple Updatable values into new derived Updatable values. For example, we can combine lastLine and seconds into a single data type that tracks updates to both values:

import Control.Applicative ((<$>), (<*>))

data Example = Example (Maybe String) Int deriving (Show)

example :: Updatable Example
example = Example <$> lastLine <*> seconds

example will update every time lastLine or seconds updates, caching and reusing portions that do not update. For example, if lastLine updates then only the first field of Example will change. Similarly, if seconds updates then only the second field of Example will change.

When we're done combining Updatable values we can plug them into mvc using the updates function:

updates :: Buffer a -> Updatable a -> Managed (Controller a)

This gives us back a Managed Controller we can feed into our mvc application:

viewController :: Managed (View Example, Controller Example)
viewController = do
    controller <- updates Unbounded example
    return (asSink print, controller)

model :: Model () Example Example
model = asPipe $
    Pipes.takeWhile (\(Example str _) -> str /= Just "quit")

main :: IO ()
main = runMVC () model viewController

This program updates in response to two concurrent inputs: time and standard input.

$ ./example
Example Nothing 0
Test<Enter>
Example (Just "Test") 0  <-- Update: New input
Example (Just "Test") 1  <-- Update: 1 second passed
Example (Just "Test") 2  <-- Update: 1 second passed
ABC<Enter>
Example (Just "ABC") 2   <-- Update: New input
Example (Just "ABC") 3   <-- Update: 1 second 
quit<Enter>
$

Spreadsheets

The previous example was a bit contrived, so let's step it up a notch. What better way to demonstrate spreadsheet-like programming than .. a spreadsheet!

I'll use Haskell's gtk library to set up the initial API, which consists of a single exported function:

module Spreadsheet (spreadsheet) where

spreadsheet
    :: Managed                   -- GTK setup
        ( Updatable Double       -- Create input  cell
        , Managed (View Double)  -- Create output cell
        , IO ()                  -- Start spreadsheet
        )
spreadsheet = ???

You can find the full source code here.

Using spreadsheet, I can now easily build my own spread sheet application:

{-# LANGUAGE TemplateHaskell #-}

import Control.Applicative (Applicative, (<$>), (<*>))
import Lens.Family.TH (makeLenses)
import MVC
import MVC.Updates (updates)
import Spreadsheet (spreadsheet)

-- Spreadsheet input (4 cells)
data In  = I
    { _i1 :: Double
    , _i2 :: Double
    , _i3 :: Double
    , _i4 :: Double
    }

-- Spreadsheet output (4 cells)
data Out = O
    { _o1 :: Double
    , _o2 :: Double
    , _o3 :: Double
    , _o4 :: Double
    }
makeLenses ''Out

-- Spreadsheet logic that converts input to output
model :: Model () In Out
model = asPipe $ loop $ \(I i1 i2 i3 i4) -> do
    return $ O (i1 + i2) (i2 * i3) (i3 - i4) (max i4 i1)

main :: IO ()
main = runMVC () model $ do
    (inCell, outCell, go) <- spreadsheet

    -- Assemble the four input cells
    c <- updates Unbounded $
        I <$> inCell <*> inCell <*> inCell <*> inCell

    -- Assemble the four output cells
    v <- fmap (handles o1) outCell
      <> fmap (handles o2) outCell
      <> fmap (handles o3) outCell
      <> fmap (handles o4) outCell

    -- Run the spread sheet
    liftIO go

    return (v, c)

You can install this program yourself by building my mvc-updates-examples package on Github:

$ git clone https://github.com/Gabriel439/Haskell-MVC-Updates-Examples-Library.git
$ cd Haskell-MVC-Updates-Examples-Library
$ cabal install
$ ~/.cabal/bin/mvc-spreadsheet-example

Or you can watch this video of the spreadsheet in action:

The key feature I want to emphasize is how concise this spreadsheet API is. We provide our user an Applicative input cell builder and a Monoid output cell builder, and we're done. We don't have to explain to the user how to acquire resources, manage threads, or combine updates. The Applicative instance for Updatable handles all of those trivial details for them. Adding extra inputs or outputs is as simple as chaining additional inCell and outCell invocations.

Reactive animations

We don't have to limit ourselves to spread sheets, though. We can program Updatable graphical scenes using these same principles. For example, let's animate a cloud that orbits around the user's mouse using the sdl library. Just like before, we will begin from a concise interface:

-- Animation frames for the cloud
data Frame = Frame0 | Frame1 | Frame2 | Frame3

-- To draw a cloud we specify the frame and the coordinates
data Cloud = Cloud Frame Int Int

-- mouse coordinates
data Mouse = Mouse Int Int

sdl :: Managed         -- SDL setup
    ( View Cloud       -- Draw a cloud
    , Updatable Mouse  -- Updatable mouse coordinates
    )

The full source is located here.

In this case, I want to combine the Updatable mouse coordinates with an Updatable time value:

main :: IO ()
main = runMVC () (asPipe cat) $ do
    (cloudOut, mouse) <- sdl
    let seconds = On length (tick (1 / 60))

        toFrame n = case (n `div` 15) `rem` 4 of
            0 -> Frame0
            1 -> Frame1
            2 -> Frame2
            _ -> Frame3

        cloudOrbit t (Mouse x y) = Cloud (toFrame t) x' y'
          where
            x' = x + truncate (100 * cos (fromIntegral t / 10))
            y' = y + truncate (100 * sin (fromIntegral t / 10))

    cloudIn <- updates Unbounded (cloudOrbit <$> seconds <*> mouse)
    return (cloudOut, cloudIn)

cloudOrbit is defined as a pure function from the current time and mouse coordinates to a Cloud. With the power of Applicatives we can lift this pure function over two Updatable values (mouse and seconds) to create a new Updatable Cloud that we pass intact to our program's View.

Like before, you can either run this program yourself:

$ git clone https://github.com/Gabriel439/Haskell-MVC-Updates-Examples-Library.git
$ cd Haskell-MVC-Updates-Examples-Library
$ cabal install
$ ~/.cabal/bin/mvc-spreadsheet-example

... or you can watch the video:

Under the hood

mvc-updates distinguishes itself from similar libraries in other languages by not relying on a semantics for concurrency. The Applicative instance for Updatable uses no concurrent operations, whatsoever:

instance Applicative Updatable where
    pure a = On (pure a) mempty

    (On foldL mControllerL) <*> (On foldR mControllerR)
        = On foldT mControllerT
      where
        foldT = onLeft foldL <*> onRight foldR

        mControllerT = fmap (fmap Left ) mControllerL
                    <> fmap (fmap Right) mControllerR

        onLeft (Fold step  begin done) =
                Fold step' begin done
          where
            step' x (Left a) = step x a
            step' x  _       = x

        onRight (Fold step  begin done) =
                 Fold step' begin done
          where
            step' x (Right a) = step x a
            step' x  _        = x

In fact, this Applicative instance only assumes that the Controller type is a Monoid, so this trick generalizes to any source that forms a Monoid.

This not only simplifies the proof of the Applicative laws, but it also greatly improves efficiency. This Applicative instance introduces no new threads or buffers. The only thread or buffer you will incur is in the final call to the updates function, but expert users can eliminate even that overhead by inlining the logic of the updates function directly into their mvc program.

Lightweight

The mvc-updates library is incredibly small. Here's the entire API:

data Updatable = forall e . On (Fold e a) (Controller e)

instance Functor     Updatable
instance Applicative Updatable

updates :: Buffer a -> Updatable a -> Managed (Controller a)

The library is very straightforward to use:

  • Build Updatable values
  • Combine them using their Applicative instance
  • Convert them back to a Managed Controller when you're done

That's it!

The small size of the library is no accident. The Updatable abstraction is an example of a scalable program architecture. When we combine Updatable values together, the end result is a new Updatable value. This keeps the API small since we always end up back where we started and we never need to introduce additional abstractions.

There is no need to distinguish between "primitive" Updatable values or "derived" Updatable values or "sheets" of Updatable values. The Applicative interface lets us unify these three concepts into a single uniform concept. Moreover, the Applicative interface is one of Haskell's widely used type classes inspired by category theory, so we can reuse people's pre-existing intuition for how Applicatives work. This is a common theme in Haskell where once you learn the core set of mathematical type classes they go a very, very long way.

Conclusion

Hopefully this post will get you excited about the power of Applicative programming. If you would like to learn more about Applicatives, I highly recommend the "Applicative Programming with Effects" paper by Conor McBride and Ross Paterson.

I would like to conclude by saying that there many classes of problems that the mvc-updates library does not solve well, such as:

  • build systems,
  • programs with computationally expensive Views, and:
  • Updatable values that share state.

However, mvc-updates excels at:

  • data visualizations,
  • control panels, and:
  • spread sheets (of course).

You can find the mvc-updates library up on Hackage or on Github.

Friday, April 25, 2014

Model-view-controller, Haskell-style

I'm releasing the mvc library for model-view-controller (MVC) programming in Haskell. I initially designed this library with games and user interfaces in mind, but the larger goal of this library is to provide a mathematically inspired framework for general-purpose component sharing in Haskell.

This library differs in a significant way from other MVC libraries: this API statically enforces in the types that the Model is pure, but with very little loss in power. Using mvc you can refactor many types of concurrent applications into a substantial and pure Model that interfaces with carefully constrained Views and Controllers.

When you purify your Model this way, you can:

  • record and replay bugs reproducibly,

  • do property-based testing (ala QuickCheck) to uncover corner cases, and:

  • prove formal properties about your Model using equational reasoning.

The first half of this post walks through two examples reproduced from the mvc documentation and the second half of this post describes the architecture that enables you to embed large and non-trivial business logic in an entirely pure Model. This post will use a side-by-side mix of theoretical terminology alongside plain English. Even if you don't understand the theoretical half of this post you should still derive benefit from the non-technical half and use that as a bridge towards understanding the underlying theory.

Examples

The mvc library uses four types to represent everything:

  • The Model is a pure streaming transformation from inputs to outputs

  • The View handles all outputs from the Model

  • The Controller supplies all inputs to the Model

  • The Managed type extends other types with logic for acquiring or releasing resources

There are no other concepts you have to learn. The API is extraordinarily small (4 types, and 8 primitive functions associated with those types).

However, as we extend our application the types will never grow more complex. In fact, the mvc library statically forbids you from increasing the complexity of your types, because the library only provides a single run function of the following type:

runMVC
    :: s                               -- Initial state
    -> Model s a b                     -- Program logic
    -> Managed (View b, Controller a)  -- Impure output and input
    -> IO s                            -- Returns final state

There is no other way to consume Models, Views, and Controllers, so runMVC forces you to consolidate all your Views into a single View and consolidate all your Controllers into a single Controller. This creates a single entry point and a single exit point for your Model. Equally important, you cannot mix your Model logic with your View or Controller logic. The mvc library enforces MVC best practices using the type system.

This first minimal example illustrates these basic concepts:

import MVC
import qualified MVC.Prelude as MVC
import qualified Pipes.Prelude as Pipes

external :: Managed (View String, Controller String)
external = do
    c1 <- MVC.stdinLines
    c2 <- MVC.tick 1
    return (MVC.stdoutLines, c1 <> fmap show c2)

model :: Model () String String
model = asPipe (Pipes.takeWhile (/= "quit"))

main :: IO ()
main = runMVC () model external

The key components are:

  • A Controller that interleaves lines from standard input with periodic ticks

  • A View that writes lines to standard output

  • A pure Model, which forwards lines until it detects the string "quit"

  • A Managed type, which abstracts over resource acquisition and release

The Model only has a single streaming entry point (the Controller) and a single streaming exit point (the View).

However, this interface is deceptively simple and can model very complex logic. For example, here's a more elaborate example using the sdl library that displays a white rectangle between every two mouse clicks:

import Control.Monad (join)
import Graphics.UI.SDL as SDL
import Lens.Family.Stock (_Left, _Right)  -- `lens-family-core`
import MVC
import MVC.Prelude
import qualified Pipes.Prelude as Pipes

data Done = Done deriving (Eq, Show)

sdl :: Managed (View (Either Rect Done), Controller Event)
sdl = join $ managed $ \k ->
  withInit [InitVideo, InitEventthread] $ do
    surface <- setVideoMode 640 480 32 [SWSurface]
    white   <- mapRGB (surfaceGetPixelFormat surface) 255 255 255

    let done :: View Done
        done = asSink (\Done -> SDL.quit)

        drawRect :: View Rect
        drawRect = asSink $ \rect -> do
            _ <- fillRect surface (Just rect) white
            SDL.flip surface

        totalOut :: View (Either Rect Done)
        totalOut = handles _Left drawRect <> handles _Right done

    k $ do
        totalIn <- producer Single (lift waitEvent >~ cat)
        return (totalOut, totalIn)

pipe :: Monad m => Pipe Event (Either Rect Done) m ()
pipe = do
    Pipes.takeWhile (/= Quit)
        >-> (click >~ rectangle >~ Pipes.map Left)
    yield (Right Done)

rectangle :: Monad m => Consumer' (Int, Int) m Rect
rectangle = do
    (x1, y1) <- await
    (x2, y2) <- await
    let x = min x1 x2
        y = min y1 y2
        w = abs (x1 - x2)
        h = abs (y1 - y2)
    return (Rect x y w h)

click :: Monad m => Consumer' Event m (Int, Int)
click = do
    e <- await
    case e of
        MouseButtonDown x y ButtonLeft ->
            return (fromIntegral x, fromIntegral y)
        _ -> click

main :: IO ()
main = runMVC () (asPipe pipe) sdl

Compile and run this program, which will open up a window, and begin clicking to paint white rectangles to the screen:

Here we package the effectful and concurrent components that we need from the sdl into a self-contained package containing a single View and Controller. Our pure logic is contained entirely within a pure Pipe, meaning that we can feed synthetic input to our program:

>>> let leftClick (x, y) = MouseButtonDown x y ButtonLeft
>>> Pipes.toList $
...     each [leftClick (10, 10), leftClick (15, 16), Quit]
...         >-> pipe
[Left (Rect {rectX = 10, rectY = 10, rectW = 5, rectH = 6}),Right
 Done]

... or even QuickCheck our program logic! We can verify that our program generates exactly one rectangle for every two clicks:

>>> import Test.QuickCheck
>>> quickCheck $ \xs ->
...     length (Pipes.toList (each (map leftClick xs) >-> pipe))
...     == length xs `div` 2
+++ OK, passed 100 tests.

These kinds of tests would be impossible to run if we settled for anything less than complete separation of impurity and concurrency from our program's logic.

However, this total separation might seem unrealistic. What happens if we don't have exactly one View or exactly one Controller?

Monoids - Part 1

Views and Controllers are Monoids, meaning that we can combine any number of Views into a single View, and likewise combine any number of Controllers into a single Controller, by using mconcat (short for "Monoid concatenation") from Data.Monoid:

-- Combine a list of `Monoid`s into a single `Monoid`
mconcat :: Monoid m => [m] -> m

When we specialize the type of mconcat to View or Controller we get the following two specialized functions:

-- Combining `View`s sequences their effects
mconcat :: [View a] -> View a

-- Combining `Controller`s interleaves their events
mconcat :: [Controller a] -> Controller a

In other words, we can can combine a list of any number of Views into a single View and combine a list of any number of Controllers into a single Controller. We get several benefits for free as a result of this design.

First, combinability centralizes our View logic and Controller logic into a single expression that we feed to runMVC. We can therefore identify all inputs and outputs to our system simply by tracing all sub-expressions that feed into this larger expression. Contrast this with a typical mature code base where locating all relevant inputs and outputs for the system is non-trivial because they are typically not packaged into a single self-contained term.

Second, combinability promotes reuse. If we find ourselves repeatedly using the same set of inputs or outputs we can bundle them into a new derived component that we can share with others.

Third, combinable inputs and outputs are the reason our Model can afford to have a single entry point and a single exit point. This beats having to write callback spaghetti code where we cannot easily reason about our application's control flow.

This is an example of a scalable architecture. The Monoid type class lets us indefinitely grow our inputs and outputs without ever increasing the number of concepts, abstractions or types.

To be more specific, this scalable architecture is a special case of the category design pattern. When combinable components are morphisms in a category, we can connect as many components as we please yet still end up back where we started. In this case the operative category is a monoid, where Views or Controllers are morphisms, (<>) is the composition operator and mempty is the identity morphism.

Functors - Part 1

However, the Monoid type class only lets us combine Views and Controllers that have the same type. For example, suppose we have a Controller for key presses, and a separate Controller for mouse events:

keys   :: Controller KeyEvent

clicks :: Controller MouseEvent

If we try to combine these using (<>) (an infix operator for mappend), we will get a type error because their types do not match:

keys <> clicks  -- TYPE ERROR!

keys and clicks don't stream the same event type, so how do we reconcile their different types? We use functors!

fmap Left keys
    :: Controller (Either KeyEvent MouseEvent)

fmap Right clicks
    :: Controller (Either KeyEvent MouseEvent)

fmap Left keys <> fmap Right clicks
    :: Controller (Either KeyEvent MouseEvent)

The functor design pattern specifies that when we have an impedance mismatch between components, we unify them to agree on a common component framework. Here, we unify both of our Controller output types using Either.

Using theoretical terminology, when we have morphisms in diverse categories, we use functors to transform these morphisms to agree on a common category. In this case keys is a morphism in the Controller KeyEvent monoid and clicks is a morphism in the Controller MouseEvent monoid. We use fmap to transform both monoids to agree on the Controller (Either KeyEvent MouseEvent) monoid.

However, in this case fmap is behaving as a functor in a different sense than we are normally accustomed to. We're already familiar with the following functor laws for fmap:

fmap (f . g) = fmap f . fmap g

fmap id = id

However, right now we're not interested in transformations from functions to functions. Instead, we're interested in transformations from monoids to monoids, so we're going to invoke a different set of functor laws for our Controllers:

fmap f (c1 <> c2) = fmap f c1 <> fmap f c2

fmap f mempty = mempty

In other words, fmap f correctly translates monoid operations from one type of Controller to another. This functor between monoids is the operative functor when we transform Controllers to agree on a common type.

Functors - Part 2

We can use the same functor design pattern to unify different types of Views as well. For example, let's assume that we have two separate Views, one that logs Strings to a file, and another that displays video Frames to a screen:

logLines :: View String

frames :: View Frame

Again, we cannot naively combine these using mappend/(<>) because the types don't match:

logLines <> frames  -- TYPE ERROR!

However, View does not implement Functor, so how do we unify the types this time?

We still use functors! However, this time we will be using the handles function from mvc, which has the following type:

handles :: Traversal' a b -> View b -> View a

This lets us use Traversals to specify which outgoing values each View should handle:

import Lens.Family.Stock (_Left, _Right)

-- _Left  :: Traversal' (Either a b) a
-- _Right :: Traversal' (Either a b) b

handles _Left logLines
    :: View (Either String Frames)

handles _Right frames
    :: View (Either String Frames)

handles _Left logLines <> handles _Right frames
    :: view (Either String Frames)

This reads a little like English: logLines handles _Left values, and frames handles _Right values.

Like the previous example, handles is a functor in two ways. The first functor maps traversal composition to function composition:

handles (t1 . t2) = handles t1 . handles t2

handles id = id

The second functor maps monoid operations from one View to another:

handles t (v1 <> v2) = handles t v1 <> handles t v2

handles t mempty = mempty

This latter functor between View monoids is the operative functor when we are unifying Views to agree on a common type.

Applicatives

Alright, but we don't typically work with unadorned Views or Controllers. If you look at the utility section of mvc you will see that most Views or Controllers are Managed, meaning that they must acquire or release some sort of resource before they can begin streaming values in or out. For example, any View or Controller that interacts with a file must initially acquire the file and release the file when done:

fromFile :: FilePath -> Managed (Controller String)

toFile :: FilePath -> Managed (View String)

Uh oh... We have a problem! runMVC doesn't accept separate Managed Views and Managed Controllers. runMVC only accepts a combined View and Controller that share the same Managed logic:

runMVC
    :: s
    -> Model s a b
    -> Managed (View b, Controller a) -- What do we do?
    -> IO s

runMVC is written this way because some Views and Controllers must acquire and release the same resource. Does this mean that I need to provide a new run function that accepts separate Managed Views and Managed Controllers?

No! Fortunately, Managed implements the Applicative type class and we can use Applicatives to combined two Managed resources into a single Managed resource:

import Control.Applicative (liftA2)

liftA2 (,)
    :: Applicative f => f a -> f b -> f (a, b)

-- Specialize `liftA2` to `Managed`
liftA2 (,)
    :: Managed a -> Managed b -> Managed (a, b)

toFile "output.txt"
    :: Managed (View String)

fromFile "input.txt"
    :: Managed (Controller String)

liftA2 (,) (toFile "output.txt") (fromFile "input.txt")
    :: Managed (View String, Controller String)

I can fuse my two Managed resources into a single Managed resource! This is another example of scalable design. We don't complicate our run function by adding special cases for every permutation of Managed Views and Controllers. Instead, we make Managed layers laterally combinable, which prevents proliferation of functions, types, and concepts.

Monoids - Part 2

Managed implements the Monoid type class, too! Specifically, we can wrap any type that implements Monoid with Managed and we will get back a new derived Monoid:

instance Monoid r => Monoid (Managed r) where
    mempty  = pure mempty
    mappend = liftA2 mappend

This means that if I have two Managed Views, I can combine them into a single Managed View using the same Monoid operations as before:

view1 :: Managed (View A)
view2 :: Managed (View A)

viewBoth :: Managed (View A)
viewBoth = view1 <> view2

The same is true for Controllers:

controller1 :: Managed (Controller A)
controller2 :: Managed (Controller A)

controllerBoth :: Managed (Controller A)
controllerBoth = controller1 <> controller2

In fact, this trick works for any Applicative, not just Managed. Applicatives let you extend arbitrary Monoids with new features while still preserving their Monoid interface. There is no limit to how many Applicative extensions you can layer this way.

Conclusion

The documentation for the mvc library is full of theoretical examples like these showing how to architect applications using scalable abstractions inspired by category theory.

The mvc library has certain limitations. Specifically, I did not design the library to handle changing numbers of inputs and outputs over time. This is not because of a deficiency in category theory. Rather, I wanted to introduce this simpler API as a stepping stone towards understanding more general abstractions later on that I will release as separate libraries.

The other reason I'm releasing the mvc library is to test the waters for an upcoming book I will write about architecting programs using category theory. I plan to write one section of the book around an application structured using this mvc style.

Links:

  • Hackage - the API and documentation (including tutorials)

  • Github - For development and issues

Saturday, April 19, 2014

How the continuation monad works

I remember the first time I read the Monad instance for ContT I was so confused. I couldn't fathom how it worked because it was hard to discern the pattern.

However, I later discovered that renaming things makes the pattern much more clear:

import Control.Applicative

newtype ContT x m r = ContT { (>>-) :: (r -> m x) -> m x }

instance Functor (ContT x m) where
    fmap f m  = ContT $ \_return ->  -- fmap f m =
        m >>- \a ->                  --     m >>= \a ->
        _return (f a)                --     return (f a)

instance Applicative (ContT x m) where
    pure r    = ContT $ \_return ->  -- pure r =
        _return r                    --     return r

    mf <*> mx = ContT $ \_return ->  -- mf <*> mx =
        mf >>- \f ->                 --     mf >>= \f ->
        mx >>- \x ->                 --     mx >>= \x ->
        _return (f x)                --     return (f x)

instance Monad (ContT x m) where
    return r  = ContT $ \_return ->  -- return r =
        _return r                    --     return r

    m >>= f   = ContT $ \_return ->  -- m >>= f =
        m   >>- \a ->                --     m   >>= \a ->
        f a >>- \b ->                --     f a >>= \b ->
        _return b                    --     return b

Friday, April 4, 2014

Scalable program architectures

Haskell design patterns differ from mainstream design patterns in one important way:

  • Conventional architecture: Combine a several components together of type A to generate a "network" or "topology" of type B

  • Haskell architecture: Combine several components together of type A to generate a new component of the same type A, indistinguishable in character from its substituent parts

This distinction affects how the two architectural styles evolve as code bases grow.

The conventional architecture requires layering abstraction on top of abstraction:

Oh no, these Bs are not connectable, so let's make a network of Bs and call that a C.

Well, I want to assemble several Cs, so let's make a network of Cs and call that a D

...

Wash, rinse, and repeat until you have an unmanageable tower of abstractions.

With a Haskell-style architecture, you don't need to keep layering on abstractions to preserve combinability. When you combine things together the result is still itself combinable. You don't distinguish between components and networks of components.

In fact, this principle should be familiar to anybody who knows basic arithmetic. When you combine a bunch of numbers together you get back a number:

3 + 4 + 9 = 16

Zero or more numbers go in and exactly one number comes out. The resulting number is itself combinable. You don't have to learn about "web"s of numbers or "web"s of "web"s of numbers.

If elementary school children can master this principle, then perhaps we can, too. How can we make programming more like addition?

Well, addition is simple because we have (+) and 0. (+) ensures that we can always convert more than one number into exactly number:

(+) :: Int -> Int -> Int

... and 0 ensures that we can always convert less than one number into exactly one number by providing a suitable default:

0 :: Int

This will look familiar to Haskell programmers: these type signatures resemble the methods of the Monoid type class:

class Monoid m where
    -- `mappend` is analogous to `(+)`
    mappend :: m -> m -> m

    -- `mempty` is analogous to `0`
    mempty  :: m

In other words, the Monoid type class is the canonical example of this Haskell architectural style. We use mappend and mempty to combine 0 or more ms into exactly 1 m. The resulting m is still combinable.

Not every Haskell abstraction implements Monoid, nor do they have to because category theory takes this basic Monoid idea and generalizes it to more powerful domains. Each generalization retains the same basic principle of preserving combinability.

For example, a Category is just a typed monoid, where not all combinations type-check:

class Category cat where
    -- `(.)` is analogous to `(+)`
    (.) :: cat b c -> cat a b -> cat a c

    -- `id` is analogous to `0`
    id  :: cat a a

... a Monad is like a monoid where we combine functors "vertically":

-- Slightly modified from the original type class
class Functor m => Monad m where
    -- `join` is analogous to `(+)`
    join :: m (m a) -> m a

    -- `return` is analogous to `0`
    return :: a -> m a

... and an Applicative is like a monoid where we combine functors "horizontally":

-- Greatly modified, but equivalent to, the original type class
class Functor f => Applicative f where
    -- `mult` is is analogous to `(+)`
    mult :: f a -> f b -> f (a, b)

    -- `unit` is analogous to `0`
    unit :: f ()

Category theory is full of generalized patterns like these, all of which try to preserve that basic intuition we had for addition. We convert more than one thing into exactly one thing using something that resembles addition and we convert less than one thing into exactly one thing using something that resembles zero. Once you learn to think in terms of these patterns, programming becomes as simple as basic arithmetic: combinable components go in and exactly one combinable component comes out.

These abstractions scale limitlessly because they always preserve combinability, therefore we never need to layer further abstractions on top. This is one reason why you should learn Haskell: you learn how to build flat architectures.

Tuesday, April 1, 2014

Worst practices are viral for the wrong reasons

This short post describes my hypothesis for why poor software engineering practices are more viral. Simply stated:

Worst practices spread more quickly because they require more attention

The following two sections outline specific manifestations of this problem and how they promote the dissemination of worst practices.

Management

Corollary 1: Teams with the greatest technical debt mentor the most employees.

Scenario 1: You manage a team that ships an important feature but with a poor execution. You can make a compelling case to management that your team needs more head count to continue supporting this feature. More employees reporting to you increases your chances of promotion and you enjoy rewarding opportunities to mentor new software engineers in your specific brand of programming.

Scenario 2: You manage a team that ships an important feature in the exact same amount of time but with an amazing execution. Your code requires little maintenance, so little in fact that your team is now obsolete. If you're lucky you are retasked to work on a new project; if you're unlucky you are fired because your skills are no longer relevant. Training others how to write software of excellent quality is out of the question either way.

In other words, software engineers that produce excellent code cannot easily pass on their wisdom to the next generation of programmers unless they go into academia.

Open source projects

Corollary 2: Poorly implemented libraries or programming languages generate more buzz.

Scenario 1: You write a useful library or programming language, but it is incredibly buggy and problematic. This generates several scathing blog posts criticizing your work, prompting others to clarify in response how to work around those issues. Don't forget to check Stack Overflow, which is full of people asking for help regarding how to use your project. Did you know that people measure popularity in terms of Stack Overflow questions?

Scenario 2: You release a useful library or programming language at the same time, except that through some miracle you get it correct on the first try. Version 1.0 is your first and last release. That means you can't advertise your library through announcement posts for subsequent releases and there are only so many ways that you can say "it works" before people accuse you of shameless advertising.

In other words, well-written open source projects can become victims of their own success, with fewer opportunities to market themselves.

Conclusion

Obviously the above examples are exaggerated hyperboles and reality is somewhere in the middle. There is no perfect software project or team and there is a limit to how much crap a company or user will tolerate.

However, I write this because I value simple and understandable software and I want to start a discussion on how software engineering can culturally reward correctness and reliability. We need to think of ways to encourage programming excellence to spread.