# News aggregator

### Functional Jobs: Big Data Engineer / Data Scientist at Recruit IT (Full-time)

- Are you a Big Data Engineer who wants to work on innovative cloud and real-time data analytic technologies?
- Do you have a passion for turning data into meaningful information?
- Does working on a world-class big data project excite you?

Our client is currently looking in growth phase and looking for passionate and creative Data Scientists who can design, development, and implement robust, and scalable big data solutions. This is a role where you will need to enjoy being on the cusp of emerging technologies, and have a genuine interest in breaking new ground.

**Your skills and experience will cover the majority of the following:**

- Experience working across real-time data analytics, machine learning, and big data solutions
- Experience working with large data sets and cloud clusters
- Experience with various NoSQL technologies and Big Data platforms including; Hadoop, Cassandra, HBASE, Accumulo, and MapReduce
- Experience with various functional programming languages including; Scala, R, Clojure, Erlang, F#, Caml, Haskell, Common Lisp, or Scheme

This is an excellent opportunity for someone who is interested in a change in lifestyle, and where you would be joining other similar experienced professionals!

New Zealand awaits!

Get information on how to apply for this position.

### Gabriel Gonzalez: 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.

MonoidsHaskell's Prelude provides the following Monoid type class:

class Monoid m wheremempty :: 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 identityx <> mempty = x -- Right identity

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

For example, Ints form a Monoid:

-- See "Appendix A" for some caveatsinstance Monoid Int where

mempty = 0

mappend = (+)

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

0 + x = xx + 0 = x

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

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

>>> 4 <> 26

>>> 5 <> mempty <> 5

10

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

Extending MonoidsWell, 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) wheremempty = (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 = xWe 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 equationmempty <> 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 proofsI 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 = xx + 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) wheremempty = (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 equationmempty <> 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 listsinstance 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?

IOWe'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 caveatsinstance 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 stdingetLine :: 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 inputHello<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 stdinreadLn :: 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 MonoidHaskell 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.

FunctionsAlright, 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) wheremempty = \_ -> 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 pluginsNow 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 = dohSetEcho 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:

$ ./loggerTest<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.

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

instance Monoid b => Monoid (a -> b) wheremempty = \_ -> 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 wherepure :: 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 whereunit :: f ()

(#) :: f a -> f b -> f (a, b)

Then the corresponding laws become much more symmetric:

fmap snd (unit # x) = x -- Left identityfmap 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) wheremempty = 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 wherepure = 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) wheremempty = 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 tuplesOne of the very first Monoid instances we wrote was:

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

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

Check this out:

instance (Monoid a, Monoid b) => Monoid (a, b) wheremempty = 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) wherepure 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 applicativesIn 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:

- Objects are types and their associated Monoid proofs
- Morphisms are Applicative Functors
- The identity morphism is the Identity applicative
- The composition operation is composition of Applicative Functors
- The category laws are isomorphisms instead of equalities

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.

ConclusionYou 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 instancesThese 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 #1instance 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 wherefromInteger :: 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) wherefromInteger 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 BThese are the proofs to establish that the following Monoid instance obeys the Monoid laws:

instance (Applicative f, Monoid b) => Monoid (f b) wheremempty = 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

### Gabriel Gonzalez: 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 constructorsnewtype 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.Managedimport 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 reasoningMy 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.Applicativeimport 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 Pipesnewtype 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.Managedimport 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.txt1

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 breuse = 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 p2reuse 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.

ConclusionExperts 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.

### Field Accessors Considered Harmful

### mightybyte: Field Accessors Considered Harmful

data Config = Config { configFieldA :: [Text] }

So your Config data structure gives your users getters and setters for field A (and any other fields you might have). Your users are happy and life is good. Then one day you decide to add a new feature and that feature requires expanding and restructuring Config. Now you have this:

data MConfig = MConfig { mconfigFieldA :: [Text] }

data Config = Config { configMC :: MConfig , configFieldX :: Text , configFieldY :: Bool }

This is a nice solution because your users get to keep the functionality over the portion of the Config that they are used to, and they still get the new functionality. But now there's a problem. You're still breaking them because configFieldA changed names to mconfigFieldA and now refers to the MConfig structure instead of Config. If this was not a data structure, you could preserve backwards compatibility by creating another function:

configFieldA = mconfigFieldA . configMC

But alas, that won't work here because configFieldA is not a normal function. It is a special field accessor generated by GHC and you know that your users are using it as a setter. It seems to me that we are at an impasse. It is completely impossible to deliver your new feature without breaking backwards compatibility somehow. No amount of deprecated cycles can ease the transition. The sad thing is that it seems like it should have been totally doable. Obviously there are some kinds of changes that understandably will break backwards compatibility. But this doesn't seem like one of them since it is an additive change. Yes, yes, I know...it's impossible to do this change without changing the type of the Config constructor, so that means that at least that function will break. But we should be able to minimize the breakage to the field accessor functions, and field accessors prevent us from doing that.

However, we could have avoided this problem. If we had a bit more foresight, we could have done this.

module Foo (mkConfig, configFieldA) where

data Config = Config { _configFieldA :: [Text] }

mkConfig :: [Text] -> Config

mkConfig = Config

configFieldA = lens _configFieldA (\c a -> c { _configFieldA = a })

This would allow us to avoid breaking backwards compatibility by continuing to export appropriate versions of these symbols. It would look something like this.

module Foo ( MConfig , mkMConfig , mconfigFieldA , Config , mkConfig , configFieldA , configMC -- ... ) where data MConfig = MConfig { _mconfigFieldA :: [Text] } data Config = Config { _configMC :: MConfig , _configFieldX :: Text , _configFieldY :: Bool } mkMConfig = MConfig mkConfig a = Config (mkMConfig a) "" False mconfigFieldA = lens _mconfigFieldA (\c a -> c { _mconfigFieldA = a }) configMC = lens _configMC (\c mc -> c { _configMC = mc }) -- The rest of the field lenses here configFieldA = configMC . mconfigFieldA Note that the type signatures for mkConfig and configFieldA stay exactly the same. We weren't able to do this with field accessors because they are not composable. Lenses solve this problem for us because they are composable and we have complete control over their definition.

For quite some time now I have thought that I understood the advantage that lenses give you over field accessors. Discovering this added ability of lenses in helping us preserve backwards compatibility came as a pleasant surprise. I'll refrain from opining on how this should affect your development practices, but I think it makes the case for using lenses in your code a bit stronger than it was before.

### Brent Yorgey: Readers wanted!

**tl;dr**: Read a draft of my thesis and send me your feedback by September 9!

Over the past year I’ve had several people say things along the lines of, “let me know if you want me to read through your thesis”. I never took them all that seriously (it’s easy to *say* you are willing to read a 200-page document…), but it never hurts to ask, right?

My thesis defense is scheduled for October 14, and I’m currently undertaking a massive writing/editing push to try to get as much of it wrapped up as I can before classes start on September 4. So, if there’s anyone out there actually interested in reading a draft and giving feedback, now is your chance!

The basic idea of my dissertation is to put combinatorial species and related variants (including a port of the theory to HoTT) in a common categorical framework, and then be able to use them for working with/talking about data types. If you’re brave enough to read it, you’ll find lots of category theory and type theory, and very little code—but I can promise lots of examples and pretty pictures. I’ve tried to make it somewhat self-contained, so it may be a good way to learn a bit of category theory or homotopy type theory, if you’ve been curious to learn more about those topics.

You can find the latest draft here (auto-updated every time I commit); more generally, you can find the git repo here. If you notice any typos or grammatical errors, feel free to open a pull request. For anything more substantial—thoughts on the organization, notes or questions about things you found confusing, suggestions for improvement, pointers to other references—please send me an email (first initial last name at gmail). And finally, please send me any feedback by **September 9** at the latest (but the earlier the better). I need to have a final version to my committee by September 23.

Last but not least, if you’re interested to read it but don’t have the time or inclination to provide feedback on a draft, never fear—I’ll post an announcement when the final version is ready for your perusal!

### Manuel M T Chakravarty: What is currying (in Swift)?

A blog post by Ole Begemann has led some people interested in Swift wondering what exactly *curried functions* and *currying* are — for example, listen to the discussion on the Mobile Couch podcast Episode 37.

Let’s look at currying in Swift. Here is a *binary* add function

and next we have a *curried* version of the same function

The difference between the two is that add takes two arguments (two Ints) and returns an Int, whereas curriedAdd takes only *one* argument and returns a function of type (y: Int) -> Int. If you put those two definitions into a Playground, both add(1, y: 2) and curriedAdd(1)(y: 2) yield 3.

In add(1, 2), we supply two arguments at once, but in curriedAdd(1)(y: 2), we supply only one argument, get a new function as the result, and then, apply that new function to the second argument. In other words, add requires two arguments **at once**, whereas its curried variant requires the two arguments one after the other in two separate function calls.

This works not only for binary functions, but also for functions expecting three or more arguments. More generally, *currying* refers to the fact that any *n*-ary function (i.e., any function expecting *n* arguments) can be rewritten as a computationally equivalent function that doesn’t get all *n* arguments at once, but gets them one after the other, always returning an intermediate function for each of the *n* function applications.

That’s…interesting, but why should we care? Curried functions are more versatile than their uncurried counterparts. We can apply the function add only to two arguments. That’s it. In contrast, we can apply curriedAdd to either one or two arguments. If we want to define an increment function, we can do that easily in terms of curriedAdd:

let inc = curriedAdd(1)As expected, inc(y: 2) gives 3.

For a simple function, such as, add, this extra versatility is not very impressive. However, Ole’s blog post explains how this ultimately enables the target-action pattern in Swift and that is pretty impressive!

As a side note, in the functional language Haskell all functions are curried by default. In fact, the concept was called currying after the mathematician Haskell B. Curry in whose honour the language was called Haskell.

### Why doesn't this type-check?

Since there's an unambiguous choice here, why doesn't GHC compile this? Is there a name for what I'm trying to do, and is there a way that works to do it?

{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes #-} class Paired i t where compute :: Int -> t data A = A deriving Show data B instance Paired A Int where compute = id instance Paired B A where compute x = A -- I understand that this instance introduces ambiguity, but as long -- as there is only one valid instance of Paired in scope, why does -- this not compile? -- -- instance Paired A A where -- compute x = A constG :: A constG = compute 0 main = print constGHere's the error:

[1 of 1] Compiling Main ( plugin.hs, plugin.o ) plugin.hs:23:10: No instance for (Paired i0 A) arising from a use of ‘compute’ The type variable ‘i0’ is ambiguous Note: there is a potential instance available: instance Paired B A -- Defined at plugin.hs:12:10 In the expression: compute 0 In an equation for ‘constG’: constG = compute 0 submitted by jonreem[link] [4 comments]

### Haskell Platform 2014.2.0.0 is Released!

### Applicative Functors Insight

### How feasible would it be to create a library for GLSL shader combinators?

I recently got into learning to use OpenGL in Haskell. The OpenGL bindings are fairly infamous for being very stateful and imperative, and unsurprisingly not very pleasant for a functional programmer. One area where this could be sorted out is with shaders. As of yet, as far as I am aware, GLSL shaders can not even be written in Haskell.

Bear with me, as some of this may seem a little unwell-formed -- I literally only thought of it an hour or so ago in the bath. For the purposes of argument, define a Shader type:

data Shader u i o = Shader { runShader :: ... , ... }u is the type of the uniform values, i the inputs, and o the outputs. Typically we might have something like u = Either Array Int, etc.

Shader u is an instance of Arrow. The identity arrow would be that which mirrors inputs to outputs; arrow composition and first work in the obvious ways.

GLSL being a c-like language we can see that there are probably instances for Shader u of ArrowChoice and ArrowLoop.

This is just a vague idea, but it seems to suggest that a shader combinators library might be possible. There already exists a library for internal representation of the glsl format: language-glsl (although it currently only works with GLSL version 1.50).

If I had the necessary knowledge/patience, I would simply implement this myself, and attach a witty name to it, like Glacial or Colossal (ok, not that witty). Unfortunately, I have neither. Would some more experienced Haskellers care to comment on the feasability of the above?

submitted by tekn04[link] [11 comments]

### What’s a module system good for anyway?

### Mike Izbicki: Scribal traditions of "ancient" Hebrew scrolls

In 2006, I saw the dead sea scrolls in San Diego. The experience changed my life. I realized I knew nothing about ancient Judea, and decided to immerse myself in it. I studied biblical Hebrew and began a collection of Hebrew scrolls.

Each scroll is between 100 to 600 years old, and is a fragment of the *Torah*. These scrolls were used by synagogues throughout Southern Europe, Africa, and the Middle East. As we’ll see in a bit, each region has subtly different scribal traditions. But they all take their *Torah* very seriously.

The first thing that strikes me about a scroll is its color. Scrolls are made from animal skin, and the color is determined by the type of animal and method of curing the skin. The methods and animals used depend on the local resources, so color gives us a clue about where the scroll originally came from. For example, scrolls with a deep red color usually come from North Africa. As the scroll ages, the color may either fade or deepen slightly, but remains largely the same. The final parchment is called either *gevil* or *klaf* depending on the quality and preparation method.

The four scrolls below show the range of colors scrolls come in:

My largest scroll is about 60 feet long. Here I have it partially stretched out on the couch in my living room:

The scroll is about 300 years old, and contains most of Exodus, Leviticus, and Numbers. A complete *Torah* scroll would also have Genesis and Deuteronomy and be around 150 feet long. Sadly, this scroll has been damaged throughout its long life, and the damaged sections were removed.

As you can imagine, many hides were needed to make these large scrolls. These hides get sewn together to form the full scroll. You can easily see the stitching on the back of the scroll:

Also notice how rough that skin is! The scribes (for obvious reasons) chose to use the nice side of the skin to write on.

Here is a front end, rotated view of the same seam above. Some columns of text are separated at these seems, but some columns are not.

Animal hides come in many sizes. The hide in this image is pretty large and holds five columns of text:

But this hide is smaller and holds only three columns:

The coolest part of these scrolls is their calligraphy. Here’s a zoomed in look on one of the columns of text above:

There’s a lot to notice in this picture:

The detail is amazing. Many characters have small strokes decorating them. These strokes are called

*tagin*(or crowns in English). A bit farther down the page we’ll see different ways other scribal traditions decorate these characters. Because of this detail in every letter, a scribe (or*sopher*) might spend the whole day writing without finishing a single piece of parchment. The average*sopher*takes between nine months to a year to complete a*Torah*scroll.There are faint indentations in the parchment that the

*sopher*used to ensure he was writing straight. We learned to write straight in grade school by writing our letters on top of lines on paper. But in biblical Hebrew, the*sopher*writes their letters below the line!Hebrew is read and written right to left (backwards from English). To keep the left margin crisp, the letters on the left can be stretched to fill space. This effect is used in different amounts throughout the text. The stretching is more noticeable in this next section:

And sometimes the *sopher* goes crazy and stretches all the things:

If you look at the pictures above carefully, you can see that only certain letters get stretched: ת ד ח ה ר ל. These letters look nice when stretched because they have a single horizontal stroke.

The next picture shows a fairly rare example of stretching the letter ש. It looks much less elegant than the other stretched letters:

Usually these stretched characters are considered mistakes. An experienced *sopher* evenly spaces the letters to fill the line exactly. But a novice *sopher* can’t predict their space usage as well. When they hit the end of the line and realize they can’t fit another full word, they’ll add one of these stretched characters to fill the space.

In certain sections, however, stretched lettering is expected. It is one of the signs of poetic text in the *Torah*. For example, in the following picture, the *sopher* intentionally stretched each line, even when they didn’t have to:

Keeping the left margin justified isn’t just about looks. The *Torah* is divided into thematic sections called *parashot*. There are two types of breaks separating *parashot*. The *petuha* (open) is a jagged edge, much like we end paragraphs in English. The *setumah* (closed) break is a long space in the middle of the line. The picture below shows both types of breaks:

A *sopher* takes these *parashot* divisions very seriously. If the *sopher* accidentally adds or removes *parashot* from the text, the entire scroll becomes non-*kosher* and cannot be used. A mistake like this would typically be fixed by removing the offending piece of parchment from the scroll, rewriting it, and adding the corrected version back in. (We’ll see some pictures of less serious mistakes at the bottom of this page.)

The vast majority of of the *Torah* is formatted as simple blocks of text. But certain sections must be formatted in special ways. This is a visual cue that the text is more poetic.

The passage below is of Numbers 10:35-36. Here we see an example of the inverted nun character being used to highlight some text. This is the only section of the *Torah* where this formatting appears (although it also appears seven times in the book of psalms). The inverted nun characters are set all by themselves, and surround a command about the Ark of the Covenant:

It’s really cool when two different scrolls have sections that overlap. We can compare them side-by-side to watch the development of different scribal traditions. The image below shows two versions of Numbers 6:22-27.

The writing is almost identical in both versions, with one exception. On the first line with special formatting, the left scroll has two words in the right column: אמור להם, but the right scroll only has the world אמור) להם is the last word on the previous line). When the *sopher* is copying a scroll, he does his best to preserve the formatting in these special sections. But due to the vast Jewish diaspora, small mistakes like this get made and propagate. Eventually they form entirely new scribal traditions. (Note that if a single letter is missing from a *Torah*, then the *Torah* is not *kosher* and is considered unfit for use. These scribal differences are purely stylistic.)

Many individual characters and words also receive special formatting throughout the text. Both images below come from the same piece of parchment (in Genesis 23) and were created by the same *sopher*. The image on the left shows the letter פ in its standard form, and the image on the right shows it in a modified form.

The meaning of these special characters is not fully known, and every scribal tradition exhibits some variation in what letters get these extra decorations. In the scroll above, the whirled פ appears only once. But some scrolls exhibit the special character dozens of times. Here is another example where you can see a whirled פ a few letters to the right of its normal version:

Another special marker is when dots are placed over the Hebrew letters. The picture below comes from the story when Esau is reconciling with Jacob in Genesis 33. Normally, the dotted word would mean that Esau kissed Jacob in reconciliation; but tradition states that these dots indicate that Esau was being incincere. Some rabbis say that this word, when dotted, could be more accurately translated as Esau “bit” Jacob.

Next, let’s take a look at God’s name written in many different styles. In Hebrew, God’s name is written יהוה. Christians often pronounce God’s name as *Yahweh* or *Jehovah*. Jews, however, never say God’s name. Instead, they say the word *adonai*, which means “lord.” In English old testaments, anytime you see the word Lord rendered in small caps, the Hebrew is actually God’s name. When writing in English, Jews will usually write God’s name as *YHWH*. Removing the vowels is a reminder to not say the name out loud.

Below are nine selected images of *YHWH*. Each comes from a different scroll and illustrates the decorations added by a different scribal tradition. A few are starting to fade from age, but they were the best examples I could find in the same style. The simplest letters are in the top left, and the most intricate in the bottom right. In the same scroll, *YHWH* is always written in the same style.

The next image shows the word *YHWH* at the end of the line. The ה letters get stretched just like in any other word. When I first saw this I was surprised a *sopher* would stretch the name of God like this—the name of God is taken very seriously and must be handled according to special rules. I can just imagine rabbis 300 years ago getting into heated debates about whether or not this was *kosher*!

There is another oddity in the image above. The letter *yod* (the small, apostrophe looking letter at the beginning of *YHWH*) appears in each line. But it is written differently in the last line. Here, it is given two *tagin*, but everywhere else it only has one. Usually, the *sopher* consistently applies the same styling throughout the scroll. Changes like this typically indicate the *sopher* is trying to emphasize some aspect of the text. Exactly what the changes mean, however, would depend on the specific scribal tradition.

The more general word for god in Hebrew is אלוהים, pronounced *elohim*. This word can refer to either *YHWH* or a non-Jewish god. Here it is below in two separate scrolls:

Many Christians, when they first learn Hebrew, get confused by the word *elohim*. The ending *im* on Hebrew words is used to make a word plural, much like the ending *s* in English. (For example, the plural of *sopher* is *sophrim*.) Christians sometimes claim that because the Hebrew word for god looks plural, ancient Jews must have believed in the Christian doctrine of the trinity. But this is very wrong, and rather offensive to Jews.

Tradition has that Moses is the sole author of the *Torah*, and that Jewish *sophrim* have given us perfect copies of Moses’ original manuscripts. Most modern scholars, however, believe in the documentary hypothesis, which challenges this tradition. The hypothesis claims that two different writers wrote the *Torah*. One writer always referenced God as *YHWH*, whereas the other always referenced God as *elohim*. The main evidence for the documentary hypothesis is that some stories in the *Torah* are repeated twice with slightly different details; in one version God is always called *YHWH*, whereas in the other God is always called *elohim*. The documentary hypothesis suggests that some later editor merged two sources together, but didn’t feel comfortable editing out the discrepancies, so left them exactly as they were. Orthodox Jews reject the documentary hypothesis, but some strains of Judaism and most Christian denominations are willing to consider that the hypothesis might be true. This controversy is a very important distinction between different Jewish sects, but most Christians aren’t even aware of the controversy in their holy book.

The next two pictures show common gramatical modifications of the words *YHWH* and *elohim*: they have letters attached to them in the front. The word *YHWH* below has a ל in front. This signifies that something is being done to *YHWH* or for *YHWH*. The word *elohim* has a ה in front. This signifies that we’re talking about *the* God, not just *a* god. In Hebrew, prepositions like “to,” “for,” and “the” are not separate words. They’re just letters that get attached to the words they modify.

Names are very important in Hebrew. Most names are actually phrases. The name *Jacob*, for example, means “heel puller.” *Jacob* earned his name because he was pulling the heel of his twin brother *Esau* when they were born in Genesis 25:26. Below are two different versions of the word *Jacob*:

But names often change in the book of Genesis. In fact, *Jacob*’s name is changed to *Israel* in two separate locations: first in Genesis 32 after *Jacob* wrestles with “a man”; then again in Genesis 35 after *Jacob* builds an alter to *elohim*. (This is one of the stories cited as evidence for the documentary hypothesis.) The name *Israel* is appropriate because it literally means “persevered with God.” The *el* at the end of *Israel* is a shortened form of *elohim* and is another Hebrew word for god.

Here is the name Israel in two different scripts:

Another important Hebrew name is ישוע. In Hebrew, this name is pronounced *yeshua*, but Christians commonly pronounce it Jesus! The name literally translates as “salvation.” That’s why the angel in Matthew 1:21 and Luke 1:31 gives Jesus this name. My scrolls are only of the old testament, so I don’t have any examples to show of Jesus’ name!

To wrap up the discussion of scribal writing styles, let’s take a look at the most common phrase in the *Torah*: ודבר יהוה אל משה. This translates to “and the Lord said to Moses.” Here is is rendered in three different styles:

Now let’s move on to what happens when the *sophrim* make mistakes.

Copying all of these intricate characters was exhausting work! And hard! So mistakes are bound to happen. But if even a single letter is wrong anywhere in the scroll, the entire scroll is considered unusable. The rules are incredibly strict, and this is why Orthodox Jews reject the documentary hypothesis. To them, it is simply inconceivable to use a version of the *Torah* that was combined from multiple sources.

The most common way to correct a mistake is to scratch off the outer layer of the parchment, removing the ink. In the picture below, the *sopher* has written the name *Aaron* (אהרן) over the scratched off parchment:

The next picture shows the end of a line. Because of the mistake, however, the *sopher* must write several characters in the margin of the text, ruining the nice sharp edge they created with the stretched characters. Writing that enters the margins like this is not *kosher*.

Sometimes a *sopher* doesn’t realize they’ve made a mistake until several lines later. In the picture below, the *sopher* has had to scratch off and replace three and a half lines:

Scratching the parchment makes it thinner and weaker. Occasionally the parchment is already very thin, and scratching would tear through to the other side. In this case, the *sopher* can take a thin piece of blank parchment and attach it to the surface. In the following picture, you can see that the attached parchment has a different color and texture.

The next picture shows a rather curious instance of this technique. The new parchment is placed so as to cover only parts of words on multiple lines. I can’t imagine how a *sopher* would make a mistake that would best be fixed in this manner. So my guess is that this patch was applied some time later, by a different *sopher* to repair some damage that had occurred to the scroll while it was in use.

Our last example of correcting mistakes is the most rare. Below, the *sopher* completely forgot a word when copying the scroll, and added it in superscript above the standard text:

If we zoom in, you can see that the superscript word is slightly more faded than the surrounding text. This might be because the word was discovered to be missing a long time (days or weeks) after the original text was written, so a different batch of ink was used to write the word.

Since these scrolls are several hundred years old, they’ve had plenty of time to accumulate damage. When stored improperly, the parchment can tear in some places and bunch up in others:

One of the worst things that can happen to a scroll is water. It damages the parchment and makes the ink run. If this happens, the scroll is ruined permanently.

If you’ve read this far and enjoyed it, then you should learn biblical Hebrew. It’s a lot of fun! You can start right now at any of these great sites:

http://foundationstone.com.au - geared for the Jewish reader, covers both biblical and modern Hebrew

http://hebrew4christians.com - very good site because it also explains lots of Jewish customs that may be unfamiliar to you; this should probably be more accurately named “hebrew4gentiles”

http://www.ulpan.net - the focus is on modern Hebrew, but the basics are the same

http://www.101languages.net/hebrew - also modern Hebrew

When you’re ready to get serious, you’ll need to get some books. The books that helped me the most were:

These books all have lots of exercises and make self study pretty simple. The Biblical Hebrew Workbook is for absolute beginners. Within the first few sessions you’re translating actual bible verses and learning the nuances that get lost in the process. I spent two days a week with this book, two hours at each session. It took about four months to finish.

The other two books start right where the workbook stops. They walk you through many important passages and even entire books of the old testament. After finishing these books, I felt comfortable enough to start reading the old testament by myself. Of course I was still very slow and was constantly looking things up in the dictionary!

For me, learning the vocabulary was the hardest part. I used a great free piece of software called FoundationStone to help. The program remembers which words you struggle with and quizes you on them more frequently.

Finally, let’s end with my favorite picture of them all. Here we’re looking down through a rolled up *Torah* scroll at one of my sandals.

### Edward Z. Yang: What’s a module system good for anyway?

This summer, I've been working at Microsoft Research implementing Backpack, a module system for Haskell. Interestingly, Backpack is not really a single monolothic feature, but, rather, an agglomeration of small, infrastructural changes which combine together in an interesting way. In this series of blog posts, I want to talk about what these individual features are, as well as how the whole is greater than the sum of the parts.

But first, there's an important question that I need to answer: **What's a module system good for anyway?** Why should you, an average Haskell programmer, care about such nebulous things as *module systems* and *modularity*. At the end of the day, you want your tools to solve specific problems you have, and it is sometimes difficult to understand what problem a module system like Backpack solves. As tomejaguar puts it: "Can someone explain clearly the precise problem that Backpack addresses? I've read the paper and I know the problem is 'modularity' but I fear I am lacking the imagination to really grasp what the issue is."

Look no further. In this blog post, I want to talk concretely about problems Haskellers have today, explain what the underlying causes of these problems are, and say why a module system could help you out.

The String, Text, ByteString problemAs experienced Haskellers are well aware, there are multitude of string types in Haskell: String, ByteString (both lazy and strict), Text (also both lazy and strict). To make matters worse, there is no one "correct" choice of a string type: different types are appropriate in different cases. String is convenient and native to Haskell'98, but very slow; ByteString is fast but are simply arrays of bytes; Text is slower but Unicode aware.

In an ideal world, a programmer might choose the string representation most appropriate for their application, and write all their code accordingly. However, this is little solace for library writers, who don't know what string type their users are using! What's a library writer to do? There are only a few choices:

- They "commit" to one particular string representation, leaving users to manually convert from one representation to another when there is a mismatch. Or, more likely, the library writer used the default because it was easy. Examples: base (uses Strings because it completely predates the other representations), diagrams (uses Strings because it doesn't really do heavy string manipulation).
- They can provide separate functions for each variant, perhaps identically named but placed in separate modules. This pattern is frequently employed to support both strict/lazy variants Text and ByteStringExamples: aeson (providing decode/decodeStrict for lazy/strict ByteString), attoparsec (providing Data.Attoparsec.ByteString/Data.Attoparsec.ByteString.Lazy), lens (providing Data.ByteString.Lazy.Lens/Data.ByteString.Strict.Lens).
- They can use type-classes to overload functions to work with multiple representations. The particular type class used hugely varies: there is ListLike, which is used by a handful of packages, but a large portion of packages simply roll their own. Examples: SqlValue in HDBC, an internal StringLike in tagsoup, and yet another internal StringLike in web-encodings.

The last two methods have different trade offs. Defining separate functions as in (2) is a straightforward and easy to understand approach, but you are still saying *no* to modularity: the ability to support multiple string representations. Despite providing implementations for each representation, the user still has to commit to particular representation when they do an import. If they want to change their string representation, they have to go through all of their modules and rename their imports; and if they want to support multiple representations, they'll still have to write separate modules for each of them.

Using type classes (3) to regain modularity may seem like an attractive approach. But this approach has both practical and theoretical problems. First and foremost, how do you choose which methods go into the type class? Ideally, you'd pick a minimal set, from which all other operations could be derived. However, many operations are most efficient when directly implemented, which leads to a bloated type class, and a rough time for other people who have their own string types and need to write their own instances. Second, type classes make your type signatures more ugly String -> String to StringLike s => s -> s and can make type inference more difficult (for example, by introducing ambiguity). Finally, the type class StringLike has a very different character from the type class Monad, which has a minimal set of operations and laws governing their operation. It is difficult (or impossible) to characterize what the laws of an interface like this should be. All-in-all, it's much less pleasant to program against type classes than concrete implementations.

Wouldn't it be nice if I could import String, giving me the type String and operations on it, but then later decide which concrete implementation I want to instantiate it with? This is something a module system can do for you! This Reddit thread describes a number of other situations where an ML-style module would come in handy.

(PS: Why can't you just write a pile of preprocessor macros to swap in the implementation you want? The answer is, "Yes, you can; but how are you going to type check the thing, without trying it against every single implementation?")

Destructive package reinstallsHave you ever gotten this error message when attempting to install a new package?

$ cabal install hakyll cabal: The following packages are likely to be broken by the reinstalls: pandoc-1.9.4.5 Graphalyze-0.14.0.0 Use --force-reinstalls if you want to install anyway.Somehow, Cabal has concluded that the only way to install hakyll is to reinstall some dependency. Here's one situation where a situation like this could come about:

- pandoc and Graphalyze are compiled against the latest unordered-containers-0.2.5.0, which itself was compiled against the latest hashable-1.2.2.0.
- hakyll also has a dependency on unordered-containers and hashable, but it has an upper bound restriction on hashable which excludes the latest hashable version. Cabal decides we need to install an old version of hashable, say hashable-0.1.4.5.
- If hashable-0.1.4.5 is installed, we also need to build unordered-containers against this older version for Hakyll to see consistent types. However, the resulting version is the same as the preexisting version: thus, reinstall!

The root cause of this error an invariant Cabal
currently enforces on a package database: there can only be *one* instance
of a package for any given package name and version. In particular,
this means that it is not possible to install a package multiple times,
compiled against different dependencies. This is a bit troublesome,
because sometimes you really do want the same package installed multiple
times with different dependencies: as seen above, it may be the only way to fulfill
the version bounds of all packages involved.
Currently, the only way to work around this problem is to use a Cabal sandbox (or blow away your package database and reinstall everything, which is basically the same thing).

You might be wondering, however, how could a module system possibly help with this? It doesn't... at least, not directly. Rather, nondestructive reinstalls of a package are a critical feature for implementing a module system like Backpack (a package may be installed multiple times with different concrete implementations of modules). Implementing Backpack necessitates fixing this problem, moving Haskell's package management a lot closer to that of Nix's or NPM.

Version bounds and the neglected PVPWhile we're on the subject of cabal-install giving errors, have you ever gotten this error attempting to install a new package?

$ cabal install hledger-0.18 Resolving dependencies... cabal: Could not resolve dependencies: # pile of outputThere are a number of possible reasons why this could occur, but usually it's because some of the packages involved have over-constrained version bounds (especially upper bounds), resulting in an unsatisfiable set of constraints. To add insult to injury, often these bounds have no grounding in reality (the package author simply guessed the range) and removing it would result in a working compilation. This situation is so common that Cabal has a flag --allow-newer which lets you override the upper bounds of packages. The annoyance of managing bounds has lead to the development of tools like cabal-bounds, which try to make it less tedious to keep upper bounds up-to-date.

But as much as we like to rag on them, version bounds have a very important function: they prevent you from attempting to compile packages against dependencies which don't work at all! An under-constrained set of version bounds can easily have compiling against a version of the dependency which doesn't type check.

How can a module system help? At the end of the day, version numbers are trying to capture something about the API exported by a package, described by the package versioning policy. But the current state-of-the-art requires a user to manually translate changes to the API into version numbers: an error prone process, even when assisted by various tools. A module system, on the other hand, turns the API into a first-class entity understood by the compiler itself: a *module signature.* Wouldn't it be great if packages depended upon signatures rather than versions: then you would never have to worry about version numbers being inaccurate with respect to type checking. (Of course, versions would still be useful for recording changes to semantics not seen in the types, but their role here would be secondary in importance.) Some full disclosure is warranted here: I am not going to have this implemented by the end of my internship, but I'm hoping to make some good infrastructural contributions toward it.

If you skimmed the introduction to the Backpack paper, you might have come away with the impression that Backpack is something about random number generators, recursive linking and applicative semantics. While these are all true "facts" about Backpack, they understate the impact a good module system can have on the day-to-day problems of a working programmer. In this post, I hope I've elucidated some of these problems, even if I haven't convinced you that a module system like Backpack actually goes about solving these problems: that's for the next series of posts. Stay tuned!