Planet Haskell

May 21, 2017

Neil Mitchell

Proving fib equivalence

Summary: Using Idris I proved the exponential and linear time fib functions are equivalent.

The Haskell wiki proclaims that Implementing the Fibonacci sequence is considered the "Hello, world!" of Haskell programming. It also provides multiple versions of fib - an exponential version and a linear version. We can translate these into Idris fairly easily:

fibExp : Nat -> Nat
fibExp Z = 0
fibExp (S Z) = 1
fibExp (S (S n)) = fibExp (S n) + fibExp n

fibLin' : Nat -> Nat -> Nat -> Nat
fibLin' Z a b = b
fibLin' (S n) a b = fibLin' n (a + b) a

fibLin : Nat -> Nat
fibLin n = fibLin' n 1 0

We've made the intermediate go function in fibLin top-level, named it fibLib' and untupled the accumulator - but it's still fundamentally the same. Now we've got the power of Idris, it would be nice to prove that fibExp and fibLin are equivalent. To do that, it's first useful to think about why fibLib' works at all. In essence we're decrementing the first argument, and making the next two arguments be fib of increasingly large values. If we think more carefully we can come up with the invariant:

fibLinInvariant : (d : Nat) -> (u : Nat) ->
fibLin' d (fibExp (1+u)) (fibExp u) = fibExp (d+u)

Namely that at all recursive calls we must have the fib of two successive values (u and u+1), and after d additional loops we end up with fib (d+u). Actually proving this invariant isn't too hard:

fibLinInvariant Z u = Refl
fibLinInvariant (S d) u =
rewrite fibLinInvariant d (S u) in
rewrite plusSuccRightSucc d u in

Idris simplifies the base case away for us. For the recursive case we apply the induction hypothesis to leave us with:

fibExp (plus d (S u)) = fibExp (S (plus d u))

Ignoring the fibExp we just need to prove d+(u+1) = (d+u)+1. That statement is obviously true because + is associative, but in our particular case, we use plusSuccRightSucc which is the associative lemma where +1 is the special S constructor. After that, everything has been proven.

Armed with the fundamental correctness invariant for fibLib, we can prove the complete equivalence.

fibEq : (n : Nat) -> fibLin n = fibExp n
fibEq n =
rewrite fibLinInvariant n 0 in
rewrite plusZeroRightNeutral n in

We appeal to the invariant linking fibLin' and finExp, do some minor arithmetic manipulation (x+0 = x), and are done. Note that depending on exactly how you define the fibLinInvariant you require different arithmetic lemmas, e.g. if you write d+u or u+d. Idris is equipped with everything required.

I was rather impressed that proving fib equivalence wasn't all that complicated, and really just requires figuring out what fundamental property makes fibLin actually work. In many ways the proof makes things clearer.

by Neil Mitchell ( at May 21, 2017 08:01 PM

May 19, 2017

Daniel Mlot (duplode)

Traversable: A Remix

Traversable is a fun type class. It lies at a crossroad, where many basic Haskell concepts meet, and it can be presented in multiple ways that provide complementary intuitions. In this post, Traversable will be described from a slightly unusual point of view, or at least one that is not put into foreground all that often. We will suspend for a moment the picture of walking across a container while using an effectful function, and instead start by considering what can be done with effectful functions.

Weird fishes

Let’s begin with a familiar sight:

a -> F b

There are quite a few overlapping ways of talking about functions with such a type. If F is a Functor, we can say the function produces a functorial context; if it is an Applicative, we (also) say it produces an effect; and if it is a Monad we (also) call it a Kleisli arrow. Kleisli arrows are the functions we use with (>>=). Kleisli arrows for a specific Monad form a category, with return as identity and the fish operator, (<=<), as composition. If we pick join as the fundamental Monad operation, (<=<) can be defined in terms of it as:

(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
g <=< f = join . fmap g . f

The category laws, then, become an alternative presentation of the monad laws:

return <=< f = f
f <=< return = f
(h <=< g) <=< f = h <=< (g <=< f)

All of that is very well-known. Something less often noted, though, is that there is an interesting category for a -> F b functions even if F is not a Monad. Getting to it is amusingly easy: we just have to take the Kleisli category operators and erase the monad-specific parts from their definitions. In the case of (<=<), that means removing the join (and, for type bookkeeping purposes, slipping in a Compose in its place):

(<%<) :: (Functor f, Functor g) =>
    (b -> g c) -> (a -> f b) -> (a -> Compose f g c)
g <%< f = Compose . fmap g . f

While (<=<) creates two monadic layers and merges them, (<%<) creates two functorial layers and leaves both in place. Note that doing away with join means the Functors introduced by the functions being composed can differ, and so the category we are setting up has all functions that fit Functor f => a -> f b as arrows. That is unlike what we have with (<=<) and the corresponding Kleisli categories, which only concern a single specific monad.

As for return, not relying on Monad means we need a different identity. Given the freedom to pick any Functor mentioned just above, it makes perfect sense to replace bringing a value into a Monad in a boring way by bringing a value into the boring Functor par excellence, Identity:

Identity :: a -> Identity a

With (<%<) as composition and Identity as identity, we can state the following category laws:

Identity <%< f ~ f
f <%< Identity ~ f
(h <%< g) <%< f ~ h <%< (g <%< f)

Why didn’t I write them as equalities? Once the definition of (<%<) is substituted, it becomes clear that they do not hold literally as equalities: the left hand sides of the identity laws will have a stray Identity, and the uses of Compose on either side of the associativity law will be associated differently. Since Identity and Compose are essentially bookkeeping boilerplate, however, it would be entirely reasonable to ignore such differences. If we do that, it becomes clear that the laws do hold. All in all, we have a category, even though we can’t go all the way and shape it into a Category instance, not only due to the trivialities we chose to overlook, but also because of how each a -> F b function introduces a functorial layer F in a way that is not reflected in the target object b.

The first thing to do once after figuring out we have a category in our hands is looking for functors involving it.1 One of the simplest paths towards one is considering a way to, given some Functor T, change the source and target objects in an a -> F b function to T a and T b (that is precisely what fmap does with regular functions). This would give an endofunctor, whose arrow mapping would have a signature shaped like this:

(a -> F b) -> T a -> F (T b)

This signature shape, however, should ring a bell:

class (Functor t, Foldable t) => Traversable t where
    traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
    -- etc.

If traverse were the arrow mapping of our endofunctor, the relevant functor laws would be:

traverse Identity = Identity
traverse (g <%< f) = traverse g <%< traverse f

Substituting the definition of (<%<) reveals these are the identity and composition laws of Traversable:

traverse Identity = Identity
traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f

There it is: a Traversable instance is an endofunctor for a category made of arbitrary context-producing functions.2

Is it really, though? You may have noticed I have glossed over something quite glaring: if (<%<) only involved Functor constraints, where does the Applicative in traverse comes from?


Let’s pretend we have just invented the Traversable class by building it around the aforementioned endofunctor. At this point, there is no reason for using anything more restrictive than Functor in the signature of its arrow mapping:

-- Tentative signature:
traverse :: (Functor f, Traversable t) => (a -> f b) -> t a -> f (t b)

The natural thing to do now is trying to write traverse for various choices of t. Let’s try it for one of the simplest Functors around: the pair functor, (,) e – values with something extra attached:

instance Traversable ((,) e) where
    -- traverse :: Functor f => (a -> f b) -> (e, a) -> f (e, b)
    traverse f (e, x) = ((,) e) <$> f x

Simple enough: apply the function to the contained value, and then shift the extra stuff into the functorial context with fmap. The resulting traverse follows the functor laws just fine.

If we try to do it for different functors, though, we quickly run into trouble. Maybe looks simple enough…

instance Traversable Maybe where
    -- traverse :: Functor f => (a -> f b) -> Maybe a -> f (Maybe b)
    traverse f (Just x) = Just <$> f x
    traverse f Nothing  = -- ex nihilo

… but the Nothing case stumps us: there is no value that can be supplied to f, which means the functorial context would have to be created out of nothing.

For another example, consider what we might do with an homogeneous pair type (or, if you will, a vector of length two):

data Duo a = Duo a a

instance Functor Duo where
    fmap f (Duo x y) = Duo (f x) (f y)

instance Traversable Duo where
    -- traverse :: Functor f => (a -> f b) -> Duo a -> f (Duo b)
    traverse f (Duo x y) = -- dilemma

Here, we seemingly have to choose between applying f to x or to y, and then using fmap (\z -> Duo z z) on the result. No matter the choice, though, discarding one of the values means the functor laws will be broken. A lawful implementation would require somehow combining the functorial values f x and f y.

As luck would have it, though, there is a type class which provides ways to both create a functorial context out of nothing and to combine functorial values: Applicative. pure solves the first problem; (<*>), the second:

instance Traversable Maybe where
    -- traverse :: Applicative f => (a -> f b) -> Maybe a -> f (Maybe b)
    traverse f (Just x) = Just <$> f x
    traverse f Nothing  = pure Nothing

instance Traversable Duo where
    -- traverse :: Applicative f => (a -> f b) -> Duo a -> f (Duo b)
    traverse f (Duo x y) = Duo <$> f x <*> f y

Shifting to the terminology of containers for a moment, we can describe the matter by saying the version of traverse with the Functor constraint can only handle containers that hold exactly one value. Once the constraint is strengthened to Applicative, however, we have the means to deal with containers that may hold zero or many values. This is a very general solution: there are instances of Traversable for the Identity, Const, Sum, and Product functors, which suffice to encode any algebraic data type.3 That explains why the DeriveTraversable GHC extension exists. (Note, though, that Traversable instances in general aren’t unique.)

It must be noted that our reconstruction does not reflect how Traversable was discovered, as the idea of using it to walk across containers holding an arbitrary number of values was there from the start. That being so, Applicative plays an essential role in the usual presentations of Traversable. To illustrate that, I will now paraphrase Definition 3.3 in Jaskelioff and Rypacek’s An Investigation of the Laws of Traversals. It is formulated not in terms of traverse, but of sequenceA:

sequenceA :: (Applicative f, Traversable t) => t (f a) -> f (t a)

sequenceA is characterised as a natural transformation in the category of applicative functors which “respects the monoidal structure of applicative functor composition”. It is worth it to take a few moments to unpack that:

  • The category of applicative functors has what the Data.Traversable documentation calls “applicative transformations” as arrows – functions of general type (Applicative f, Applicative g) => f a -> g a which preserve pure and (<*>).

  • sequenceA is a natural transformation in the aforementioned category of applicative functors. The two functors it maps between amount to the two ways of composing an applicative functor with the relevant traversable functor. The naturality law of Traversable

    -- t is an applicative transformation
    t . sequenceA = sequenceA . fmap t

… captures that fact (which, thanks to parametricity, is a given in Haskell).

  • Applicative functors form a monoid, with Identity as unit and functor composition as multiplication. sequenceA preserves these monoidal operations, and the identity and composition laws of Traversable express that:

    sequenceA . fmap Identity = Identity
    sequenceA . fmap Compose = Compose . fmap sequenceA . sequenceA

All of that seems only accidentally related to what we have done up to this point. However, if sequenceA is taken as the starting point, traverse can be defined in terms of it:

traverse f = sequenceA . fmap f

Crucially, the opposite path is also possible. It follows from parametricity4 that…

traverse f = traverse id . fmap f

… which allows us to start from traverse, define…

sequenceA = traverse id

… and continue as before. At this point, our narrative merges with the traditional account of Traversable.

A note about lenses

In the previous section, we saw how using Applicative rather than Functor in the type of traverse made it possible to handle containers which don’t necessarily hold just one value. It is not a coincidence that, in lens, this is precisely the difference between Traversal and Lens:

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

A Lens targets exactly one value. A Traversal might reach zero, one or many targets, which requires a strengthening of the constraint. Van Laarhoven (i.e. lens-style) Traversals and Lenses can be seen as a straightforward generalisation of the traverse-as-arrow-mapping view we have been discussing here, in which the, so to say, functoriality of the container isn’t necessarily reflected at type level in a direct way.

A note about profunctors

Early on, we noted that (<%<) gave us a category that cannot be expressed as a Haskell Category because its composition is too quirky. We have a general-purpose class that is often a good fit for things that look like functions, arrows and/or Category instances but don’t compose in conventional ways: Profunctor. And sure enough: profunctors defines a profunctor called Star

-- | Lift a 'Functor' into a 'Profunctor' (forwards).
newtype Star f d c = Star { runStar :: d -> f c }

… which corresponds to the arrows of the category we presented in the first section. It should come as no surprise that Star is an instance of a class called Traversing

-- Abridged definition.
class (Choice p, Strong p) => Traversing p where
  traverse' :: Traversable f => p a b -> p (f a) (f b)
  wander :: (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t

instance Applicative m => Traversing (Star m) where
  traverse' (Star m) = Star (traverse m)
  wander f (Star amb) = Star (f amb)

… which is a profunctor-oriented generalisation of Traversable.

Amusingly, it turns out there is a baroque way of expressing (<%<) composition with the profunctors vocabulary. Data.Profunctor.Composition gives us a notion of profunctor composition:

data Procompose p q d c where
  Procompose :: p x c -> q d x -> Procompose p q d c

Procompose simply pairs two profunctorial values with matching extremities. That is unlike Category composition, which welds two arrows5 into one:

(.) :: Category cat => cat b c -> cat a b -> cat a c

The difference is rather like that between combining functorial layers at type level with Compose and fusing monadic layers with join6.

Among a handful of other interesting things, Data.Functor.Procompose offers a lens-style isomorphism

stars :: Functor f => Iso' (Procompose (Star f) (Star g) d c) (Star (Compose f g) d c)

… which gives us a rather lyrical encoding of (<%<):

GHCi> import Data.Profunctor
GHCi> import Data.Profunctor.Composition
GHCi> import Data.Profunctor.Traversing
GHCi> import Data.Functor.Compose
GHCi> import Control.Lens
GHCi> f = Star $ \x -> print x *> pure x
GHCi> g = Star $ \x -> [0..x]
GHCi> getCompose $ runStar (traverse' (view stars (g `Procompose` f))) [0..2]

If you feel like playing with that, note that Data.Profunctor.Sieve offers a more compact (though prosaic) spelling:

GHCi> import Data.Profunctor.Sieve
GHCi> :t sieve
sieve :: Sieve p f => p a b -> a -> f b
GHCi> getCompose $ traverse (sieve (g `Procompose` f)) [0..2]

Further reading

  • The already mentioned An Investigation of the Laws of Traversals, by Mauro Jaskelioff and Ondrej Rypacek, is a fine entry point to the ways of formulating Traversable. It also touches upon some important matters I didn’t explore here, such as how the notion of container Traversable mobilises can be made precise, or the implications of the Traversable laws. I plan to discuss some aspects of these issues in a follow-up post.

  • Will Fancher’s Profunctors, Arrows, & Static Analysis is a good applied introduction to profunctors. In its final sections, it demonstrates some use cases for the Traversing class mentioned here.

  • The explanation of profunctor composition in this post is intentionally cursory. If you want to dig deeper, Dan Piponi’s Profunctors in Haskell can be a starting point. (N.B.: Wherever you see “cofunctor” there, read “contravariant functor” instead). Another option is going to Bartosz Milewski’s blog and searching for “profunctor” (most of the results will be relevant).

<section class="footnotes">
  1. For why that is a good idea, see Gabriel Gonzalez’s The functor design pattern.

  2. A more proper derivation for the results in this section can be found in this Stack Overflow answer, which I didn’t transcribe here to avoid boring you.

  3. Suffice, that is, with the help of the trivial data types, () (unit) and Void. As an arbitrary example, Maybe can be encoded using this functor toolkit as Sum (Const ()) Identity.

  4. The property is an immediate consequence of the free theorem for traverse. Cf. this Stack Overflow answer by Rein Heinrichs.

  5. I mean “arrows” in the general sense, and not necessarily Arrows as in Control.Arrow!

  6. This is not merely a loose analogy. For details, see Bartosz Milewski’s Monoids on Steroids, and and in particular its section about Arrows.

Comment on GitHub (see the full post for a reddit link)

by Daniel Mlot at May 19, 2017 07:30 AM

May 16, 2017

Neil Mitchell

Idris reverse proofs

Summary: I proved O(n) reverse is equivalent to O(n^2) reverse.

Following on from my previous post I left the goal of given two reverse implementations:

reverse1 : List a -> List a
reverse1 [] = []
reverse1 (x :: xs) = reverse1 xs ++ [x]

rev2 : List a -> List a -> List a
rev2 acc [] = acc
rev2 acc (x :: xs) = rev2 (x :: acc) xs

reverse2 : List a -> List a
reverse2 = rev2 []

Proving the following laws hold:

proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs

The complete proofs are available in my Idris github repo, and if you want to get the most out of the code, it's probably best to step through the types in Idris. In this post I'll talk through a few of the details.

Directly proving the reverse1 (reverse1 x) = x by induction is hard, since the function doesn't really follow so directly. Instead we need to define a helper lemma.

proof_reverse1_append : (xs : List a) -> (ys : List a) ->
reverse1 (xs ++ ys) = reverse1 ys ++ reverse1 xs

Coming up with these helper lemmas is the magic of writing proofs - and is part intuition, part thinking about what might be useful and part thinking about what invariants are obeyed. With that lemma, you can prove by induction on the first argument (which is the obvious one to chose since ++ evaluates the first argument first). Proving the base case is trivial:

proof_reverse1_append [] ys =
rewrite appendNilRightNeutral (reverse1 ys) in

The proof immediately reduces to reverse1 ys == reverse1 ys ++ [] and we can invoke the standard proof that if ++ has [] on the right we can ignore it. After applying that rewrite, we're straight back to Refl.

The :: is not really any harder, we immediately get to reverse1 ys ++ (reverse1 xs ++ [x]), but bracketed the wrong way round, so have to apply appendAssociative to rebracket so it fits the inductive lemma. The proof looks like:

proof_reverse1_append (x :: xs) ys =
rewrite appendAssociative (reverse1 ys) (reverse1 xs) [x] in
rewrite proof_reverse1_append xs ys in Refl

Once we have the proof of how to move reverse1 over ++ we use it inductively to prove the original lemma:

proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse1_reverse1 [] = Refl
proof_reverse1_reverse1 (x :: xs) =
rewrite proof_reverse1_append (reverse1 xs) [x] in
rewrite proof_reverse1_reverse1 xs in

For the remaining two proofs, I first decided to prove reverse1 x = reverse2 x and then prove the reverse2 (reverse2 x) = x in terms of that. To prove equivalence of the two functions I first needed information about the fundamental property that rev2 obeys:

proof_rev : (xs : List a) -> (ys : List a) ->
rev2 xs ys = reverse2 ys ++ xs

Namely that the accumulator can be tacked on the end. The proof itself isn't very complicated, although it does require two calls to the inductive hypothesis (you basically expand out rev2 on both sides and show they are equivalent):

proof_rev xs [] = Refl
proof_rev xs (y :: ys) =
rewrite proof_rev [y] ys in
rewrite sym $ appendAssociative (rev2 [] ys) [y] xs in
rewrite proof_rev (y :: xs) ys in

The only slight complexity is that I needed to apply sym to switch the way the appendAssocative proof is applied. With that proof available, proving equivalence isn't that hard:

proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs
proof_reverse1_reverse2 [] = Refl
proof_reverse1_reverse2 (x :: xs) =
rewrite proof_rev [x] xs in
rewrite proof_reverse1_reverse2 xs in

In essence the proof_rev term shows that rev behaves like the O(n^2) reverse.

Finally, actually proving that reverse2 (reverse2 x) is true just involves replacing all the occurrences of reverse2 with reverse1, then applying the proof that the property holds for reverse1. Nothing complicated at all:

proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse2_reverse2 xs =
rewrite sym $ proof_reverse1_reverse2 xs in
rewrite sym $ proof_reverse1_reverse2 (reverse1 xs) in
rewrite proof_reverse1_reverse1 xs in

If you've got this far and are still hungry for more proof exercises I recommend Exercises on Generalizing the Induction Hypothesis which I have now worked through (solutions if you want to cheat).

by Neil Mitchell ( at May 16, 2017 08:08 PM

May 15, 2017

Brent Yorgey

Algorithms lecture notes and assignments

I just finished teaching our algorithms course for the second time. The first time around, last spring, I was always scrambling at the last minute to prepare for class, make new assignments, and so on (although I did have some excellent material from Brent Heeringa to start with). This time around, I had a bit more breathing room to develop a fuller set of assignments and actually TeX up all my hand-written lecture notes. The course is loosely based on the approach taken by Kleinberg and Tardos, though I don’t really rely on the book.

Feel free to use any of the lecture notes, assignments, or even exam questions. I didn’t leave the exams linked by accident; I use an exam format where the students have a week or so to prepare solutions to the exam, using any resources they want, and then have to come in on exam day and write down their solutions without referring to anything (I got this idea from Scott Weinstein). So leaving the exams posted publically on the web isn’t a problem for me.

Please don’t ask for solutions; I won’t give any, even if you are an instructor. But questions, comments, bug reports, etc. are most welcome.

by Brent at May 15, 2017 06:10 PM

May 11, 2017

Mark Jason Dominus

Zomg lots more anagram stuff

I'm almost done with anagrams. For now, anyway. I think. This article is to mop up the last few leftover anagram-related matters so that I can put the subject to rest.

(Earlier articles: [1] [2] [3] [•] )

Code is available

Almost all the code I wrote for this project is available on Github.

The documentation is not too terrible, I think.

Anagram lists are available

I have also placed my scored anagram lists on my web site. Currently available are:

  • Original file from the 1990s. This contains 23,521 anagram pairs, the results of my original scoring algorithm on a hand-built dictionary that includes the Unix spellcheck dictionary (/usr/dict/words), the Webster's Second International Dictionary word list, and some lexicons copied from a contemporaneous release of WordNet. This file has been in the same place on my web site since 1997 and is certainly older than that.

  • New file from February. Unfortunately I forget what went into this file. Certainly everything in the previous file, and whatever else I had lying around, probably including the Moby Word Lists. It contains 38,333 anagram pairs.

  • Very big listing of Wikipedia article titles. (11 MB compressed) I acquired the current list of article titles from the English Wikipedia; there are around 13,000,000 of these. I scored these along with the other lexicons I had on hand. The results include 1,657,150 anagram pairs. See below for more discussion of this.

!‌!Con talk

On Saturday I gave a talk about the anagram-scoring work at !‌!Con in New York. The talk was not my best work, since I really needed 15 minutes to do a good job and I was unwilling to cut it short enough. (I did go overtime, which I deeply regret.) At least nobody came up to me afterward and complained.

Talk materials are on my web site and I will link other talk-related stuff from there when it becomes available. The video will be available around the end of May, and the text transcript probably before that.

[ Addendum 20170518: The video is available thanks to Confreaks. ]

Both algorithms are exponential

The day after the talk an attendee asked me a very good question: why did I say that one algorithm for scoring algorithms was better than the other, when they are both exponential? (Sorry, I don't remember who you were—if you would like credit please drop me a note.)

The two algorithms are:

  • A brute-force search to construct all possible mappings from word A to word B, and then calculate the minimum score over all mappings (more details)

  • The two words are converted into a graph; we find the maximum independent set in the graph, and the size of the MIS gives the score (more details)

The answer to this excellent question begins with: just because two problems are both hard doesn't mean they are equally hard. In this case, the MIS algorithm is better for several reasons:

  1. The number of possible mappings from A to B depends on the number of repeated letters in each word. For words of length n, in the worst case this is something like . This quantity is superexponential; it eventually exceeds for all constants . The naïve algorithm for MIS is only exponential, having .

  2. The problem size for the mapping algorithm depends on the number of repeated letters in the words. The problem size for the MIS algorithm depends on the number of shared adjacent letter pairs in the two words. This is almost always much smaller.

  3. There appears to be no way to score all the mappings without constructing the mappings and scoring them. In contrast, MIS is well-studied and if you don't like the obvious algorithm you can do something cleverer that takes only .

  4. Branch-and-bound techniques are much more effective for the MIS problem, and in this particular case we know something about the graph structure, which can be exploited to make them even more effective. For example, when calculating the score for

    chromophotolithograph photochromolithograph

    my MIS implementation notices the matching trailing olithograph parts right away, and can then prune out any part of the MIS search that cannot produce a mapping with fewer than 11 chunks. Doing this in the mapping-generating algorithm is much more troublesome.

Stuff that didn't go into the talk

On Wednesday I tried out the talk on Katara and learned that it was around 75% too long. I had violated my own #1 content rule: “Do not begin with a long introduction”. My draft talk started with a tour of all my favorite anagrams, with illustrations. Included were:

  • “Please” and “asleep” and “elapse”.

  • “Spectrum” and “crumpets” ; my wife noticed this while we were at a figure-skating event at the Philadelphia Spectrum, depicted above.

  • “English” and “shingle” ; I came up with this looking at a teabag while at breakfast with my wife's parents. This prompted my mother-in-law to remark that it must be hard to always be thinking about such things—but then she admitted that when she sees long numerals she always checks them for divisibility by 9.

  • “Soupmaster” and “mousetraps”. The picture here is not perfect. I wanted a picture of the Soupmaster restaurant that was at the Liberty Place food court in Philadelphia, but I couldn't find one.

  • I also wanted to show the back end of a Honda Integra and a picture of granite, but I couldn't find a good picture of either one before I deleted them from the talk. (My wife also gets credit for noticing this one.) [ Addendum 20170515: On the road yesterday I was reminded of another one my wife noticed: “Pontiac” / “caption”. ]

Slide #1 defines what anagrams actually are, with an example of “soapstone” / “teaspoons”. I had originally thought I might pander to the left-wing sensibilities of the !‌!Con crowd by using the example “Donald Trump” / “Lord Dampnut” and even made the illustration. I eventually rejected this for a couple of reasons. First, it was misleading because I only intended to discuss single-word anagrams. Second, !‌!Con is supposed to be fun and who wants to hear about Donald Trump?

But the illustration might be useful for someone else, so here it is. Share and enjoy.

After I rejected this I spent some time putting together an alternative, depicting “I am Lord Voldemort” / “Tom Marvolo Riddle”. I am glad I went with the soapstone teaspoons instead.

People Magazine

Clearly one important ingredient in finding good anagrams is that they should have good semantics. I did not make much of an effort in this direction. But it did occur to me that if I found a list of names of well-known people I might get something amusing out of it. For example, it is well known that “Britney Spears” is an anagram of “Presbyterians” which may not be meaningful but at least provides something to mull over.

I had some trouble finding a list of names of well-known people, probably because i do not know where to look, but I did eventually find a list of a few hundred on the People Magazine web site so I threw it into the mix and was amply rewarded:

Cheryl Burke Huckleberry

I thought Cheryl Burke was sufficiently famous, sufficiently recently, that most people might have heard of her. (Even I know who she is!) But I gave a version of the !‌!Con talk to the Philadelphia Perl Mongers the following Monday and I was the only one in the room who knew. (That version of the talk took around 75 minutes, but we took a lot of time to stroll around and look at the scenery, much of which is in this article.)

I had a struggle finding the right Cheryl Burke picture for the !‌!Con talk. The usual image searches turned up lots of glamour and fashion pictures and swimsuit pictures. I wanted a picture of her actually dancing and for some reason this was not easy to find. The few I found showed her from the back, or were motion blurred. I was glad when I found the one above.


A few days before the !‌!Con talk my original anagram-scoring article hit #1 on Hacker News. Hacker News user Pxtl suggested using the Wikipedia article title list as an input lexicon. The article title list is available for download from the Wikimedia Foundation so you don't have to scrape the pages as Pxtl suggested. There are around 13 million titles and I found all the anagrams and scored them; this took around 25 minutes with my current code.

The results were not exactly disappointing, but neither did they deliver anything as awesomely successful as “cinematographer” / “megachiropteran”. The top scorer by far was “ACEEEFFGHHIILLMMNNOORRSSSTUV”, which is the pseudonym of 17th-century German writer Hans Jakob Christoffel von Grimmelshausen. Obviously, Grimmelshausen constructed his pseudonym by sorting the letters of his name into alphabetical order.

(Robert Hooke famously used the same scheme to claim priority for discovery of his spring law without actually revealing it. He published the statement as “ceiiinosssttuv” and then was able to claim, two years later, that this was an anagram of the actual law, which was “ut tensio, sic vis”. (“As the extension, so the force.”) An attendee of my Monday talk wondered if there is some other Latin phrase that Hooke could have claimed to have intended. Perhaps someone else can take the baton from me on this project.)

Anyway, the next few top scorers demonstrate several different problems:

    21 Abcdefghijklmnopqrstuvwxyz / Qwertyuiopasdfghjklzxcvbnm
    21 Abcdefghijklmnopqrstuvwxyz / Qwertzuiopasdfghjklyxcvbnm
    21 Ashland County Courthouse / Odontorhynchus aculeatus
    21 Daniel Francois Malherbe / Mindenhall Air Force Base

    20 Christine Amongin Aporu / Ethnic groups in Romania
    20 Message force multiplier / Petroleum fiscal regimes

    19 Cholesterol lowering agent / North West Regional College
    19 Louise de Maisonblanche / Schoenobius damienella
    19 Scorpaenodes littoralis / Steroidal spirolactones

The “Qwerty” ones are intrinsically uninteresting and anyway we could have predicted ahead of time that they would be there. And the others are just sort of flat. “Odontorhynchus aculeatus” has the usual problems. One can imagine that there could be some delicious irony in “Daniel Francois Malherbe” / “Mindenhall Air Force Base” but as far as I can tell there isn't any and neither was Louise de Maisonblanche killed by an S. damienella. (It's a moth. Mme de Maisonblanche was actually killed by Variola which is not an anagram of anything interesting.)

Wikipedia article titles include many trivial variations. For example, many people will misspell “Winona Ryder” as “Wynona Rider”, so Wikipedia has pages for both, with the real article at the correct spelling and the incorrect one redirecting to it. The anagram detector cheerfully picks these up although they do not get high scores. Similarly:

  • there are a lot of articles about weasels that have alternate titles about “weasles”
  • there are a lot of articles about the United States or the United Kingdom that have alternate titles about the “Untied States” or the “Untied Kingdom”
  • Articles about the “Center for” something or other with redirects to (or from) the “Centre for” the same thing.
  • There is an article about “Major professional sports leagues in Canada and the United States” with a redirect from “Major professional sports leagues in the United States and Canada”.
  • You get the idea.

The anagram scorer often had quite a bit of trouble with items like these because they are long and full of repeated letter pairs. The older algorithm would have done even worse. If you're still wondering about the difference between two exponential algorithms, some of these would make good example cases to consider.

As I mentioned above you can download the Wikipedia anagrams from my web site and check for yourself. My favorite item so far is:

    18 Atlantis Casino Resort Spa / Carter assassination plot


Some words appear with surprising frequency and I don't know why. As I mentioned above one of the top scorers was “Ethnic groups in Romania” and for some reason Romania appears in the anagram list over and over again:

    20 Christine Amongin Aporu / Ethnic groups in Romania
    17 List of Romanian actors / Social transformation
    15 Imperial Coronation  / Romanian riot police
    14 Rakhine Mountains / Romanians in the UK
    14 Mindanao rasbora / Romanians abroad
    13 Romanian poets / ramosopinnate
    13 Aleuron carinatum / Aromanian culture
    11 Resita Montana / Romanian state
    11 Monte Schiara / The Romaniacs
    11 Monetarianism / Romanian Times
    11 Marion Barnes / Romanian Serb
    11 Maarsen railway station / Romanian State Railways
    11 Eilema androconia / Nicolae de Romania
    11 Ana Maria Norbis / Arabs in Romania

    ( 170 more )

Also I had never thought of this before, but Romania appears in this unexpected context:

    09 Alicia Morton / Clitoromania
    09 Carinito Malo / Clitoromania

(Alicia Morton played Annie in the 1999 film. Carinito Malo is actually Cariñito Malo. I've already discussed the nonequivalence of “n” and “ñ” so I won't beat that horse again.)

Well, this is something I can investigate. For each string of letters, we have here the number of Wikipedia article titles in which the string appears (middle column), the number of anagram pairs in which the string appears (left column; anagrams with score less than 6 are not counted) and the quotient of the two (right column).

            romania               110  4106  2.7%
            serbia                109  4400  2.5%
            croatia                68  3882  1.8%
            belarus                24  1810  1.3%

            ireland               140 11426  1.2%
            andorra                 7   607  1.2%
            austria                60  5427  1.1%
            russia                137 15944  0.9%

            macedonia              28  3167  0.9%
            france                111 14785  0.8%
            spain                  64  8880  0.7%
            slovenia               18  2833  0.6%

            wales                  47  9438  0.5%
            portugal               17  3737  0.5%
            italy                  21  4353  0.5%
            denmark                19  3698  0.5%

            ukraine                12  2793  0.4%
            england                37  8719  0.4%
            sweden                 11  4233  0.3%
            scotland               16  4945  0.3%

            poland                 22  6400  0.3%
            montenegro              4  1446  0.3%
            germany                16  5733  0.3%
            finland                 6  2234  0.3%

            albania                10  3268  0.3%
            slovakia                3  1549  0.2%
            norway                  9  3619  0.2%
            greece                 10  8307  0.1%

            belgium                 3  2414  0.1%
            switzerland             0  5439  0.0%
            netherlands             1  3522  0.0%
            czechia                 0    75  0.0%

As we see, Romania and Serbia are substantially ahead of the others. I suspect that it is a combination of some lexical property (the interesting part) and the relatively low coverage of those countries in English Wikipedia. That is, I think if we were to identify the lexical component, we might well find that russia has more of it, but scores lower than romania because Russia is much more important. My apologies if I accidentally omitted your favorite European country.

[ Oh, crap, I just realized I left out Bosnia. ]


Another one of the better high scorers turns out to be the delightful:

   16 Lesbian intercourse / Sunrise Celebration

“Lesbian”, like “Romania”, seems to turn up over and over; the next few are:

    11 Lesbian erotica / Oreste Bilancia
    11 Pitane albicollis / Political lesbian
    12 Balearic islands / Radical lesbians
    12 Blaise reaction / Lesbian erotica

    (43 more)

Wikipedia says:

The Blaise reaction is an organic reaction that forms a β-ketoester from the reaction of zinc metal with a α-bromoester and a nitrile.

A hundred points to anyone who can make a genuinely funny joke out of this.

Oreste Bilancia is an Italian silent-film star, and Pitane albicollis is another moth. I did not know there were so many anagrammatic moths. Christian Bale is an anagram of Birthana cleis, yet another moth.

I ran the same sort of analysis on lesbian as on romania, except that since it wasn't clear what to compare it to, I picked a bunch of random words.

    nosehair                 3     3 100.0%
    margarine                4    16  25.0%
    penis                   95   573  16.6%
    weasel                  11   271   4.1%
    phallus                  5   128   3.9%
    lesbian                 26   863   3.0%
    center                 340 23969   1.4%
    flowers                 14  1038   1.3%
    trumpet                  6   487   1.2%
    potato                  10   941   1.1%
    octopus                  4   445   0.9%
    coffee                  12  1531   0.8%

It seems that lesbian appears with unusually high but not remarkably high frequency. The unusual part is its participation in so many anagrams with very high scores. The outstanding item here is penis. (The top two being rare outliers.) But penis still wins even if I throw away anagrams with scores less than 10 (instead of less than 6):

    margarine               1    16   6.2%
    penis                  13   573   2.3%
    lesbian                 8   863   0.9%
    trumpet                 2   487   0.4%
    flowers                 4  1038   0.4%
    center                 69 23969   0.3%
    potato                  2   941   0.2%
    octopus                 1   445   0.2%
    coffee                  1  1531   0.1%
    weasel                  0   271   0.0%
    phallus                 0   128   0.0%
    nosehair                0     3   0.0%

Since I'm sure you are wondering, here are the anagrams of margarine and nosehair:

    07 Nosehair / Rehsonia
    08 Aso Shrine / Nosehairs
    09 Nosehairs / hoariness

    04 Margaret Hines / The Margarines
    07 Magerrain / margarine
    07 Ramiengar / margarine
    08 Rae Ingram / margarine
    11 Erika Armstrong / Stork margarine

I think “Margaret Hines” / “The Margarines” should score more than 4, and that this exposes a defect in my method.

Acrididae graphs 

Here is the graph constructed by the MIS algorithm for the pair “acrididae” / “cidaridae”, which I discussed in an earlier article and also mentioned in my talk.

Each maximum independent set in this graph corresponds to a minimum-chunk mapping between “acrididae” and “cidaridae”. In the earlier article, I claimed:

This one has two maximum independent sets

which is wrong; it has three, yielding three different mappings with five chunks:

My daughter Katara points out that the graphs above resemble grasshoppers. My Gentle Readers will no doubt recall that acrididae is the family of grasshoppers, comprising around 10,000 species. I wanted to find an anagram “grasshopper” / “?????? graph”. There are many anagrams of “eoprs” and “eoprss” but I was not able to find anything good. The best I could do was “spore graphs”.

Thank you, Gentle Readers, for taking this journey with me. I hope nobody walks up to me in the next year to complain that my blog does not feature enough anagram-related material.

by Mark Dominus ( at May 11, 2017 05:26 PM


Haskell development jobs with Well-Typed

tl;dr If you’d like a job with us, send your application as soon as possible.

We are looking for several (probably two) Haskell experts to join our team at Well-Typed. This is a great opportunity for someone who is passionate about Haskell and who is keen to improve and promote Haskell in a professional context.

About Well-Typed

We are a team of top notch Haskell experts. Founded in 2008, we were the first company dedicated to promoting the mainstream commercial use of Haskell. To achieve this aim, we help companies that are using or moving to Haskell by providing a range of services including consulting, development, training, and support and improvement of the Haskell development tools. We work with a wide range of clients, from tiny startups to well-known multinationals. We have established a track record of technical excellence and satisfied customers.

Our company has a strong engineering culture. All our managers and decision makers are themselves Haskell developers. Most of us have an academic background and we are not afraid to apply proper computer science to customers’ problems, particularly the fruits of FP and PL research.

We are a self-funded company so we are not beholden to external investors and can concentrate on the interests of our clients, our staff and the Haskell community.

About the jobs

Generally, the roles are not tied to a single specific project or task, and allow remote work. However, we are also looking for someone to work on a specific project with one of our clients, and that requires work on-site in London.

Please indicate in your application whether on-site work in London is an option for you.

In general, work for Well-Typed could cover any of the projects and activities that we are involved in as a company. The work may involve:

  • working on GHC, libraries and tools;

  • Haskell application development;

  • working directly with clients to solve their problems;

  • teaching Haskell and developing training materials.

We try wherever possible to arrange tasks within our team to suit peoples’ preferences and to rotate to provide variety and interest.

Well-Typed has a variety of clients. For some we do proprietary Haskell development and consulting. For others, much of the work involves open-source development and cooperating with the rest of the Haskell community: the commercial, open-source and academic users.

Our ideal candidate has excellent knowledge of Haskell, whether from industry, academia or personal interest. Familiarity with other languages, low-level programming and good software engineering practices are also useful. Good organisation and ability to manage your own time and reliably meet deadlines is important. You should also have good communication skills.

You are likely to have a bachelor’s degree or higher in computer science or a related field, although this isn’t a requirement.

Further (optional) bonus skills:

  • experience in teaching Haskell or other technical topics,

  • experience of consulting or running a business,

  • knowledge of and experience in applying formal methods,

  • familiarity with (E)DSL design,

  • knowledge of concurrency and/or systems programming,

  • experience with working on GHC,

  • experience with web programming (in particular front-end),

  • … (you tell us!)

Offer details

The offer is initially for one year full time, with the intention of a long term arrangement. For the remote role(s), living in England is not required. For the on-site role, you have to be allowed to work in England. We may be able to offer either employment or sub-contracting, depending on the jurisdiction in which you live.

If you are interested, please apply via Tell us why you are interested and why you would be a good fit for Well-Typed, and attach your CV. Please indicate whether the on-site work in London is an option for you. Please also indicate how soon you might be able to start.

We are more than happy to answer informal enquiries. Contact Duncan Coutts (, dcoutts on IRC), Adam Gundry (, agundry on IRC) or Andres Löh (, kosmikus on IRC) for further information.

We will consider applications as soon as we receive them, and will try to fill the positions as soon as possible. In any case, please try to get your application to us by 8 June 2017.

by andres, duncan, adam at May 11, 2017 01:56 PM

May 10, 2017

Douglas M. Auclair (geophf)

April 2017 1HaskellADay 1Liners

  • April 14th, 2017: given
    eitherOr, neitherNor :: Eq a => a -> a -> a -> Bool

    Is eitherOr not neitherNor?

    Prove or disprove.
  • April 14th, 2017: given
    neitherNor :: Eq a => a -> a -> a -> Bool
    andNot :: Eq a => a -> a -> Bool

    How do you compose neitherNor 1 0 and andNot 4?
  • April 11th, 2017:

    opts :: Credentials -> Options
    opts c = defaults & auth ?~ basicAuth (pack $ keyToken c) (pack $ secretToken c)



    data Credentials = Credentials { keyToken, secretToken :: String }

    and (?~) and (&) are from Control.Lens

    Snaps for elegance

    The above code from quillio/Twillo.hs by ismailmustafa

by geophf ( at May 10, 2017 06:44 PM

May 08, 2017

Mark Jason Dominus

An anagrammatic cautionary tale

I previously claimed that “cinematographer” / “megachiropteran” was the best anagram in English. Scoring all the anagrams in the list of 13 million Wikipedia article titles did not refute this, but it did reveal that “cinematographer” is also an anagram of “Taichang Emperor”.

The Taichang Emperor (泰昌) lived from 1582 to 1620 and was the 14th emperor of the Ming Dynasty. His reign as emperor lasted only 29 days, after which he died of severe diarrhea. Wikipedia says:

According to non-official primary sources, the Taichang Emperor's illness was brought about by excessive sexual indulgence after he was presented with eight maidens by Lady Zheng.

To counteract the diarrhea, the emperor took a “red pill” offered to him by a court official:

It was recorded in official Ming histories that the Taichang Emperor felt much better after taking the red pill, regained his appetite and repeatedly praised Li Kezhuo as a "loyal subject". That same afternoon, the emperor took a second pill and was found dead the next morning.

Surely this tale of Ming China has something to teach us even today.

by Mark Dominus ( at May 08, 2017 12:25 PM

May 07, 2017

Neil Mitchell

Proving stuff with Idris

Summary: I've been learning Idris to play around with writing simple proofs. It seems pretty cool.

The Idris programming language is a lot like Haskell, but with quite a few cleanups (better export syntax, more though out type classes), and also dependent types. I'm not a massive fan of dependent types as commonly presented - I want to write my code so it's easy to prove, not intertwine my beautiful code with lots of invariants. To try out Idris I've been proving some lemmas about list functions. I'm very much an Idris beginner, but thought I would share what I've done so far, partly to teach, partly to remember, and party to get feedback/criticism about all the beginner mistakes I've made.

Before proving stuff, you need to write some definitions. Idris comes with an append function (named ++ as you might expect), but to keep everything simple and out in the open I've defined:

append : List a -> List a -> List a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

Coming from Haskell the only real difference is that cons is :: and types are :. Given how Haskell code now looks, that's probably the right way around anyway. We can load that code in the Idris interactive environment and run it:

$ idris Main.idr
Main> append [1,2] [3]
[1,2,3] : List Integer

What we can also do, but can't easily do in Haskell, is start proving lemmas about it. We'd like to prove that append xs [] = xs, so we write a proof:

proof_append_nil : (xs : List a) -> append xs [] = xs
proof_append_nil xs = ?todo

We name the proof proof_append_nil and then say that given xs (of type List a) we can prove that append xs [] = xs. That's pretty direct and simple. Now we have to write the proof - we first write out the definition leaving ?todo where we want the proof to go. Now we can load the proof in Idris and type :t todo to get the bit of the proof that is required, and Idris says:

todo : append xs [] = xs

That's fair - we haven't proven anything yet. Since we know the proof will proceed by splitting apart the xs we can rewrite as:

proof_append_nil [] = ?todo_nil
proof_append_nil (x :: xs) = ?todo_cons

We can now ask for the types of the two remaining todo bits:

todo_nil : [] = []
todo_cons : x :: append xs [] = x :: xs

The first todo_nil is obviously true since the things on either side of the equality match, so we can replace it with Refl. The second statement looks like the inductive case, so we want to apply proof_append_nil to it. We can do that with rewrite proof_append_nil xs, which expands to append xs [] = xs, and rewrites the left-hand-side of the proof to be more like the right. Refined, we end up with:

proof_append_nil [] = Refl
proof_append_nil (x :: xs) = rewrite proof_append_nil xs in ?todo_cons

Reloading again and asking for the type of todo_cons we get:

todo_cons : x :: xs = x :: xs

These things are equal, so we replace todo_cons with Refl to get a complete proof of:

proof_append_nil : (xs : List a) -> append xs [] = xs
proof_append_nil [] = Refl
proof_append_nil (x :: xs) = rewrite proof_append_nil xs in Refl

Totality Checking

Proofs are only proofs if you have code that terminates. In Idris, seemingly sprinkling the statement:

%default total

At the top of the file turns on the totality checker, which ensures the proof is really true. With the statement turned on I don't get any warnings about totality issues, so we have proved append really does have [] as a right-identity.

Avoiding rewrite

The rewrite keyword seems like a very big hammer, and in our case we know exactly where we want to apply the rewrite. Namely at the end. In this case we could have equally written:

cong (proof_append_nil xs)

Not sure which would be generally preferred style in the Idris world, but as the proofs get more complex using rewrite certainly seems easier.

Differences from Haskell

Coming from a Haskell background, and sticking to simple things, the main differences in Idris were that modules don't have export lists (yay), lists are :: and types are : (yay), functions can only use functions defined before them (sad, but I guess a restriction to make dependent types work) and case/lambda both use => instead of -> (meh).

Next steps

For my first task in Idris I also defined two reverse functions:

reverse1 : List a -> List a
reverse1 [] = []
reverse1 (x :: xs) = reverse1 xs `append` [x]

rev2 : List a -> List a -> List a
rev2 acc [] = acc
rev2 acc (x :: xs) = rev2 (x :: acc) xs

reverse2 : List a -> List a
reverse2 = rev2 []

The first reverse1 function is reverse in O(n^2), the second is reverse in O(n). I then tried to prove the three lemmas:

proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs

Namely that both reverse1 and reverse2 are self inverses, and then that they are equivalent. To prove these functions required a few helper lemmas, but only one additional Idris function/feature, namely:

sym : (left = right) -> right = left

A function which transforms a proof of equality from one way around to the other way around. I also required a bunch of helper lemmas, including:

proof_append_assoc : (xs : List a) -> (ys : List a) -> (zs : List a) -> append xs (append ys zs) = append (append xs ys) zs

Developing these proofs in Idris took me about ~2 hours, so were a nice introductory exercise (with the caveat that I've proven these lemmas before, although not in 4+ years). I'd invite anyone interested in learning this aspect of Idris to have a go, and I'll post my proofs sometime in the coming week.

Update: additional notes on this material can be found here from Reddit user chshersh.

by Neil Mitchell ( at May 07, 2017 08:35 PM

Michael Snoyman

The Worst Function in Conduit

This blog post addresses a long-standing FIXME in the conduit-combinators documentation, as well as a question on Twitter. This blog post will assume familiarity with the Conduit streaming data library; if you'd like to read up on it first, please check out the tutorial. The full executable snippet is at the end of this blog post, but we'll build up intermediate bits along the way. First, the Stack script header, import statement, and some minor helper functions.

#!/usr/bin/env stack
--stack --resolver lts-8.12 script
import Conduit

src10 :: Monad m => ConduitM i Int m ()
src10 = yieldMany [1..10]

remaining :: MonadIO m => ConduitM i o m ()
remaining = lengthC >>= \x -> liftIO (putStrLn ("Remaining: " ++ show x))

src10 just provides the numbers 1 through 10 as a source, and remaining tells you how many values are remaining from upstream. Cool.

Now let's pretend that the Conduit libraries completely forgot to provide a drop function. That is, a function that will take an Int and discard that many values from the upstream. We could write one ourselves pretty easily:

dropSink :: Monad m => Int -> ConduitM i o m ()
dropSink cnt
  | cnt <= 0 = return ()
  | otherwise = await >> dropSink (cnt - 1)

(Bonus points to readers: this function is inefficient in the case that upstream has less than cnt values, optimize it.)

This function will drop a certain number of elements from upstream, so the next component we monadically bind with can pick it up. Let's see how that looks:

goodDropSink :: IO ()
goodDropSink = runConduit
             $ src10
            .| (dropSink 5 >> remaining)

All well and good. But notice two things:

  • I called this dropSink. Why sink?
  • I stressed that we had to monadically bind. Why?

Well, there's another formulation of this drop function. Instead of letting the next monadically bound component pick up remaining values, we could pass the remaining values downstream. Fortunately it's really easy to implement this function in terms of dropSink:

dropTrans :: Monad m => Int -> ConduitM i i m ()
dropTrans cnt = dropSink cnt >> mapC id

(For more meaningless bonus points, feel free to implement this without dropSink, or for a greater challenge, implement dropSink in terms of dropTrans.) Anyway, this function can be used easily as:

goodDropTrans :: IO ()
goodDropTrans = runConduit
              $ src10
             .| dropTrans 5
             .| remaining

Many may argue that this is more natural. To some extent, it mirrors the behavior of take more closely, as take passes the initial values downstream. On the other hand, dropTrans cannot guarantee that the values will be removed from the stream; if instead of dropTrans 5 .| remaining I simply did dropTrans 5 .| return (), then the dropTrans would never have a chance to fire, since execution is driven from downstream. Also, as demonstrated, it's really easy to capture this transformer behavior from the sink behavior; the other way is trickier.

My point here is that we have two legitimate definitions of a function. And from my experience, different people expect different behavior for the function. In fact, some people (myself included) intuitively expect different behavior depending on the circumstance! This is what earns drop the title of worst function in conduit.

To make it even more clear how bad this is, let's see how you can misuse these functions unintentionally.

badDropSink :: IO ()
badDropSink = runConduit
            $ src10
           .| dropSink 5
           .| remaining

This code looks perfectly reasonable, and if we just replaced dropSink with dropTrans, it would be correct. But instead of saying, as expected, that we have 5 values remaining, this will print 0. The reason: src10 yields 10 values to dropSink. dropSink drops 5 of those and leaves the remaining 5 untouched. But dropSink never itself yields a value downstream, so remaining receives nothing.

Because of the type system, it's slightly trickier to misuse dropTrans. Let's first do the naive thing of just assuming it's dropSink:

badDropTrans :: IO ()
badDropTrans = runConduit
             $ src10
            .| (dropTrans 5 >> remaining)

GHC does not like this one bit:

    • Couldn't match type ‘Int’ with ‘Data.Void.Void’
      Expected type: ConduitM () Data.Void.Void IO ()
        Actual type: ConduitM () Int IO ()

The problem is that runConduit expects a pipeline where the final output value is Void. However, dropTrans has an output value of type Int. And if it's yielding Ints, so must remaining. This is definitely an argument in favor of dropTrans being the better function: the type system helps us a bit. (It's also an argument in favor of keeping the type signature of runConduit as-is.)

However, it's still possible to accidentally screw things up in bigger pipelines, e.g.:

badDropTrans :: IO ()
badDropTrans = runConduit
             $ src10
            .| (dropTrans 5 >> remaining)
            .| (sinkList >>= liftIO . print)

This code may look a bit contrived, but in real-world Conduit code it's not at all uncommon to deeply nest these components in such a way that the error would not be present. You may be surprised to hear that the output of this program is:

Remaining: 0

The reason is that the sinkList is downstream from dropTrans, and grabs all of its output. dropTrans itself will drain all output from src10, leaving nothing behind for remaining to grab.

The Conduit libraries use the dropSink variety of function. I wish there was a better approach here that felt more intuitive to everyone. The closest I can think of to that is deprecating drop and replacing it with more explicitly named dropSink and dropTrans, but I'm not sure how I feel about that (feedback welcome, and other ideas certainly welcome).

Full code

#!/usr/bin/env stack
--stack --resolver lts-8.12 script
import Conduit

dropSink :: Monad m => Int -> ConduitM i o m ()
dropSink cnt
  | cnt <= 0 = return ()
  | otherwise = await >> dropSink (cnt - 1)

dropTrans :: Monad m => Int -> ConduitM i i m ()
dropTrans cnt = dropSink cnt >> mapC id

src10 :: Monad m => ConduitM i Int m ()
src10 = yieldMany [1..10]

remaining :: MonadIO m => ConduitM i o m ()
remaining = lengthC >>= \x -> liftIO (putStrLn ("Remaining: " ++ show x))

goodDropSink :: IO ()
goodDropSink = runConduit
             $ src10
            .| (dropSink 5 >> remaining)

badDropSink :: IO ()
badDropSink = runConduit
            $ src10
           .| dropSink 5
           .| remaining

goodDropTrans :: IO ()
goodDropTrans = runConduit
              $ src10
             .| dropTrans 5
             .| remaining

badDropTrans :: IO ()
badDropTrans = runConduit
             $ src10
            .| (dropTrans 5 >> remaining)
            .| (sinkList >>= liftIO . print)

main :: IO ()
main = do
  putStrLn "Good drop sink"
  putStrLn "Bad drop sink"
  putStrLn "Good drop trans"
  putStrLn "Bad drop trans"

Full output

Good drop sink
Remaining: 5
Bad drop sink
Remaining: 0
Good drop trans
Remaining: 5
Bad drop trans
Remaining: 0

May 07, 2017 05:10 AM

Robert Harper

A “proof by contradiction” is not a proof that ends with a contradiction

It is well-known that constructivists renounce “proof by contradiction”, and that classicists scoff at the critique.  “Those constructivists,” the criticism goes, “want to rule out proofs by contradiction.  How absurd!  Look, Pythagoras showed that the square root of two is irrational by deriving a contradiction from the assumption that it is rational.  There is nothing wrong with this.  Ignore them!”

On examination that sort of critique fails, because a proof by contradiction is not a proof that derives a contradiction.  Pythagoras’s  proof is valid, one of the eternal gems of mathematics.  No one questions the validity of that argument, even if they question proof by contradiction. 

Pythagoras’s Theorem expresses a negation: it is not the case that the square root of two can be expressed as the ratio of two integers.  Assume that it can be so represented.  A quick deduction shows that this is impossible.  So the assumption is false.  Done.  This is a direct proof of a negative assertion; it is not a “proof by contradiction”.

What, then, is a proof by contradiction?  It is the affirmation of a positive statement by refutation of its denial.  It is a direct proof of the negation of a negative assertion that is then pressed into service as a direct proof of the assertion, which it is not.  Anyone is free to ignore the distinction for the sake of convenience, as a philosophical issue, or as a sly use of “goto” in a proof, but the distinction nevertheless exists and is important.  Indeed, part of the beauty of constructive mathematics is that one can draw such distinctions, for, once drawn, one can selectively disregard them.  Once blurred, forever blurred, a pure loss of expressiveness.

For the sake of explanation, let me rehearse a standard example of a proof by contradiction.  The claim is that there exists irrationals a and b such that a to the b power is rational.  Here is an indirect proof, a true proof by contradiction.  Move number one, let us prove instead that it is impossible that any two irrationals a and b are such that a to the b is irrational.  This is a negative statement, so of course one proves it be deriving a contradiction from assuming it. But it is not the original statement!  This will be clear from examining the information content of the proof.

Suppose, for a contradiction, that every two irrationals a and b are such that a to the b power is irrational.  We know from Pythagoras that root two is irrational, so plug it in for both a and b, and conclude that root two to the root two power is irrational.  Now use the assumption again, taking a to be root two to the root two, and b to be root two.  Calculate a to the power of b, it is two, which is eminently rational.  Contradiction.

We have now proved that it is not the case that every pair of irrationals, when exponentiated, give an irrational.  There is nothing questionable about this proof as far as I am aware.  But it does not prove that there are two irrationals whose exponent is rational!  If you think it does, then I ask you, please name them for me.  That information is not in this proof (there are other proofs that do name them, but that is not relevant for my purposes).  You may, if you wish, disregard the distinction I am drawing, that is your prerogative, and neither I nor anyone has any problem with that.  But you cannot claim that it is a direct proof, it is rather an indirect proof, that proceeds by refuting the negative of the intended assertion.

So why am I writing this?  Because I have learned, to my dismay, that in U.S. computer science departments–of all places!–students are being taught, erroneously, that any proof that derives a contradiction is a “proof by contradiction”.  It is not.  Any proof of a negative must proceed by contradiction.  A proof by contradiction in the long-established sense of the term is, contrarily, an indirect proof of a positive by refutation of the negative.  This distinction is important, even if you want to “mod out” by it in your work, for it is only by drawing the distinction that one can even define the equivalence with which to quotient.

That’s my main point.  But for those who may not be familiar with the distinction between direct and indirect proof, let me take the opportunity to comment on why one might care to draw such a distinction.  It is entirely a matter of intellectual honesty: the information content of the foregoing indirect proof does not fulfill the expectation stated in the theorem.  It is a kind of boast, an overstatement, to claim otherwise.  Compare the original statement with the reformulation used in the proof.  The claim that it is not the case that every pair of irrationals exponentiate to an irrational is uncontroversial.  The proof proves it directly, and there is nothing particularly surprising about it.  One would even wonder why anyone would bother to state it.  Yet the supposedly equivalent claim stated at the outset appears much more fascinating, because most people cannot easily think up an example of two irrationals that exponentiate to rationals.  Nor does the proof provide one. Once, when shown the indirect proof, a student of mine blurted out “oh that’s so cheap.”  Precisely.

Why should you care?  Maybe you don’t, but there are nice benefits to keeping the distinction, because it demarcates the boundary between constructive proofs, which have direct interpretation as functional programs, and classical proofs, which have only an indirect such interpretation (using continuations, to be precise, and giving up canonicity).  Speaking as a computer scientist, this distinction matters, and it’s not costly to maintain.  May I ask that you adhere to it?

Edit: rewrote final paragraph, sketchy and irrelevant, and improved prose throughout. 


Filed under: Programming, Research, Teaching

by Robert Harper at May 07, 2017 02:31 AM

May 05, 2017

Joachim Breitner

Farewall green cap

For the last two years, I was known among swing dancers for my green flat cap:

Monti, a better model than me

Monti, a better model than me

This cap was very special: It was a gift from a good friend who sewed it by hand from what used to be a table cloth of my deceased granny, and it has traveled with me to many corners of the world.

Just like last week, when I was in Paris where I attended the Charleston class of Romuald and Laura on Saturday (April 29). The following Tuesday I went to a Swing Social and wanted to put on the hat, and noticed that it was gone. The next day I bugged the manager and the caretaker of the venue of the class (Salles Sainte-Roche), and it seems that the hat was still there, that morning, im Salle Kurtz1, but when I went there it was gone.

And that is sad.

The last picture with the hat

The last picture with the hat

  1. How fitting, given that my granny’s maiden name is Kurz.

by Joachim Breitner ( at May 05, 2017 10:13 PM

May 04, 2017

Roman Cheplyaka

Please help me with these open source Haskell projects

Here are some pull requests and issues that have been awaiting my attention for months or years.

Sadly, I haven’t found and probably won’t find enough time for them. So I am asking you for help.

If you can work on and close at least one of the items below, that would be awesome.

Thanks to people who have helped so far:

  • Alexey Zabelin @alexeyzab — immortal: add wait

Pull requests awaiting reviews

These are pull requests submitted to my projects. For each one, I describe what needs to be done.

ansi-terminal: add save, restore, report cursor

Needs a review and testing on different platforms.

ansi-terminal: compatibility with Win32- and above

Needs review and testing.

tasty: build with GHCJS

This one actually has little to do with tasty or ghcjs; it only needs a PR for the clock package to fall back to time.

tasty: make --quickcheck-show-replay always show the seed (not just on failure)

Need to figure out how to fix this without going back to random (see this comment).

temporary: canonicalized versions of withSystemTempDirectory and withTempDirectory

Needs another pair of eyes — especially regarding the mysterious withCanonicalizedSystemTempDirectory.

tasty: add soft timeouts

When a QuickCheck test runs into a timeout, Tasty does not report the input values generated by QuickCheck for the interrupted run.

This PR is probably affected by this change in exception handling — you’ll need to figure out how exactly and update the pull request appropriately.

immortal: add wait

Done on 2017-05-07 by Alexey Zabelin

For graceful shutdown, I wait for threads to finish in my servers main loop. I would like to do the same with Immortal threads.

What needs to be done:

  1. Rebase
  2. Add a test

tasty-golden: add golden test for text files

I think the point of this PR is to add an internal diff implementation, but I am not sure.

If you understand and like the idea, please update the PR and make a new case for it; otherwise I’ll probably close it.

tasty: Silence a few GHC warnings

Needs rebase and review.

Issues that need to be fixed

Here are a couple of issues that I care about and was going to fix myself, but can’t find the time.

stack: no package names in haddock index

xmonad: notifications pop up on top of xscreensaver

May 04, 2017 08:00 PM

May 03, 2017

Christopher Allen

What a Haskell Study Group is Not

This article is by Steven Syrek. I’m reposting it here because I endorse what he’s saying. I believe Steven brings a valuable perspective on the haskell book, reading groups, and education in general.

Steven posted this article on his Medium.

He has also written some extended notes on pedagogy tied to this post here.

The most rewarding thing about learning Haskell is the feeling that you are making real progress toward understanding not just the syntax of a programming language but a way of solving problems that is more universal than the domain of software development. The most rewarding thing about teaching Haskell is watching others make this same progress. The most frustrating thing about both learning and teaching Haskell is the widespread attitude that functional programming in general, or Haskell specifically, is difficult.

The goal of any teacher should be to expel this myth. The Haskell community is too small to support much formal education and those most apt to teach have precious little time to do so. And so the myth persists, and many people who could or would learn Haskell do not, whether out of fear, misprision, or lack of communal encouragement. Independent study groups, however, can meet the needs of language learners just as well, but only if they are committed at the outset to pragmatic goals and maintain a culture of mutual support and accountability.

Over the course of about eight months, from September 2016 to April 2017, I ran a Haskell study group in New York City based on Chris Allen and Julie Moronuki’s book, Haskell Programming from First Principles. Since this book was designed to provide a curriculum, it was ideally suited to our purposes. We covered one chapter a week, more or less, as there is just enough content per chapter to keep a dedicated group humming along: challenged but not overwhelmed.

In this article, I will share my thoughts on what made our group successful, where we went astray, and in particular on what a Haskell study group should not be—as the pitfalls are many but advice for avoiding them, based on actual experience, scant. My own background happens to be in education, which has no doubt informed my observations, but I was just as much a student in this study group, even if I happened to be its organizer. I hope this dual role has given me insight from both sides of the pedagogical divide that will be useful to others thinking about starting their own Haskell study groups, a course of action I highly recommend.

1. A Haskell study group is not meant to serve any purpose other than helping people learn Haskell.

Keep this mantra in mind: the point of a Haskell study group is to help people learn Haskell. Nothing else matters. Refer to this mantra whenever you’re in doubt about anything else.

2. A Haskell study group is not a place for people to learn about monads.

Or any other specific language feature. Do not let the random people who will inevitably show up derail your meetings with general, off-topic questions. Make a schedule, post it publicly, and stick to it. Once you embark on diversions, you may never get back on track. Respect the time, commitment, and ongoing progress of your regulars and let newcomers catch up on their own. Always assume anyone who comes to a meeting has: 1) read the chapter for that week, 2) typed in all the code in the chapter and, separately, 3) attempted to complete all the exercises in the chapter. Avoid spending too much time on topics everyone should already know or any time at all on questions about the language from Meetup shoppers.

3. A Haskell study group should not reinforce mistaken or unhelpful stereotypes about Haskell.

Many people have had a hard time learning Haskell. This has given the language a reputation for being hard to learn. In reality, Haskell is elegant and far easier to learn than many other, less elegant languages. The dearth of teaching materials and low quality of documentation have made it difficult for entrants to gain a foothold in the community as compared to language communities that go out of their way to be approachable to newcomers. The Haskell Book directly addresses this problem, however, and it does no one any good to credit assumptions that Haskell requires you to be a math genius. Haskell is capable of representing extremely abstract mathematical entities, but so is math itself, and you hardly need to understand linear algebra to balance your checkbook. I’ve been a college writing instructor for over a decade. Writing is hard. Teaching writing is hard. But anyone can become a proficient writer, even if few will ever write literary masterpieces. We can respect the challenge without succumbing to it or using it as an excuse. Practice, and you’ll improve. Complain, and you’ll remain mediocre. Focus on the positives and the cumulative effect of breakthroughs in the Haskell learning experience.

4. A Haskell study group is not a language advocacy committee.

Given Haskell’s rather esoteric reputation in the world of professional developers, you are likely to be issued demands to defend Haskell’s general usefulness, the practical utility of certain concepts, or the viability of functional programming as a whole. Don’t do it. People have Google if they want to research such things and the entire rest of the Internet if they want to bring their spoons to a knife fight. Your group exists to teach people how to code, not to teach developers how to do their jobs. Focus on the people. Ignore the trolls, don’t use facile comparisons to OOP to explain anything, and don’t waste your energy trying to convince the skeptical. Actually, examples of what you can do in Haskell won’t necessarily help your cause, because most programming languages can do anything any other language can do. The power of Haskell isn’t in any one abstraction. It’s in leveraging all of them together to build software, and software is complex, composed of many interlocking parts. You aren’t likely to persuade by showing someone “the amazing things you can do with Functor” or what have you. Ultimately, they will have to find out for themselves.

5. A Haskell study group is not an experiment in deliberative democracy.

A successful study group requires leadership. Leadership means that someone has to be in charge. Someone has to find space for the meetings, plan them, show up to all of them on time, be responsible for any contingencies that arise, and enforce norms of behavior. If there is no point person, it is unlikely that the group as a whole will make much progress. Sometimes, leaders emerge organically, but it’s better for someone to volunteer to be the organizer in advance. Natural leaders can serve a useful purpose, but they can also be destructive if they aren’t reliable, grow resentful at having assumed a role they didn’t sign up for, or turn your study group into a cult of personality instead of a collaborative learning environment. It’s also essential for the organizer to have buy-in from the rest of the group. On the one hand, participants should appreciate the amount of work it takes to put a study group together and keep it together. On the other hand, an effective leader makes decisions without turning every possible choice into a referendum. Democracy is a fine thing, but in this situation, it is more likely to result in anarchy and listlessness than efficient and decisive action. Respect for the organizer(s) is also relevant to the next point:

6. A Haskell study group should not turn anyone into a martyr.

Whoever is running your group, it’s a good idea if the person in charge is a fellow learner. Someone already proficient in Haskell will need to be especially motivated to teach others to stick with a study group for beginners. Another beginner, however, will have intrinsic motivation. In fact, the organizer will have an even stronger incentive to keep up with the work. Beware any situation in which a single person has assumed all of the responsibility but has little incentive to continue participating or is otherwise crushed by the demands of a dysfunctional group culture—it’s not sustainable.

7. A Haskell study group is not a traditional classroom.

While it is advantageous for the organizer to have prior teaching experience, it is not essential. Since such experience is in short supply, most groups will have to go with what and whom they have. That means the culture of the group is even more important, because people who don’t know how to teach should probably not try to do it. Go over exercises, break into pairs or smaller groups if necessary, but avoid devoting too much of any given meeting to lectures or presentations. Talking is no substitute for coding.

8. A Haskell study group is not a hackathon.

That is, it shouldn’t be a freeform, come-and-do-as-you-please affair. Adhere to a long term curriculum, keep individual meetings structured, and enforce norms of accountability. People who drift in and out or consistently show up unprepared are only going to drain energy from the room. Shower those who participate in good faith with praise and attention. Marginalize those who only come for Haskell social hour or for the free food and drinks. Speaking of which:

9. A Haskell study group is not a Meetup.

Go ahead and use Meetup to schedule your meetings. I did. But don’t give people the impression that it’s one of those Meetups where you can show up to eat pizza, drink beer, and contribute nothing. Likewise:

10. A Haskell study group is not a tech talk.

Your study group is not a form of entertainment. Don’t just give talks or show slides. Some of that may be an inducement to attend, but you want students, not audience members. Your best bet is to plug in to a projector, display the REPL side-by-side with the PDF of the book, and code. You can do pairing, mobbing, taking turns on the exercises, or whatever other method you desire as long as you’re coding and everyone else has the chance to code right along with you. Live coding can be scary, so make it an exercise in solidarity. If everyone did their homework, then everyone should have something to contribute. I suggest you ask them to close their computers and have them do the exercises again, on the spot, for reinforcement. You’ll probably find that everyone ends up loving that in spite of themselves. And failures along the way are fine. In fact, the type checker invites “failure-driven development.” Work things out together. Learn to love the REPL together. Encourage hands-on work, and figure out as a group how to leverage error messages to produce provably correct code.

11. Haskell study group meetings should not go on forever.

People are busy. If you get anyone to dedicate an hour a week to attending a Haskell meeting, it’s a miracle. Don’t ask for too much, or you’re just going to discourage people who would otherwise like to come. As with learning anything, most of the work of learning Haskell people have to do on their own. The study group can provide motivation and moral support (and asynchronous assistance if you use Slack or something similar), but the meetings themselves shouldn’t be longer than an hour or two. Use them to catch up, go over as many of the exercises as possible, and answer questions relevant to that week’s chapter assignment. The book provides a curriculum, and it’s best to just follow it. There is no need to diverge into advanced language features or demonstrate practical applications of every concept. Keep it short, and keep it simple. Also, you don’t have to make sure everyone completely understands everything. Give people time to figure things out, and help them do so however you can, but if it takes too long, move on. You can always work with people one-on-one if they get stuck somewhere.

12. Haskell study groups themselves should not go on forever.

Choose a realistic goal for your study group. Covering chapters 1 to 18 is a realistic goal, at least to start. That will get you through monads (the denouement for many students), at which point you can decide how to proceed with the more advanced material. Some will have had enough, while others will be ready to learn independently. At any rate, don’t give people the impression that they’ll be visiting your co-working cubicle farm every week for the rest of their lives.

13. A Haskell study group is not group therapy.

Remember the point of a Haskell study group? It isn’t to make people feel good about themselves or give them a place to go at night. It’s to teach people Haskell. You don’t need to be an intimidating jerk, but you aren’t doing anyone who attends any favors by not prodding them at least a little bit. If group members come prepared, they should be able to participate in group discussion of the exercises. You can organize smaller groups if some members are truly shrinking violets, but I don’t recommend letting people off the hook just because they’re reluctant to speak up. Create a supportive environment, and there’s no reason for anyone to be terrified of contributing. You never know when an otherwise shy person may be withholding a valuable insight just for being reluctant to be the center of attention. Moreover, you may never know when one such person’s confusion about a concept is shared by others, just because no one wants to admit it. Seek out opportunities for productive conversations. Don’t let people be dominating or rude, but also don’t let them be window dressing. Both attitudes are often just forms of pride, and you need to break through that to reach the vulnerable, yearning students within. Likewise, don’t be afraid to ask people to leave if their attitude or behavior is causing problems or their lack of preparedness makes their ongoing participation pointless and a negative example for others.

14. A Haskell study group is not a race.

Do not skip material in the book, and do not try to cover too much at once. A chapter a week, more or less, should be the pace you adopt. Any faster is overwhelming. Any slower is boring and ineffective. Some chapters are long enough to warrant coverage over multiple weeks, but that should be a rarity. And precious few chapters (certainly not chapter 1) are skippable. Set a reasonable pace, and trust the curriculum. Don’t feel the need to move quickly or to slow down, even if some people ask for it. I repeat, most of the work they do, they should do at home. The meetings are for review, as much as you can reasonably do, and not to serve the needs of any one student. Also, don’t skip the chapter on QuickCheck, and don’t let anyone skip writing all those quickBatch tests. We know who you are.

15. A Haskell study group is not a competition.

Programmers often have strong, competitive personalities. Do your best to contain that. Even better, turn it to useful ends: make the game about helping others, not being smarter or further along in the book. Encourage more experienced students to help less experienced students, in pairs if necessary, so the value of collective progress is enhanced and “being in charge, because I’m the best” diminished. That said, a competitive spirit can be motivating as long as it isn’t toxic. Whatever keeps people showing up without discouraging others—it’s often a fine balance.

16. A Haskell study group should not encourage or facilitate cheating.

Implore group members to at least try the exercises for themselves and avoid looking for solutions online. Insist that they do not post solutions publicly themselves. On a related note, make sure they buy the book. The authors worked hard on it, of course, but most people will value something more highly if they have paid for it. You’ll want your group to have that feeling of “buy-in” however you can get it.

17. A Haskell study group should not let its culture develop spontaneously.

The culture of any group of people has at least as much to do with how that group behaves and what it considers acceptable, en masse, than its laws. And culture has inertia. If the culture of your study group is misaligned with the goal of learning Haskell, you will have a hard time changing it. Therefore, establish and reinforce your group’s culture from the outset. Be serious about the responsibilities of its members and that it’s not OK to show up unprepared. Think about creating the proper incentives for productive behavior, and avoid giving in to a culture of impunity. Over time, as the group becomes habituated to doing things the right way, you won’t need to be an enforcer as much. On the other hand, a culture that has gone astray will not easily be corrected with new rules, because by that point, leadership will no longer have the credibility to overrule custom: consuetudo pro lege servatur.

18. A Haskell study group does not need anything other than Haskell in order to teach people Haskell.

Use the tools provided by the language to teach the language: the REPL, the type checker, handy compiler extensions such as InstanceSigs, etc. Empower students to use these tools to develop an intuition for the type system and how to use it to solve problems. You don’t need to explain anything in terms of JavaScript, and be careful about overusing metaphors, too. Comparing Haskell to other languages and making abstract concepts more concrete feel like easy wins, but don’t do either as a substitute for teaching and learning the language on its own terms.

19. A Haskell study group is not for people who can’t handle discipline and hard work.

The Haskell Book is nothing if not demanding. But the intensity of the curriculum is meant to guide students to develop an intuition for how the type system works and the ability to interpret the terse but expressive syntax of Haskell code as quickly as possible. It helps you build up a repertoire of fundamental concepts and techniques that lead to ever more complex, but still comprehensible, abstractions down the road. There are no shortcuts here. Diligent learners will rapidly establish for themselves that foundation of understanding, and it will help them move more easily, and with a greater sense of achievement, as more advanced concepts are introduced. Conversely, the less studious are unlikely to overcome the psychological barriers that make people think Haskell is difficult. They will grow frustrated and give up as their more enthusiastic peers come to seem like magicians when working with the REPL. The truth is just the difference in commitment.

20. A Haskell study group is not only about discipline and hard work.

After your meetings, go out with the group to a local bar or cafe. Pick a regular place so it becomes a tradition. Not only is it good for community cohesion, which is good for the continuation of your study group, but it gives people a venue for venting their natural desire to socialize—a venue that is not the meeting place itself. You’re likely going to end up with a core group of people who always come. Cultivate them. Cherish them. Protect their interests. Get the less committed to want to be a part of the in-crowd, and welcome them with open arms when they prove themselves worthy.

I know this site is a bit of a disaster zone, but if you like my writing or think you could learn something useful from me, please take a look at the Haskell book I've been writing. There's a free sample available too!

May 03, 2017 12:00 AM

May 01, 2017

Robert Harper

What, if anything, is a programming paradigm?

Just out, an essay on the Cambridge University Press author’s blog about “programming paradigms”, and why I did not structure Practical Foundations for Programming Languages around them.



Filed under: Programming, Teaching Tagged: programming languages

by Robert Harper at May 01, 2017 07:01 PM

FP Complete

What pure functional programming is all about: Part 2

In the last post, we covered the following:

  • What purity is and what it isn't.
  • We looked at functions and function composition.
  • We've looked at how reasoning is easier if you only have functions.

In this post, we'll explore:

  • SQL as a pure language, which is a familiar language to almost everybody.
  • How pure languages deal with the real-world and doing side-effects, which are obviously practical things to do.
  • Evaluation vs execution, the generalization of pure vs impure languages.

In the next post, we'll explore the performance and declarative-code-writing benefits of pure functional languages in particular detail, looking at generated code, assembly, performance, etc.

In a familiar setting: SQL

In the last post, we established that pure languages (like Haskell or PureScript) are unable to make observations about the real world directly.

So, then, the question is: How do pure languages interact with the real world? Let's look at SQL first, because everyone knows SQL, and then use that as a bridge towards how it's done in Haskell and other general purpose pure languages.

Imagine a subset of SQL which is pure. It's not a big leap: SQL is mostly pure anyway. I don't like it when people write an article and ask me to imagine a syntax that's in their heads, so here is trivial a PEG grammar, which you can try online here.

Select = 'SELECT ' Fields ' FROM ' Names Where?
Names = Name (', ' Name)*
Fields = Exp (', ' Exp)*
Where = ' WHERE ' Exp
Exp = Prefix? (Funcall / Condition / Name) (Connective Exp)?
Funcall = Name '(' Exp ')'
Condition = (Funcall / Name) Op Exp
Prefix = 'NOT '
Connective = ' AND ' / ' OR '
Op = ' = ' / ' <> ' / ' < ' / ' > ' / ' * '
Name = [a-zA-Z0-9]+

The following is an example of the above grammar.

SELECT sin(foo), bar * 3 FROM table1, table2 WHERE foo > 1 AND NOT bar = floor(foo)

This language is pure. The result of evaluating one of these expressions is the same every time. You can swap the order of commutative expressions like floor(foo) = bar and it doesn't change the meaning of the program. floor(x) * sin(y) = sin(y) * floor(x).

You get a description of the work you want to be done, and then the database engine (PostgreSQL, MySQL, SQL Server, etc.), usually creating an optimized query plan based on what it knows about your query and the database schema and contents, executes the query on the database, returning a collection of results.

You didn't write instructions about how to get the database, where to look on the database, how to map indices across tables and whether to do an index scan or a sequence scan, allocating a buffer, etc.

And yet, above, we clearly are giving the SQL engine a little program (not a turing complete one), that can compute conditionals and even functions (floor and sin) that we specified freely.

Because our little program is pure, SQL is capable of basically rewriting it completely, reducing it into a more normalized form without redundancy, and executing something far more efficient.

Look at what PostgreSQL is able to do with your queries. Here I do a query which works on an indexed field on a table with 37,626,086 rows. PostgreSQL knows both the query and my data, and plans accordingly, able to estimate the cost of how much work we'll have to do.

ircbrowse=> explain select * from event where id > 123 and id < 200*2;
                                    QUERY PLAN
 Index Scan using event_unique_id on event  (cost=0.56..857.20 rows=309 width=87)
   Index Cond: ((id > 123) AND (id < 400))

(The 200*2 was evaluated statically.)

Simply based on a static analysis of the SQL program.

Evaluation vs execution

The SQL example is a specific case of a more general way of separating two concerns: evaluation and execution (or interpretation). On the one side you have your declarative language that you can evaluate, pretty much in terms of substition steps (and that's how you do your reasoning, in terms of the denotational semantics), and on the other you have a separate program which interprets that language in "the real world" (associated with operational semantics).

I'm sure any programmer reading this easily understands the informal denotational semantics of the SQL mini language above, and would feel comfortable implementing one or more ways of executing it.

In the same way, Haskell and other pure languages, construct declarative descriptions of work which a separate program can execute.


What's evaluation, as differentiated from execution? To do your language's regular evaluation steps, as you might do on paper. If you've read your Structured and Interpretation of Computer Programs by MIT, you'll know this as the substitution model. Here's an example.

If you want to count the length of a linked list, you might do:

length [1, 2, 3]

And length is implemented like this:

length [] = 0
length (x:xs) = 1 + length xs

So let's evaluate the expression, step-by-step:

length [1, 2, 3]

1 + length [2, 3]

1 + (1 + length [3])

1 + (1 + (1 + length []))

1 + (1 + (1 + 0))

1 + (1 + 1)

1 + 2


Even if you don't know Haskell, I think the simple substitution steps to evaluate the expression are straight-forward and make sense. That's evaluation.

A Terminal mini-language

Let's look at a data type that models a list of terminal actions to perform. I realise that if you don't know Haskell or ML, the below is mostly nonsense. I'll also bring in JavaScript as a "lingua franca", so that the idea translates nicely.

(If it looks concise in Haskell and verbose in JavaScript, it's because JavaScript was designed for imperative, OO-style programming, and Haskell was designed for pure functional programming.)

data Terminal a
  = Print String (Terminal a)
  | GetLine (String -> Terminal a)
  | Return a
function Print(string, next) {
  this.line = string; = next;
function GetLine(cont) {
  this.f = cont;
function Return(a) {
  this.a = a;

It can describe printing to stdout, getting a line from stdin, or returning a result. An example might be:

  "Please enter your name: "
     (\name ->
           ("Hello, " ++ name ++ "!")
           (Return ())))
new Print(
  "Please enter your name: ",
  new GetLine(function(name){
    return new Print("Hello, " + name + "!",
                     new Return(null));}))

Think of this like an abstract syntax tree. It's the description of what to do. When there is a function in the AST, that's a callback. The callback is just another pure function that returns a new action to be interpreted.

The expressions above can be evaluated, but they perform no side-effects. It's a piece of purely functional code which generates a data structure. Our substitution model above still works.

Hammering the point home, consider a greeting action like this:

greeting :: String -> Terminal ()
greeting msg =
       (\name ->
          if name == "Chris"
            then Print "That's my name too." (Return ())
            else Print "Hello, stranger!" (Return ())))

The greeting function itself is pure. It takes a message string, and constructs a Print using that. That's done by evaluation. Also, the sub-expression (\name -> ...) is another pure function that takes a name and conditionally produces one action or another.

Now, onto execution.


We can write a number of ways to interpret this AST. Here is one pure implementation. It takes as input (1) some action list to run and (2) lines of input, then it returns a value and some output lines:

data Result a = Success a | Failure String deriving Show
interpretPure :: Terminal a -> [String] -> Result (a,[String])
interpretPure action stdin =
  case action of
    Return a -> Success (a, [])
    Print line next ->
      case interpretPure next stdin of
        Success (a, stdout) -> Success (a, line : stdout)
        Failure e -> Failure e
    GetLine f ->
      case stdin of
        [] -> Failure "stdin closed"
        (line:stdin') -> interpretPure (f line) stdin'

In diagram form:

Note the part,

    GetLine f ->
      case stdin of
        [] -> Failure "stdin closed"
        (line:stdin') -> interpretPure (f line) stdin'
-------------------------------------- ^

Above is where we call the pure function from GetLine to produce another action for us to interpret.

In JavaScript:

function Success(x){ this.success = x; }
function Failure(e){ this.error = e; }
function interpretPure(action, stdin) {
  if (action instanceof Return) {
    return new Success({ result: action.a, stdout: [] });
  } else if (action instanceof Print) {
    var result = interpretPure(, stdin);
    if (result instanceof Success) {
      return new Success({
        result: result.success.result,
        stdout: [action.line].concat(result.success.stdout)
    } else return result;
  } else if (action instanceof GetLine) {
    if (stdin == "") {
      return new Failure("stdin closed");
    } else {
      var line = stdin[0];
      var stdin_ = stdin.slice(1);
      return interpretPure(action.f(line), stdin_);

Which we can run like this:

> interpretPure demo ["Dave"]
Success ((),["Please enter your name: ","Hello, Dave!"])
> interpretPure demo []
Failure "stdin closed"
> JSON.stringify(interpretPure(demo, ["Dave"]));
"{"success":{"result":null,"stdout":["Please enter your name: ","Hello, Dave!"]}}"
> JSON.stringify(interpretPure(demo, []));
"{"error":"stdin closed"}"

If we liked, we could interpret this as real I/O that talks to the world directly.

In Haskell, we translate it to a different type called IO. In JavaScript, let's do a good olde-fashioned 90's-style alert/prompt user interaction.

interpretIO :: Terminal a -> IO a
interpretIO terminal =
  case terminal of
    Return a -> return a
    Print str next -> do
      putStrLn str
      interpretIO next
    GetLine f -> do
      line <- getLine
      interpretIO (f line)
function interpretIO(action) {
  if (action instanceof Return) {
    return action.a;
  } else if (action instanceof Print) {
  } else if (action instanceof GetLine) {
    var line = prompt();

In this case, we're just translating from one model to another. The IO a type is interpreted by the Haskell runtime either in a REPL prompt, or in a compiled program. JavaScript is capable of executing things directly during evaluation, so we were able to implement something similar to what Haskell's runtime does for IO.

In SICP, they talk about programs as being spells, and the interpreter being like a spirit that does your bidding. Here is a formal description:

(In practice, Haskell's IO type is not a closed set of operations, but an open set that can be extended with e.g. bindings to C libraries and such, and it isn't interpreted at runtime but rather compiled down to bytecode or machine code. The strict evaluation/execution separation remains in place, however.)


We've covered an informal comparison between "evaluating" and "executing" code, which is a distinction often discussed in the functional programming community.

We've explored making a declarative data type that represents terminal interaction, and implemented two different ways of interpreting it: as a pure function, or executing it directly. There may be other interpretations, such as talking to a server. We could write an interpreter which logs every action performed. We could also write a test suite which feeds randomized or specific inputs and demands consistent outputs.

We looked at how SQL is such an example of an evaluation (1 + 1 is evaluated before executing the query) vs execution separation. In SELECT customer.purchases + 1 FROM customer, the customer.purchases + 1 expression is evaluated by the interpreter for each row in the table.

In the next post, we'll explore:

  • Performance of pure code.
  • Optimization of pure code, in particular: Inlining, deforestation, common sub-expression elimination, fusion, rewrite rules, etc.
  • And how these optimizations allow for low- or zero-cost abstractions.

We may further explore different types of interpreters (software transactional memory, local mutation, parsers, etc).


There are some extra articles that may be of interest for the fearless:

May 01, 2017 04:04 PM

Douglas M. Auclair (geophf)

April 2017 1HaskellADay Problems and Solutions

by geophf ( at May 01, 2017 01:42 PM

April 30, 2017

Erik de Castro Lopo

What do you mean ExceptT doesn't Compose?

Disclaimer: I work at Ambiata (our Github presence) probably the biggest Haskell shop in the southern hemisphere. Although I mention some of Ambiata's coding practices, in this blog post I am speaking for myself and not for Ambiata. However, the way I'm using ExceptT and handling exceptions in this post is something I learned from my colleagues at Ambiata.

At work, I've been spending some time tracking down exceptions in some of our Haskell code that have been bubbling up to the top level an killing a complex multi-threaded program. On Friday I posted a somewhat flippant comment to Google Plus:

Using exceptions for control flow is the root of many evils in software.

Lennart Kolmodin who I remember from my very earliest days of using Haskell in 2008 and who I met for the first time at ICFP in Copenhagen in 2011 responded:

Yet what to do if you want composable code? Currently I have
type Rpc a = ExceptT RpcError IO a
which is terrible

But what do we mean by "composable"? I like the wikipedia definition:

Composability is a system design principle that deals with the inter-relationships of components. A highly composable system provides recombinant components that can be selected and assembled in various combinations to satisfy specific user requirements.

The ensuing discussion, which also included Sean Leather, suggested that these two experienced Haskellers were not aware that with the help of some combinator functions, ExceptT composes very nicely and results in more readable and more reliable code.

At Ambiata, our coding guidelines strongly discourage the use of partial functions. Since the type signature of a function doesn't include information about the exceptions it might throw, the use of exceptions is strongly discouraged. When using library functions that may throw exceptions, we try to catch those exceptions as close as possible to their source and turn them into errors that are explicit in the type signatures of the code we write. Finally, we avoid using String to hold errors. Instead we construct data types to carry error messages and render functions to convert them to Text.

In order to properly demonstrate the ideas, I've written some demo code and made it available in this GitHub repo. It compiles and even runs (providing you give it the required number of command line arguments) and hopefully does a good job demonstrating how the bits fit together.

So lets look at the naive version of a program that doesn't do any exception handling at all.

  import Data.ByteString.Char8 (readFile, writeFile)

  import Naive.Cat (Cat, parseCat)
  import Naive.Db (Result, processWithDb, renderResult, withDatabaseConnection)
  import Naive.Dog (Dog, parseDog)

  import Prelude hiding (readFile, writeFile)

  import System.Environment (getArgs)
  import System.Exit (exitFailure)

  main :: IO ()
  main = do
    args <- getArgs
    case args of
      [inFile1, infile2, outFile] -> processFiles inFile1 infile2 outFile
      _ -> putStrLn "Expected three file names." >> exitFailure

  readCatFile :: FilePath -> IO Cat
  readCatFile fpath = do
    putStrLn "Reading Cat file."
    parseCat <$> readFile fpath

  readDogFile :: FilePath -> IO Dog
  readDogFile fpath = do
    putStrLn "Reading Dog file."
    parseDog <$> readFile fpath

  writeResultFile :: FilePath -> Result -> IO ()
  writeResultFile fpath result = do
    putStrLn "Writing Result file."
    writeFile fpath $ renderResult result

  processFiles :: FilePath -> FilePath -> FilePath -> IO ()
  processFiles infile1 infile2 outfile = do
    cat <- readCatFile infile1
    dog <- readDogFile infile2
    result <- withDatabaseConnection $ \ db ->
                 processWithDb db cat dog
    writeResultFile outfile result

Once built as per the instructions in the repo, it can be run with:

  dist/build/improved/improved Naive/Cat.hs Naive/Dog.hs /dev/null
  Reading Cat file 'Naive/Cat.hs'
  Reading Dog file 'Naive/Dog.hs'.
  Writing Result file '/dev/null'.

The above code is pretty naive and there is zero indication of what can and cannot fail or how it can fail. Here's a list of some of the obvious failures that may result in an exception being thrown:

  • Either of the two readFile calls.
  • The writeFile call.
  • The parsing functions parseCat and parseDog.
  • Opening the database connection.
  • The database connection could terminate during the processing stage.

So lets see how the use of the standard Either type, ExceptT from the transformers package and combinators from Gabriel Gonzales' errors package can improve things.

Firstly the types of parseCat and parseDog were ridiculous. Parsers can fail with parse errors, so these should both return an Either type. Just about everything else should be in the ExceptT e IO monad. Lets see what that looks like:

  {-# LANGUAGE OverloadedStrings #-}
  import           Control.Exception (SomeException)
  import           Control.Monad.IO.Class (liftIO)
  import           Control.Error (ExceptT, fmapL, fmapLT, handleExceptT
                                 , hoistEither, runExceptT)

  import           Data.ByteString.Char8 (readFile, writeFile)
  import           Data.Monoid ((<>))
  import           Data.Text (Text)
  import qualified Data.Text as T
  import qualified Data.Text.IO as T

  import           Improved.Cat (Cat, CatParseError, parseCat, renderCatParseError)
  import           Improved.Db (DbError, Result, processWithDb, renderDbError
                               , renderResult, withDatabaseConnection)
  import           Improved.Dog (Dog, DogParseError, parseDog, renderDogParseError)

  import           Prelude hiding (readFile, writeFile)

  import           System.Environment (getArgs)
  import           System.Exit (exitFailure)

  data ProcessError
    = ECat CatParseError
    | EDog DogParseError
    | EReadFile FilePath Text
    | EWriteFile FilePath Text
    | EDb DbError

  main :: IO ()
  main = do
    args <- getArgs
    case args of
      [inFile1, infile2, outFile] ->
              report =<< runExceptT (processFiles inFile1 infile2 outFile)
      _ -> do
          putStrLn "Expected three file names, the first two are input, the last output."

  report :: Either ProcessError () -> IO ()
  report (Right _) = pure ()
  report (Left e) = T.putStrLn $ renderProcessError e

  renderProcessError :: ProcessError -> Text
  renderProcessError pe =
    case pe of
      ECat ec -> renderCatParseError ec
      EDog ed -> renderDogParseError ed
      EReadFile fpath msg -> "Error reading '" <> T.pack fpath <> "' : " <> msg
      EWriteFile fpath msg -> "Error writing '" <> T.pack fpath <> "' : " <> msg
      EDb dbe -> renderDbError dbe

  readCatFile :: FilePath -> ExceptT ProcessError IO Cat
  readCatFile fpath = do
    liftIO $ putStrLn "Reading Cat file."
    bs <- handleExceptT handler $ readFile fpath
    hoistEither . fmapL ECat $ parseCat bs
      handler :: SomeException -> ProcessError
      handler e = EReadFile fpath (T.pack $ show e)

  readDogFile :: FilePath -> ExceptT ProcessError IO Dog
  readDogFile fpath = do
    liftIO $ putStrLn "Reading Dog file."
    bs <- handleExceptT handler $ readFile fpath
    hoistEither . fmapL EDog $ parseDog bs
      handler :: SomeException -> ProcessError
      handler e = EReadFile fpath (T.pack $ show e)

  writeResultFile :: FilePath -> Result -> ExceptT ProcessError IO ()
  writeResultFile fpath result = do
    liftIO $ putStrLn "Writing Result file."
    handleExceptT handler . writeFile fpath $ renderResult result
      handler :: SomeException -> ProcessError
      handler e = EWriteFile fpath (T.pack $ show e)

  processFiles :: FilePath -> FilePath -> FilePath -> ExceptT ProcessError IO ()
  processFiles infile1 infile2 outfile = do
    cat <- readCatFile infile1
    dog <- readDogFile infile2
    result <- fmapLT EDb . withDatabaseConnection $ \ db ->
                 processWithDb db cat dog
    writeResultFile outfile result

The first thing to notice is that changes to the structure of the main processing function processFiles are minor but all errors are now handled explicitly. In addition, all possible exceptions are caught as close as possible to the source and turned into errors that are explicit in the function return types. Sceptical? Try replacing one of the readFile calls with an error call or a throw and see it get caught and turned into an error as specified by the type of the function.

We also see that despite having many different error types (which happens when code is split up into many packages and modules), a constructor for an error type higher in the stack can encapsulate error types lower in the stack. For example, this value of type ProcessError:

  EDb (DbError3 ResultError1)

contains a DbError which in turn contains a ResultError. Nesting error types like this aids composition, as does the separation of error rendering (turning an error data type into text to be printed) from printing.

We also see that with the use of combinators like fmapLT, and the nested error types of the previous paragraph, means that ExceptT monad transformers do compose.

Using ExceptT with the combinators from the errors package to catch exceptions as close as possible to their source and converting them to errors has numerous benefits including:

  • Errors are explicit in the types of the functions, making the code easier to reason about.
  • Its easier to provide better error messages and more context than what is normally provided by the Show instance of most exceptions.
  • The programmer spends less time chasing the source of exceptions in large complex code bases.
  • More robust code, because the programmer is forced to think about and write code to handle errors instead of error handling being and optional afterthought.

Want to discuss this? Try reddit.

April 30, 2017 02:22 AM

April 28, 2017

Neil Mitchell

HLint on Travis/Appveyor

Summary: Running HLint on your CI is now quick and easy.

I've always wanted to run HLint on my continuous integration servers (specifically Travis for Linux and Appveyor for Windows), to automatically detect code that could be improved. That has always been possible, and packages like lens and freer-effects have done so, but it was unpleasant for two reasons:

  • Setting up a custom HLint settings file and applying these settings was a lot of upfront work.
  • Building hlint on the CI server could be quite slow.

With HLint v2.0.4, both of these issues are addressed. I am now running HLint as standard for many of my projects. The two steps are outlined below.

Setting up custom HLint settings

Locally run hlint . --default > .hlint.yaml and it will generate a file which ignores all hints your project currently triggers. If you then run hlint . there will be no warnings, as the ignore settings will automatically be picked up. Check in .hlint.yaml.

Later, as a future step, you may wish to review your .hlint.yaml file and fix some of the warnings.

Running HLint on the server

There are now precompiled binaries at GitHub, along with scripts to download and execute them for each CI system. In both cases below, replace ARGUMENTS with your arguments to hlint, e.g. . to check the current directory.

On Travis, execute the following command:

wget -O - --quiet | sh -s ARGUMENTS

On Appveyor, add the following statements to .appveyor.yml:

- set PATH=C:\Program Files\Git\mingw64\bin;%PATH%
- curl -ohlint.bat -L

Since these are precompiled binaries the additional time required to run HLint should be minimal.

by Neil Mitchell ( at April 28, 2017 07:52 PM

José Pedro Magalhães

Four openings for Haskell developers at Standard Chartered

I'm happy to announce that the Strats team at Standard Chartered is still hiring! We currently have openings for four roles. These will typically involve direct contact with traders to automate processes, often in rapid delivery style.

The growing Strats team now consists of about 40 developers in either Singapore or London, working exclusively in Haskell. Dozens of people from other teams are also writing Haskell code, so this is a chance to join what's probably the largest Haskell dev team in the world, and work on the largest Haskell codebase (over 3 million lines of code).

We currently offer only contractor positions (with the possibility of conversion to permanent in the future) with very competitive compensation. We require demonstrated experience in typed FP (Haskell, OCaml, F# etc); no financial background is required. We also require physical presence in either Singapore or London, and offer a relocation package for international moves. Flexible work arrangements are possible, but relocation to the UK or Singapore is necessary.

If this sounds exciting to you, please email your CV and a short motivation text to Feel free to also ask any questions you might have.

by José Pedro Magalhães ( at April 28, 2017 01:02 PM

Joachim Breitner

ghc-proofs rules more now

A few weeks ago I blogged about an experiment of mine, where I proved equalities of Haskell programs by (ab)using the GHC simplifier. For more details, please see that post, or the video of my talk at the Zürich Haskell User Group, but one reason why this approach has any chance of being useful is the compiler’s support for rewrite rules.

Rewrite rules are program equations that the programmer specifies in the source file, and which the compiler then applies, from left to right, whenever some intermediate code matches the left-hand side of the equation. One such rule, for example, is

{-# RULES "foldr/nil" forall k z. foldr k z [] = z #-}

taken right out of the standard library.

In my blog post I went through the algebraic laws that a small library of mine, successors, should fulfill, and sure enough, once I got to more interesting proofs, they would not go through just like that. At that point I had to add additional rules to the file I was editing, which helped the compiler to finish the proofs. Some of these rules were simple like

{-# RULES "mapFB/id" forall c. mapFB c (\x -> x) = c #-}
{-# RULES "foldr/nil" forall k n. GHC.Base.foldr k n [] = n #-}
{-# RULES "foldr/undo" forall xs. GHC.Base.foldr (:) [] xs = xs #-}

and some are more intricate like

{-# RULES "foldr/mapFB" forall c f g n1 n2 xs.
    GHC.Base.foldr (mapFB c f) n1 (GHC.Base.foldr (mapFB (:) g) n2 xs)
    = GHC.Base.foldr (mapFB c (f.g)) (GHC.Base.foldr (mapFB c f) n1 n2) xs

But there is something fishy going on here: The foldr/nil rule is identical to a rule in the standard library! I should not have to add to my file that as I am proving things. So I knew that the GHC plugin, which I wrote to do these proofs, was doing something wrong, but I did not investigate for a while.

I returned to this problem recetly, and with the efficient and quick help of Simon Peyton Jones, I learned what I was doing wrong.1 After fixing it, I could remove all the simple rules from the files with my proofs. And to my surprise, I could remove the intricate rule as well!

So with this bug fixed, ghc-proofs is able to prove all the Functor, Applicative and Monad rules of the Succs functor without any additional rewrite rules, as you can see in the example file! (I still have to strategically place seqs in a few places.)

That’s great, isn’t it! Yeah, sure. But having to introduce the rules at that point provided a very good narrative in my talk, so when I will give a similar talk next week in Pairs (actually, twice, first at the university and then at the Paris Haskell meetup, I will have to come up with a different example that calls for additional rewrite rules.

In related news: Since the last blog post, ghc-proofs learned to interpret proof specifications like

applicative_law4 :: Succs (a -> b) -> a -> Proof
applicative_law4 u y = u <*> pure y
                   === pure ($ y) <*> u

where it previously only understood

applicative_law4 = (\ u (y::a) -> u <*> (pure y :: Succs a))
               === (\ u (y::a) -> pure ($ y) <*> u)

I am not sur if this should be uploaded to Hackage, but I invite you to play around with the GitHub version of ghc-proofs.

  1. In short: I did not initialize the simplifier with the right InScopeSet, so RULES about functions defined in the current module were not always applied, and I did not feed the eps_rules to the simplifier, which contains all the rules found in imported packages, such as base.

by Joachim Breitner ( at April 28, 2017 03:11 AM

April 27, 2017

Michael Snoyman

Stackage's no-revisions (experimental) field

I'm announcing a new, experimental field in the build-constraints.yaml file for Stackage. For those not familiar with Hackage revisions, let me give a quick rundown of how things work:

  • When you upload a package to Hackage, your tarball includes a .cabal file
  • That .cabal file gets included in the index tarball containing all .cabal files
  • From the Hackage website, package maintainers and Hackage Trustees are able to edit some metadata about a package, like its dependency bounds
  • When such an edit takes place, a new .cabal file is added at the end of the index tarball with the updated content
  • It is the responsibility of tooling (like cabal, Stack, and the Stackage build tools) to—when extracting a package's tarball—replace the original .cabal file with the correct version, usually the newest version available

When a Stackage build runs, until now it would always take the most recent revision of a .cabal file and use that for bounds checking (and other activities). Then, when creating a snapshot, it would include a hash of the revision of the .cabal file it used. That hash is in turn used by Stack to ensure that—when building a package from a snapshot—it uses the same revision for reproducibility.

(Sound complicated? It kind of is.)

OK, all that said: what's the problem? Well, there are some disagreements in certain cases about whether a revision to a package's .cabal file should have occurred. An unwanted revision can create undesired work for the package author. After this situation arose a few times, I discussed with some involved parties, and came up with the no-revisions field. Its purpose is really simple:

When the Stackage build tool is choosing which .cabal file revision to use, if a package is present in the no-revisions list, then the original revision is used. Otherwise, the newest revision is used.

UPDATE Someone pointed out that this "unwanted work" description was pretty vague. To clarify, here's an example situation:

  1. Package author Alice uploads package foo, and depends on bar >= 2.3 (with no upper bounds). The latest version of bar on Hackage is 2.3.
  2. Hackage Trustee Bob adds an upper so that, now, foo depends on bar >= 2.3 && < 2.4
  3. Package author Charlie uploads bar-2.4 to Hackage.
  4. Alice checks on her Git repo and sees that the current foo code is compatible with bar-2.4, so does nothing.
  5. Meanwhile, Stackage discovers the upper bounds and files a bug report for Alice to remove the upper bound (that she's not aware of).
  6. Alice needs to log in to Hackage and remove the upper bound (or at least relax it).
  7. Alternatively, with no-revisions in place, Alice could initially put foo in the no-revisions list, and then Bob's changes would be ignored completely by Stackage.

This is an opt-in field, so people who want the current behavior need not do anything. This change will transparently work for Stack, since it will simply respect the hash of the .cabal file. And since there may be some negative ramifications of this change I haven't considered, I'm calling this feature experimental and asking for feedback if this causing anyone some issues.

Hopefully this change will let people who are using the Stack and Stackage toolchain work with less interference, with less friction occurring with Hackage Trustees making version bounds modifications.

April 27, 2017 06:00 AM

Jasper Van der Jeugt

An informal guide to better compiler errors

Earlier this month I gave a talk at the HaskellX Bytes meetup on how to improve compiler errors.

Haskell is very commonly used to implement DSLs. When you implement one of these DSLs, the focus is usually performance or correctness. Something that’s not mentioned often is the “quality” of error messages.

In this talk I talked through some techniques to improve various kinds (parser, renamer, modules, interpreter, typechecker) of error messages and discuss how that impacts user experience.

The recording can be watched on their website. Unfortunately I cannot embed it here, but at least you can watch it without creating an account.

The slides can be found here.

by Jasper Van der Jeugt at April 27, 2017 12:00 AM

April 25, 2017

Roman Cheplyaka

Generic zipWith

In response to the traverse-with-class 1.0 announcement, user Gurkenglas asks:

Can you use something like this to do something like gzipWith (+) :: (Int, Double) -> (Int, Double) -> (Int, Double)?

There are two separate challenges here:

  1. How do we traverse two structures in lockstep?
  2. How do we make sure that the values we are combining are of the same type?

Because traverse-with-class implements Michael D. Adams’s generic zipper, I first thought that it would suffice to traverse the two values simultaneously. That didn’t quite work out. That zipper is designed to traverse the structure in all four directions: not just left and right, but also up and down. Therefore, if we want to traverse an (Int, Double) tuple with a Num constraint, all possible substructures — including (Int, Double) itself — must satisfy that constraint. The way this manifests itself is through Rec c constraints, which cannot be satisfied for tuples without defining extra Num instances.

It is possible to design a restricted zipper that would only travel left and right and will not impose any unnecessary constraints. But because we need only a simple one-way traversal, we can get away with something even simpler — a free applicative functor. (Indeed, a free applicative is a building block in Adams’s zipper.)

This is simple and beautiful: because a free applicative functor is an applicative functor, we can gtraverse with it; and because a free applicative functor is essentially a heterogeneous list, we can zip two such things together.

Another way we could approach this is by using Oleg’s Zipper from any Traversable, which is based on the continuation monad. I haven’t tried it, but I think it should work, too.

Now we arrive at the second challenge. In traverse-with-class, when we traverse a heterogeneous value, we observe each field as having an existential type exists a . c a => a. If the type of (+) was something like (Num a1, Num a2) => a1 -> a2 -> a1 — as it is in many object-oriented languages — it would be fine. But in Haskell, we can only add two Num values if they are of the same type.

Packages like one-liner or generics-sop use a type-indexed generic representation, so we can assert field-wise type equality of two structures at compile time. traverse-with-class is not typed in this sense, so we need to rely on run-time type checks via Typeable.

The full code for gzipWith is given below. Note that relying on Ørjan’s free applicative has two important consequences:

  1. We zip from right to left, so that gzipWith @Num (+) [1,2,3] [1,2] evaluates to [3,5], not [2,4].
  2. For GTraversable instances that are right-associated (e.g. the standard GTraversable instance for lists), the complexity is quadratic.

I believe that both of these issues can be resolved, but I don’t have the time to spend on this at the moment.

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances,
             ConstraintKinds, RankNTypes, AllowAmbiguousTypes, TypeApplications,
             UndecidableInstances, GADTs, UndecidableSuperClasses,
             FlexibleContexts, TypeOperators #-}

import Data.Typeable
import Data.Generics.Traversable

-- TypeableAnd c is a synonym for (c a, Typeable a)
class    (c a, Typeable a) => TypeableAnd c a
instance (c a, Typeable a) => TypeableAnd c a

-- Ørjan Johansen’s free applicative functor
data Free c a
  = Pure a
  | forall b. (c b, Typeable b) => Snoc (Free c (b -> a)) b

instance Functor (Free c) where
  fmap f (Pure x) = Pure $ f x
  fmap f (Snoc lft x) = Snoc (fmap (f .) lft) x

instance Applicative (Free c) where
  pure = Pure
  tx <*> Pure e = fmap ($ e) tx
  tx <*> Snoc ty az = Snoc ((.) <$> tx <*> ty) az

unit :: TypeableAnd c b => b -> Free c b
unit = Snoc (Pure id)

toFree :: forall c a . GTraversable (TypeableAnd c) a => a -> Free c a
toFree = gtraverse @(TypeableAnd c) unit

fromFree :: Free c a -> a
fromFree free =
  case free of
    Pure a -> a
    Snoc xs x -> fromFree xs x

zipFree :: (forall b . c b => b -> b -> b) -> Free c a -> Free c a -> Free c a
zipFree f free1 free2 =
  case (free1, free2) of
    (Pure a1, _) -> Pure a1
    (_, Pure a2) -> Pure a2
    (Snoc xs1 (x1 :: b1), Snoc xs2 (x2 :: b2)) ->
      case (eqT :: Maybe (b1 :~: b2)) of
        Nothing -> error "zipFree: incompatible types"
        Just Refl -> Snoc (zipFree f xs1 xs2) (f x1 x2)

  :: forall c a . GTraversable (TypeableAnd c) a
  => (forall b . c b => b -> b -> b)
  -> a -> a -> a
gzipWith f a1 a2 = fromFree $ zipFree f (toFree @c a1) (toFree @c a2)

zippedTuple :: (Int, Double)
zippedTuple = gzipWith @Num (+) (1, 1) (3, pi)
-- (4,4.141592653589793)

April 25, 2017 08:00 PM

April 24, 2017


Upcoming courses and events 2017

We are excited to be teaching Haskell courses once again – in June 2017, at Skills Matter’s CodeNode venue in London.

We are offering three courses:

Fast Track to Haskell (26-27 June)

Compact two-day course aimed at software developers with no prior experience in Haskell who want to learn the fundamentals of Haskell and functional programming.

Guide to the Haskell Type System (28 June)

One-day course covering most of GHC’s extensions of the Haskell type system, such as GADTs, data kinds, and type families. Suitable for Haskellers who want to get most out of Haskell’s powerful type system and understand the trade-offs involved.

Guide to Haskell Performance and Optimization (29-30 June)

Two-day course focusing on the internals of GHC, the evaluation strategy, how programs are compiled and executed at run-time. Explains how to choose the right data structure for your program in a lazy functional language, what kind of optimizations you can expect the compiler to perform, and how to write beautiful programs that scale.

Each of these courses is open for registration, with reduced rates available if you book soon.

The courses will also be held again in October 2017, in connection with the Haskell eXchange.

We also provide on-site (and remote) courses tailored to your specific needs. If you want to know more, have a look at our training page or contact us.

Other upcoming events

The following are some other events in 2017 we are planning to participate in (we may be at other events, too):

ZuriHac (9-11 June 2017)

As in previous years, we’ll be at ZuriHac again, which is the largest European Haskell Hackathon. Whether you’re a newcomer who wants to try Haskell for the first time or an experienced Haskeller with many years of experience, we are looking forward to meeting you there.

ICFP + Haskell Symposium + HIW + CUFP (3-9 September 2017)

The annual International Conference on Functional Programming will take place in Oxford this year. A full week of events focused on functional programming, including the two-day Haskell Symposium and the Haskell Implementors Workshop. There’s also the Commercial Users of Functional Programming conference which features several tutorials on various programming languages and techniques.

We will certainly be there and participate actively.

Haskell eXchange (12-13 October 2017 + 14-15 October 2017)

The two-day Haskell developer conference organized by us and Skills Matter in London is back for another year. We are currently looking for talk proposals for this conference, so if you have anything you would like to present, please submit! Registration is also open already, and tickets are cheaper the earlier you book.

There’s also going to be a two-day hackathon / unconference on the weekend after the Haskell eXchange.

If you would be interested in sponsoring the Haskell eXchange, please let us know.

by andres at April 24, 2017 08:20 AM

Ken T Takusagawa

[vqoxpezv] Omitting named function arguments

Consider a programming language whose syntax for function calls requires naming each passed argument, but as a benefit for this extra verbosity, allows specifying the arguments in any order:

f { foo = 3, bar = True, baz = "hello" }

If an argument is omitted, there are several things that could happen, depending on how the language is defined.

  1. Compile time error.
  2. It becomes a partial function application, a lambda function of the missing arguments.  Haskell does this with currying when trailing arguments are omitted.  (Tangentially, in Haskell, creating a lambda for a missing argument that is not the last one requires a little bit more work.)
  3. The missing arguments get silently assigned a lazy "undefined" value, which results in a run-time error if the "undefined" is ever evaluated.
  4. The language permits the function definition to provide default values to some omitted arguments.  If there is no default value, then compile-time error.  C++ does this.

It would be nice if a language could provide all of these options, even though strictly speaking they are mutually exclusive.

An imperfect solution is to have special keywords invoking #2, #3 and #4, perhaps something like f { foo = 3, REST UNDEFINED } or REST DEFAULT or REST LAMBDA, explicitly indicating indicating what do with the rest of arguments omitted at a call site.

I have seen default values implemented in Haskell using its typeclass mechanism, e.g., configuration values in xmonad.  Default values are overridden using record modification syntax.

A hybrid between #1 and #4 would have the compiler always produce an error if arguments are missing, but indicate in the compile error that a default value is available via an explicit keyword (as above) when one is.

A list of named parameters and their values looks kind of like a record or struct.  Make such a list a real type and allow variables of that type to be declared and assigned.  A special syntax allows invoking a function with a record instead of a named argument list.  If two functions have the same named parameters, are their parameter record types the same?  Duck typing.

This scheme also gets​ messy when arguments may be omitted; we need to be able to define record types with only a subset of the parameters of a function, as well as possibly allowing REST UNDEFINED or REST DEFAULT as dynamic values in the record.  If using REST LAMBDA, and whether a record field is defined is only known dynamically, then type checking and kind checking has to be postponed until run-time.

One of the things that makes me uneasy about Haskell record syntax is the following: REST UNDEFINED (#3) occurs implicitly when records are constructed whereas REST LAMBDA (#2) occurs when omitting trailing arguments when using positional constructors.  The latter will usually cause a type checking error if the argument was omitted accidentally whereas the former waits for a run-time error.

Previously: Same idea.

Having to specify a function name as well as all its parameter names might become tedious for the programmer.  Perhaps have mechanisms for a programmer to define alternate parameter names or omit a name.  Vaguely related: by type.

by Ken ( at April 24, 2017 08:06 AM

Michael Snoyman

Haskell Success Stories

I've probably blogged, spoken, Tweeted, and commented on a variation on this theme many times in the past, so please excuse me for being a broken record. This is important.

I think we have a problem in the Haskell community. We all know that using Haskell to create a simple web service, a CRUD app, a statically linked command line tool, or a dozen other things is not only possible, but commonplace, trivial, and not even noteworthy. So we don't bother commenting when we create general purpose reverse proxy tools with prebuilt Docker images for auth-enabling arbitrary webapps. It's boring. Unfortunately, people outside our community don't know this. By not bothering to talk about this (for us) boring topic, we're hiding away the fact that Haskell is a practical language for creating real things.

Instead, we like to talk about better preludes, optimizing common functions, or dangers in our standard libraries. I'm picking on myself here with these examples, but my comments apply far more generally.

I know personally at least 10-15 Haskell success stories that have never been talked about publicly. And I have to apologize for not leading by example here; unfortunately most of my work in the past few years has either been under NDA, or been of absolutely no interest to people outside the Haskell community (usually open source infrastructure and libraries). So I'm hoping to inspire others to step up to the plate.

I'm not trying to tell anyone to stop talking about the things we find interesting. I just want to point out that just because we, within the Haskell community, may not find a "I launched a web service, and it's running, and it's not as buggy as we would have expected v1 to be" kind of blog post noteworthy, I think others will. These kinds of blog posts are also a much easier way to get started talking publicly about Haskell, since not all of us can explain zygohistomorphic prepomorphisms (I know I certainly can't).

As I was batting the idea for this post around with my wife last night, she pointed out that, most likely, the people best suited to write these kinds of posts may not have dedicated blogs at all right now. If you fall into that category, but would still be interested in writing up a post about your Haskell success story, I'd like to offer assistance. I'm happy to let guests write posts on the Yesod blog. Articles may also be relevant to And we've run Haskell experience reports on FP Complete's website many times in the past.

I hope this time around this message had a bit of a different twist, and maybe can hit a different group of readers.

April 24, 2017 06:00 AM

April 23, 2017

Roman Cheplyaka

traverse-with-class 1.0 release

I have released the 1.0 version of traverse-with-class. This library generalizes many Foldable and Traversable functions to heterogeneous containers such as records.

For instance, you can apply Show to all fields and collect the results:

{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,
             ConstraintKinds, UndecidableInstances, TypeApplications #-}

import Data.Generics.Traversable
import Data.Generics.Traversable.TH

data User a = User
 { name :: String
 , age  :: Int
 , misc :: a

deriveGTraversable ''User

allFields = gfoldMap @Show (\x -> [show x]) $ User "Alice" 22 True
-- ["\"Alice\"","22","True"]

You also get a free zipper for your data types.

The main change in the version 1.0 is that the constraint with which the traversal is conducted is specified via a visible type application. Type applications weren’t available when I originally wrote this library in 2013, so in that version I used implicit parameters to pass around the annoying proxies.

Thanks to Hao Lian for his help with this transition.

Right after I published this blog post, I saw this tweet:

<script async="async" charset="utf-8" src=""></script>

Guess what, traverse-with-class provides the sensible Foldable-like instance for tuples:

{-# LANGUAGE FlexibleInstances, TypeApplications #-}

import Data.Generics.Traversable

-- U is a trivial constraint satisfied by all types
class U a
instance U a

tupleLength = gfoldl' @U (\c _ -> c + 1) 0 (1::Int, True)
-- returns 2

April 23, 2017 08:00 PM


Talk: Real World Reflex

I recently gave a talk at BayHac about some of the things I've learned in building production Reflex applications. If you're interested, you can find it here: video slides github

by mightybyte ( at April 23, 2017 12:00 PM

Chris Smith

CodeWorld Video Presentation

If you’re interested, I gave a presentation on CodeWorld at BayHac a few weeks ago.  The video is now available.


by cdsmith at April 23, 2017 06:37 AM

April 22, 2017

Brandon Simmons

Choosing a binary-to-text encoding

I had an occasion to think about text-friendly binary encoding schemes for the first time at work. The obvious choice is Base64, but my immediate subsequent thought was “there must be something much more efficient for our purposes”, and a quick google led here in which OP echos the same feeling:

It seems to me that we can greatly improve since on my keyboard I already see 94 easily distinguishable printable keys.

But of course if our goal is to “greatly improve” over Base64, then with a with a little thought we might conclude that the answer is “no, we can’t”. In Base64 we use 2^6 = 64 tokens, each of which represents a 6-bit string. Since those tokens are ASCII they take up 8-bits. So with Base64 we’re already at 75% efficiency (or “25% bloat”, or “33% larger than binary”), which seems… not so bad.

You can read about other binary encoding schemes here. From that table, we can see that Base85 which @rene suggests is modestly-better at 80% efficient. Base122 (the best on the list that can reasonably be called a “text encoding”) is 86% efficient.

Decision criteria

So you can make your messages ~13% smaller by ditching Base64 for the most exotic Base122, but what about other considerations?

Things you really want in a binary-to-text encoding, aside from size-efficiency are:

  • correct cross-platform compatible encoding/decoding; easy to get right
  • fast to encode/decode
  • compresses well (gzip is everywhere)

Other things that would be nice are that the encoding make some sense to the naked eye, be easily diffable, maybe even support some operations without requiring decoding (a binary search say).

It’s possible that all of these are more important to you than the efficiency of the raw encoding. With that in mind let’s consider a third (in addition to Base64 and BaseExoticInteger): the venerable hex encoding.

Hexadecimal (base-16) encoding requires two ASCII characters to represent a byte, so it’s 50% efficient. But as we’ll see it’s arguably better than these other two according to every other of our criteria!

Base64 is not sensible to the naked eye

Base64 encodes 6 bits per character. This means 3 octets (bytes) of input become 4 characters of the output. In a world where our data is overwhelmingly based on bytes and words our Base64 encoding is horribly out of phase!

When we see the two strings:


…our senses don’t tell us anything. Whereas in hex the lizard brain is able to perceive patterns, symmetry and magnitude right away:


There must be value to being able to use our eyes (especially when it’s the only sense we haven’t abandoned for the work we’re doing). The former might represent an obscured bug in an encryption routine for instance.

Interestingly a Base85 encoding is also superior to Base64 in this respect: every 5 characters represent 4 bytes of the input, so we retain the ability to recognize and compare 32- and 64-bit word chunks.

Base85 is tricky, but Base64 is the worst kind of tricky

It’s a nearly-alphanumeric encoding, which reserves for the (in some cases, more rare) last two code words the + and / characters. Furthermore the choice of these last two characters varies among implementations. I have no doubt that this has caused bugs, e.g. a validation regex that assumed an alphanumeric encoding.

Similarly, the encoding must itself be url-encoded if the + and / scheme is used, which has certainly caused bugs. Same story for the = padding rule (quite possible to misunderstand, fail to test against, or never observe in examples).

Base85 schemes are of course more complicated (and likely slower). We’d hope to find well-tested implementations on all the platforms we require but even so we should be prepared for the possibility that we’d need to implement it ourselves in the future.

More compact encodings compress worse

Much of the data flying around the internet is gzipped at some layer of a protocol. Because Base64/85 etc. are out of phase with bytes, and word sizes, they tend to frustrate compression schemes by obscuring patterns in block oriented data. Here are examples of gzip applied to the same tortured Hobbes quote (270 bytes of ASCII text, compressing to 194 bytes):

Encoding | Original size | Compressed size
-------- | ------------- | ---------------
hex      | 541           | 249
Base64   | 361           | 289
Base85   | 342           | 313

So for uncompressed binary data we can probably expect a more compact encoding to result in more bloat over the wire in a gzipped payload.

Two other things that were interesting to me:

  • all of the compression tools I tried did worse on the hex encoded string than on the original ascii. Maybe that’s due to the size required for the decoding table? We could test on larger strings
  • gzip was able to compress 361 bytes drawn from /dev/urandom to 316 bytes, so it’s clear Base64 doesn’t wholly obscure the structure of the data to our compression algorithm

Other alternatives and conclusions

It probably doesn’t matter, so just use Base64. If size is the only thing that matters then I’d suggest zipping first and then using the most gnarly encoding you can stomach. But maybe you should be using a proper binary protocol in that case.

In a world where it was totally ubiquitous I would suggest using either the terminal-friendly ZeroMQ Base85 flavor or a simple hex encoding.

I also like that encodings like this one exist though. It’s worth stepping back, doing some quick math, and making sure that you’re optimizing for the right thing.

April 22, 2017 08:22 PM

April 21, 2017

Joachim Breitner

veggies: Haskell code generation from scratch

How hard it is to write a compiler for Haskell Core? Not too hard, actually!

I wish we had a formally verified compiler for Haskell, or at least for GHC’s intermediate language Core. Now formalizing that part of GHC itself seems to be far out of reach, with the many phases the code goes through (Core to STG to CMM to Assembly or LLVM) and optimizations happening at all of these phases and the many complicated details to the highly tuned GHC runtime (pointer tagging, support for concurrency and garbage collection).

Introducing Veggies

So to make that goal of a formally verified compiler more feasible, I set out and implemented code generation from GHC’s intermediate language Core to LLVM IR, with simplicity as the main design driving factor.

You can find the result in the GitHub repository of veggies (the name derives from “verifiable GHC”). If you clone that and run ./ some-directory, you will find that you can use the program some-directory/bin/veggies just like like you would use ghc. It comes with the full base library, so your favorite variant of HelloWorld might just compile and run.

As of now, the code generation handles all the Core constructs (which is easy when you simply ignore all the types). It supports a good number of primitive operations, including pointers and arrays – I implement these as need – and has support for FFI calls into C.

Why you don't want to use Veggies

Since the code generator was written with simplicity in mind, performance of the resulting code is abysmal: Everything is boxed, i.e. represented as pointer to some heap-allocated data, including “unboxed” integer values and “unboxed” tuples. This is very uniform and simplifies the code, but it is also slow, and because there is no garbage collection (and probably never will be for this project), will fill up your memory quickly.

Also, the code is currently only supports 64bit architectures, and this is hard-coded in many places.

There is no support for concurrency.

Why it might be interesting to you nevertheless

So if it is not really usable to run programs with, should you care about it? Probably not, but maybe you do for one of these reasons:

  • You always wondered how a compiler for Haskell actually works, and reading through a little over a thousands lines of code is less daunting than reading through the 34k lines of code that is GHC’s backend.
  • You have wacky ideas about Code generation for Haskell that you want to experiment with.
  • You have wacky ideas about Haskell that require special support in the backend, and want to prototype that.
  • You want to see how I use the GHC API to provide a ghc-like experience. (I copied GHC’s Main.hs and inserted a few hooks, an approach I copied from GHCJS).
  • You want to learn about running Haskell programs efficiently, and starting from veggies, you can implement all the trick of the trade yourself and enjoy observing the speed-ups you get.
  • You want to compile Haskell code to some weird platform that is supported by LLVM, but where you for some reason cannot run GHC’s runtime. (Because there are no threads and no garbage collection, the code generated by veggies does not require a runtime system.)
  • You want to formally verify Haskell code generation. Note that the code generator targets the same AST for LLVM IR that the vellvm2 project uses, so eventually, veggies can become a verified arrow in the top right corner map of the DeepSpec project.

So feel free to play around with veggies, and report any issues you have on the GitHub repository.

by Joachim Breitner ( at April 21, 2017 03:30 PM

April 20, 2017

Dimitri Sabadie

Postmortem #1 – Revision 2017

On the weekend of 14th – 17th of April 2017, I was attending for the forth time the easter demoparty Revision 2017. This demoparty is the biggest so far in the world and gathers around a thousand people coming from around the world. If you’re a demomaker, a demoscene passionated or curious about it, that’s the party to go. It hosts plenty of competitions, among photos, modern graphics, oldschool graphics, games, size-limited demos (what we call intros), demos, tracked and streamed music, wild, live compo, etc. It’s massive.

So, as always, once a year, I attend Revision. But this year, it was a bit different for me. Revision is very impressive and most of the “big demogroups” release their productions they’ve been working on for months or even years. I tend to think “If I release something here, I’ll just be kind of muted by all those massive productions.” Well, less than two weeks before Revision 2017, I was contacted by another demogroup. They asked me to write an invitro – a kind of intro or demo acting as a communication production to invite people to go to another party. In my case, I was proposed to make the Outline 2017 invitro. Outline was the first party I attended years back then, so I immediately accepted and started to work on something. That was something like 12 days before the Revision deadline.

I have to tell. It was a challenge. All productions I wrote before was made in about a month and a half and featured less content than the Outline Invitation. I had to write a lot of code from scratch. A lot. But it was also a very nice project to test my demoscene framework, written in Rust – you can find spectra here or here

An hour before hitting the deadline, the beam team told me their Ubuntu compo machine died and that it would be neat if I could port the demo to Windows. I rushed like a fool to make a port – I even forked and modified my OpenAL dependency! – and I did it in 35 minutes. I’m still a bit surprised yet proud that I made it through!

Anyway, this post is not about bragging. It’s about hindsight. It’s a post-mortem. I did that for Céleri Rémoulade as I was the only one working on it – music, gfx, direction and obviously the Rust code. I want to draw a list of what went wrong and what went right. In the first time, for me. So that I have enhancement axis for the next set of demos I’ll make. And for sharing those thoughts so that people can have a sneak peek into the internals of what I do mostly – I do a lot of things! :D – as a hobby on my spare time.

You can find the link to the production here (there’re Youtube links if you need).

What went wrong

Sooooooooo… What went wrong. Well, a lot of things! spectra was designed to build demo productions in the first place, and it’s pretty good at it. But something that I have to enhance is the user interaction. Here’s a list of what went wrong in a concrete way.

Hot-reloading went wiiiiiiiiiiild²

With that version of spectra, I added the possibility to hot-reload almost everything I use as a resource: shaders, textures, meshes, objects, cameras, animation splines, etc. I edit the file, and as soon as I save it, it gets hot-reloaded in realtime, without having to interact with the program (for curious ones, I use the straight-forward notify crate crate for registering callbacks to handle file system changes). This is very great and it saves a lot of time – Rust compilation is slow, and that’s a lesson I’ve learned from Céleri Rémoulade: keeping closing the program, making a change, compiling and then running is a waste of time.

So what’s the issue with that? Well, the main problem is the fact that in order to implement hot-reloading, I wanted performance and something very simple. So I decided to use shared mutable smart states. As a Haskeller, I kind of offended myself there – laughter! Yeah, in the Haskell world, we try hard to avoid using shared states – IORef – because it’s not referentially transparent and reasoning about it is difficult. However, I tend to strongly think that in some very specific cases, you need such side-effects. I’m balanced but I think it’s the way to go.

Well, in Rust, shared mutable state is implemented via two types: Rc/Arc and Cell/RefCell.

The former is a runtime implementation of the Rust borrowing rules and enables you to share a value. The borrowing rules are not enforced at compile-time anymore but dynamically checked. It’s great because in some cases, you can’t know how long your values will be borrowed for or live. It’s also dangerous because you have to pay extra attention to how you borrow your data – since it’s checked at runtime, you can literally crash your program if you’re not extra careful.

Rc means ref counted and Arc means atomic-ref counted. The former is for values that stay on the same and single thread; the latter is for sharing between threads.

Cell/RefCell are very interesting types that provide internal mutation. By default, Rust gives you external mutation. That is, if you have a value and its address, can mutate what you have at that address. On the other hand, internal mutation is introduced by the Cell and RefCell types. Those types enable you to mutate the content of an object stored at a given address without having the exterior mutation property. It’s a bit technical and related to Rust, but it’s often used to mutate the content of a value via a function taking an immutable value. Imagine an immutable value that only holds a pointer. Exterior mutation would give you the power to change what this pointer points to. Interior mutation would give you the power to change the object pointed by this pointer.

Cell only accepts values that can be copied bit-wise and RefCell works with references.

Now, if you combine both – Rc<RefCell<_>>, you end up with a single-thread shareable – Rc<_> – mutable – RefCell<_> – value. If you have a value of type Rc<RefCell<u32>> for instance, that means you can clone that integer and store it everywhere in the same thread, and at any time, borrow it and inspect and/or mutate it. All copies of the value will observe the change. It’s a bit like C++’s shared_ptr, but it’s safer – thank you Rust!

So what went wrong with that? Well, the borrow part. Because Rust is about safety, you still need to tell it how you want to borrow at runtime. This is done with the [RefCell::borrow()](] and RefCell::borrow_mut() functions. Those functions return special objects that borrow the ref as long as it lives. Then, when it goes out of scope, it releases the borrow.

So any time you want to use an object that is hot-reloadable with my framework, you have to call one of the borrow functions presented above. You end up with a lot of borrows, and you have to keep in mind that you can litterally crash your program if you violate the borrowing rules. This is a nasty issue. For instance, consider:

let cool_object = …; // Rc<RefCell<Object>>, for instance
let cool_object_ref = cool_object.borrow_mut();
// mutate cool_object

just_read(&cool_object.borrow()); // borrowing rule violated here because a mut borrow is in scope

As you can see, it’s pretty simple to fuck up the program if you don’t pay extra attention to what you’re doing with your borrow. To solve the problem above, you’d need a smaller scope for the mutable borrow:

let cool_object = …; // Rc<RefCell<Object>>, for instance

let cool_object_ref = cool_object.borrow_mut();
// mutate cool_object

just_read(&cool_object.borrow()); // borrowing rule violated here because a mut borrow is in scope

So far, I haven’t really spent time trying to fix that, but that’s something I have to figure out.

Resources declaration in code

This is a bit tricky. As a programmer, I’m used to write algorithms and smart architectures to transform data and resolve problems. I’m given inputs and I provide the outputs – the solutions. However, a demoscene production is special: you don’t have inputs. You create artsy audiovisual outputs from nothing but time. So you don’t really write code to solve a problem. You write code to create something that will be shown on screen or in a headphone. This aspect of demo coding has an impact on the style and the way you code. Especially in crunchtime. I have to say, I was pretty bad on that part with that demo. To me, code should only be about transformations – that’s why I love Haskell so much. But my code is clearly not.

If you know the let keyword in Rust, well, imagine hundreds and hundreds of lines starting with let in a single function. That’s most of my demo. In rush time, I had to declare a lot of things so that I can use them and transform them. I’m not really happy with that, because those were data only. Something like:

let outline_emblem = cache.get::<Model>("Outline-Logo-final.obj", ()).unwrap();
let hedra_01 = cache.get::<Model>("DSR_OTLINV_Hedra01_Hi.obj", ()).unwrap();
let hedra_02 = cache.get::<Model>("DSR_OTLINV_Hedra02_Hi.obj", ()).unwrap();
let hedra_04 = cache.get::<Model>("DSR_OTLINV_Hedra04_Hi.obj", ()).unwrap();
let hedra_04b = cache.get::<Model>("DSR_OTLINV_Hedra04b_Hi.obj", ()).unwrap();
let twist_01 = cache.get::<Object>("DSR_OTLINV_Twist01_Hi.json", ()).unwrap();

It’s not that bad. As you can see, spectra features a resource cache that provides several candies – hot-reloading, resource dependency resolving and resource caching. However, having to declare those resources directly in the code is a nasty boilerplate to me. If you want to add a new object in the demo, you have to turn it off, add the Rust line, re-compile the whole thing, then run it once again. It breaks the advantage of having hot-reloading and it pollutes the rest of the code, making it harder to spot the actual transformations going on.

This is even worse with the way I handle texts. It’s all &'static str declared in a specific file called with the same insane load of let. Then I rasterize them in a function and use them in a very specific way regarding the time they appear. Not fun.

Still not enough data-driven

As said above, the cache is a great help and enables some data-driven development, but that’s not enough. The file is more than 600 lines long and 500 lines are just declarations of of clips (editing) and are all very alike. I intentionally didn’t use the runtime version of the timeline – but it’s already implemented – because I was editing a lot of code at that moment, but that’s not a good excuse. And the timeline is just a small part of it (the cuts are something like 10 lines long) and it annoyed me at the very last part of the development, when I was synchronizing the demo with the soundtrack.

I think the real problem is that the clips are way too abstract to be a really helpful abstraction. Clips are just lambdas that consume time and output a node. This also has implication (you cannot borrow something for the node in your clip because of borrowing rules ; duh!).

Animation edition

Most of the varying things you can see in my demos are driven by animation curves – splines. The bare concept is very interesting: an animation contains control points that you know have a specific value at a given time. Values in between are interpolated using an interpolation mode that can change at each control points if needed. So, I use splines to animate pretty much everything: camera movements, objects rotations, color masking, flickering, fade in / fade out effects, etc.

Because I wanted to be able to edit the animation in a comfy way – lesson learned from Céleri Rémoulade, splines can be edited in realtime because they’re hot-reloadable. They live in JSON files so that you just have to edit the JSON objects in each file and as soon as you save it, the animation changes. I have to say, this was very ace to do. I’m so happy having coded such a feature.

However, it’s JSON. It’s already a thing. Though, I hit a serious problem when editing the orientations data. In spectra, an orientation is encoded with a unit quaternion. This is a 4-floating number – hypercomplex. Editing those numbers in a plain JSON file is… challenging! I think I really need some kind of animation editor to edit the spline.

Video capture

The Youtube capture was made directly in the demo. At the end of each frame, I dump the frame into a .png image (with a name including the number of the frame). Then I simply use ffmpeg to build the video.

Even though this is not very important, I had to add some code into the production code of the demo and I think I could just refactor that into spectra. I’m talking about three or four lines of code. Not a big mess.


This is will appear as both pros. and cons. Compositing, in spectra, is implemented via the concept of nodes. A node is just an algebraic data structure that contains something that can be connected to another thing to compose a render. For instance, you get find nodes of type render, color, texture, fullscreen effects and composite – the latter is used to mix nodes between them.

Using the nodes, you can build a tree. And the cool thing is that I implemented the most common operators from std::ops. I can then apply a simple color mask to a render by doing something like

render_node * RGBA::new(r, g, b, a).into()

This is extremely user-friendly and helped me a lot to tweak the render (the actual ASTs are more complex than that and react to time, but the idea is similar). However, there’s a problem. In the actual implementation, the composite node is not smart enough: it blends two nodes by rendering them into a separate framebuffer (hence two framebuffers), then sample via a fullscreen quad the left framebuffer and then the right one – and apply the appropriate blending.

I’m not sure about performance here, but I feel like this is the wrong way to go – bandwidth! I need to profile.

On a general note: data vs. transformations

My philosphy is that code should be about transformation, not data. That’s why I love Haskell. However, in the demoscene world, it’s very common to move data directly into functions – think of all those fancy shaders you see everywhere, especially on shadertoy. As soon as I see a data constant in my code, I think “Wait; isn’t there a way to remove that from the function and have access to it as an input?”

This is important, and that’s the direction I’ll take from now on for the future versions of my frameworks.

What went right!

A lot as well!

Hot reloading

Hot reloading was the thing I needed. A hot-reload everything. I even hot-reload the tessellation of the objects (.obj), so that I can change the shape / resolution of a native object and I don’t have to relaunch the application. I saved a lot of precious time thanks to that feature.

Live edition in JSON

I had that idea pretty quickly as well. A lot of objects – among splines – live in JSON files. You edit the file, save it and tada: the object has changed in the application – hot reloading! The JSON was especially neat to handle splines of positions, colors and masks – it went pretty bad and wrong with orientations, but I already told you that.


As said before, compositing was also a win, because I lifted the concept up to the Rust AST, enabling me to express interesting rendering pipeline just by using operators like *, + and some combinators of my own (like over).


Editing was done with a cascade of types and objects:

  • a Timeline holds several Tracks and Overlaps;
  • a Track holds several Cuts;
  • a Cut holds information about a Clip: when the cut starts and ends in the clip and when such a cut should be placed in the track;
  • a Clip contains code defining a part of the scene (Rust code, can’t live in JSON for obvious reasons;
  • an Overlap is a special object used to fold several nodes if several cuts are triggered at the same time; it’s used for transitions mostly;
  • alternatively, a TimelineManifest can be used to live-edit all of this (the JSON for the cuts has a string reference for the clip, and a map to actual code must be provided when folding the manifest into an object of type Timeline).

I think such a system is very neat and helped me a lot to remove naive conditions (like timed if-else if-else if-else if…-else nightmare). With that system, there’s only one test per frame to determine which cuts must be rendered (well, actually, one per track), and it’s all declarative. Kudos.

Resources loading was insanely fast

I thought I’d need some kind of loading bars, but everything loaded so quickly that I decided it’d be a wast of time. Even though I might end up modifying the way resources are loaded, I’m pretty happy with it.


Writing that demo in such a short period of time – I have a job, a social life, other things I enjoy, etc. – was such a challenge! But it was also the perfect project to stress-test my framework. I saw a lot of issues while building my demo with spectra and a lot of “woah, that’s actually pretty great doing this that way!”. I’ll have to enhance a few things, but I’ll always do that with a demo as a work-in-progress because I target pragmatism. As I released spectra on, I might end up writing another blog entry about it sooner or later, and even speak about it at a Rust meeting!

Keep the vibe!

by Dimitri Sabadie ( at April 20, 2017 10:18 AM

Michael Snoyman

Generalizing Type Signatures

In each of the following, which is the best version of the type signature (assume Monad m context)?

when :: Bool -> m () -> m ()
when :: Bool -> m a  -> m ()

mapM_ :: (a -> m ()) -> [a] -> m ()
mapM_ :: (a -> m b)  -> [a] -> m ()

runConduit :: ConduitM () Void m r -> m r
runConduit :: ConduitM i  o    m r -> m r

In each of these cases, the second, more generalized version of the signature can easily be provided, but the question is, should it be? I know of the following arguments:

Pro generalized:

  • Why would we artificially limit the generality of our functions?
  • Having to sprinkle a bunch of voids around is a code smell

Against generalized:

  • It can allow accidental bugs to slip in by unintentionally ignoring values
  • In some cases, the generalized version has worse performance

I don't think these points bring anything new to the table: it seems to me that these trade-offs are fairly well understood, even if not talked about explicitly often. The other thing I'd observe is that, ignoring the issue of performance, this is just a rehashing of the much more general argument of explicit vs implicit. We can all acknowledge that with liberal application of void and similar functions, it's always possible to rewrite code relying on the generalized version to use the specialized version. The question comes down to that annoying need for throwing in void.

How do we determine whether we should use generalized or specialized functions? I'm starting to follow this procedure:

  1. If there's a performance concern, let that take precedence. Having accidentally slower code due to a desire to make code shorter/more beautiful is a bad trade-off.
  2. If there's no performance issue (like with runConduit), it's a completely subjective decision. The facts I'd look for are examples of bugs people run into with the generalized version.

On the bug front, I think it's important to point out that, in my experience, the bugs are less likely to appear during initial code writing, but during code review and refactoring. When you write something like when foo getLine, you've probably gone through the thought process "I'm just trying to give the user a chance to hit <ENTER>, and I'm intentionally ignoring whatever the user entered." But during refactoring that may not be so obvious, and some ignored user input may be surpring. By contrast, when foo (void getLine) stands out more blatantly.

Finally, in comparing this to the general discussion of explicit vs implicit, I want to point out that there's no "one right answer" here. This falls into the same category of "do I define a typeclass/interface?", which is always a judgement call. You can give general guidelines, but I think we can all agree that both extremes:

  • Never define a typeclass for any purpose
  • Define every single function to be a member of a typeclass

Are ridiculous oversimplifications that we should not advocate. Same thing applies here: there are times when a generalized type signature makes sense, and times when it doesn't.


As an aside, if anyone is wondering where this random blog post came from, while working on a presentation on Conduit and Yesod, I revisited an issue from a few months ago about deprecating older type synonyms (PR now available), and was reminded of the ongoing debate around which of the following is the correct runConduit signature:

1: ConduitM ()   Void m r -> m r -- today
2: ConduitM i    o    m r -> m r -- most general
3: ConduitM Void Void m r -> m r -- standardize on Void
4: ConduitM ()   ()   m r -> m r -- standardize on unit

The current situation of () for input and Void for output has been around for a while, and originated with discussions around the conduit/pipes dichotomy. (And in fact, pipes today has the same split.) I'm not convinced that the split between input and output is a great thing, so the arguments in favor of each of these signatures seem to be:

  1. Backwards compatibility
  2. Generalize, avoiding any need for explicit conversion ever, and avoid the ()/Void debate entirely * Note that we won't really avoid the debate entirely, since other parts of conduit will still need to indicate "nothing upstream" or "nothing downstream"
  3. Most explicit about what we're doing: we guarantee that there will never be any real values yielded from upstream, or yielded downstream. You can look through the conduit codebase for usages of absurd to see this play out.
  4. More explicit, but less cognitive overhead of learning about Void.

I think for now I'm leaning towards (1), as backwards compat has been a big guiding principle for me, but the debate is still raging for me.

April 20, 2017 06:00 AM

April 18, 2017

Dominic Steinitz

Trouble with Tribbles


Tribbles originate from the planet Iota Geminorum IV and, according to Dr. McCoy, are born pregnant. No further details are given but we can follow Gurtin and MacCamy (1974) and perhaps recover some of what happens on the Enterprise.

Of course, age-dependent population models are of more than fictional use and can be applied, for example, to modelling the progression of Malaria in infected hosts. We roughly follow some of J. J. Thibodeaux and Schlittenhardt (2011) who themselves reference Belair, Mackey, and Mahaffy (1995).

Of interest to Haskellers are:

  • The use of the hmatrix package which now contains functions to solve tridiagonal systems used in this post. You will need to use HEAD until a new hackage / stackage release is made. My future plan is to use CUDA via accelerate and compare.

  • The use of dimensions in a medium-sized example. It would have been nice to have tried the units package but it seemed harder work to use and, as ever, “Time’s wingèd chariot” was the enemy.

The source for this post can be downloaded from github.

Age-Dependent Populations

McKendrick / von Foerster

McKendrick and von Foerster independently derived a model of age-dependent population growth.

Let n(a,t) be the density of females of age a at time t. The number of females between ages a and a + \delta a are thus n(a, t)\delta a. Assuming individuals are born at age 0, we have

\displaystyle   \frac{\partial}{\partial t}(n(a, t)\delta a) =  J(a, t) - J(a + \delta a, t) - \mu(a, t)n(a, t)\delta a

where \mu(a, t) is the death rate density and J(a, t) denotes the rate of entry to the cohort of age a. Dividing by \delta a we obtain

\displaystyle   \frac{\partial}{\partial t}n(a, t) =   - \frac{J(a + \delta a, t) - J(a, t)}{\delta a} - \mu(a, t)n(a, t)

which in the limit becomes

\displaystyle   \frac{\partial}{\partial t}n(a, t) =   - \frac{\partial J(a, t)}{\partial a} - \mu(a, t)n(a, t)

We can further assume that the rate of entry to a cohort is proportional to the density of individuals times a velocity of aging v(a, t).

\displaystyle   J(a, t) = n(a, t)v(a, t)

Occasionally there is some reason to assume that aging one year is different to experiencing one year but we further assume v = 1.

We thus obtain

\displaystyle   \frac{\partial n(a, t)}{\partial t} + \frac{\partial n(a, t)}{\partial a} =  - \mu(a, t)n(a, t)

Gurtin / MacCamy

To solve any PDE we need boundary and initial conditions. The number of births at time t is

\displaystyle   n(0, t) = \int_0^\infty n(a, t) m(a, N(t))\, \mathrm{d}a

where m is the natality aka birth-modulus and

\displaystyle   N(t) = \int_0^\infty n(a, t)\, \mathrm{d}a

and we further assume that the initial condition

\displaystyle   n(a, 0) = n_0(a)

for some given n_0.

Gurtin and MacCamy (1974) focus on the situation where

\displaystyle   m(a, N(t)) = \beta(N)e^{-\alpha a}

and we can also assume that the birth rate of Tribbles decreases exponentially with age and further that Tribbles can live forever. Gurtin and MacCamy (1974) then transform the PDE to obtain a pair of linked ODEs which can then be solved numerically.

Of course, we know what happens in the Enterprise and rather than continue with this example, let us turn our attention to the more serious subject of Malaria.


I realise now that I went a bit overboard with references. Hopefully they don’t interrupt the flow too much.

The World Health Organisation (WHO) estimated that in 2015 there were 214 million new cases of malaria resulting in 438,000 deaths (source: Wikipedia).

The lifecycle of the plasmodium parasite that causes malaria is extremely ingenious. J. J. Thibodeaux and Schlittenhardt (2011) model the human segment of the plasmodium lifecycle and further propose a way of determing an optimal treatment for an infected individual. Hall et al. (2013) also model the effect of an anti-malarial. Let us content ourselves with reproducing part of the paper by J. J. Thibodeaux and Schlittenhardt (2011).

At one part of its sojourn in humans, plasmodium infects erythrocytes aka red blood cells. These latter contain haemoglobin (aka hemoglobin). The process by which red blood cells are produced, Erythropoiesis, is modulated in a feedback loop by erythropoietin. The plasmodium parasite severely disrupts this process. Presumably the resulting loss of haemoglobin is one reason that an infected individual feels ill.

As can be seen in the overview by Torbett and Friedman (2009), the full feedback loop is complex. So as not to lose ourselves in the details and following J. J. Thibodeaux and Schlittenhardt (2011) and Belair, Mackey, and Mahaffy (1995), we consider a model with two compartments.

  • Precursors: prototype erythrocytes developing in the bone marrow with p(\mu, t) being the density of such cells of age \mu at time t.

  • Erythrocytes: mature red blood cells circulating in the blood with m(\mu, t) being the density of such cells of age \nu at time t.

\displaystyle   \begin{aligned}  \frac{\partial p(\mu, t)}{\partial t} + g(E(t))\frac{\partial p(\mu, t)}{\partial \mu} &=  \sigma(\mu, t, E(t))p(\mu, t) & 0 < \mu < \mu_F & & 0 < t < T \\  \frac{\partial m(\nu, t)}{\partial t} + \phantom{g(E(t))}\frac{\partial m(\nu, t)}{\partial \nu} &=  -\gamma(\nu, t, M(t))m(\nu, t) & 0 < \nu < \nu_F & &  0 < t < T  \end{aligned}

where \sigma(\mu, t, E(t)) is the birth rate of precursors and \gamma(\nu, t, M(t)) is the death rate of erythrocytes, g(E(t)) is the maturation rate of precursors and where

\displaystyle   M(t) = \int_0^{\nu_F} p(\nu, t) \,\mathrm{d}\nu

As boundary conditions, we have that the number of precursors maturing must equal the production of number of erythrocytes

\displaystyle   m(0, t) = g(E(t))p(\mu_F, t)

and the production of the of the number of precursors depends on the level of erythropoietin

\displaystyle   g(E(t))p(0, t) = \phi(t)E(t)

where \phi(t) is some proportionality function.

As initial conditions, we have

\displaystyle   \begin{aligned}  p(\mu, 0) &= p_0(\mu) \\  m(\nu, 0) &= m_0(\nu)  \end{aligned}

We can further model the erythropoietin dynamics as

\displaystyle   \frac{\mathrm{d}E(t)}{\mathrm{d}t} = f(M(t), t) - a_E(P(t))E(t)

where f is the feedback function from the kidneys and the decay rate, a_E depends on the total precursor population P(t) (Sawyer, Krantz, and Goldwasser (1987)) although this often is taken to be a constant and I would feel more comfortable with a more recent citation and where

\displaystyle   P(t) = \int_0^{\mu_F} p(\mu, t) \,\mathrm{d}\mu

As initial condition we have

\displaystyle   E(0) = E_0

A Finite Difference Attempt

Let us try solving the above model using a finite difference scheme observing that we currently have no basis for whether it has a solution and whether the finite difference scheme approximates such a solution! We follow J. J. Thibodeaux and Schlittenhardt (2011) who give a proof of convergence presumably with some conditions; any failure of the scheme is entirely mine.

Divide up the age and time ranges, [0, \mu_F], [0, \nu_F] and [0, T] into equal sub-intervals, [\mu_i, \mu_{i+1}], [\nu_j, \nu_{j+1}] and [t_k, t_{k+1}] where

\displaystyle   \begin{aligned}  \mu_i &= i\Delta\mu & & \mathrm{for} & i = 1 \ldots n_1 \\  \nu_j &= j\Delta\nu & & \mathrm{for} & j = 1 \ldots n_2 \\  t_k   &= k\Delta t  & & \mathrm{for} & k = 1 \ldots K  \end{aligned}

where \Delta\mu = \mu_F / n_1, \Delta\nu = \nu_F / n_2 and \Delta t = T / K.

Denoting p(\mu_i, t_k) = p_i^k and similarly we obtain

\displaystyle   \begin{aligned}  \frac{p_i^{k+1} - p_i^k}{\Delta t} + g^k\frac{p_i^{k+1} - p_{i-1}^{k+1}}{\Delta\mu} &= \sigma_i^k p_i^{k+1} \\  \frac{m_j^{k+1} - m_j^k}{\Delta t} + \phantom{g^k}\frac{m_j^{k+1} - m_{j-1}^{k+1}}{\Delta\mu} &= -\gamma_j^k m_j^{k+1}  \end{aligned}


\displaystyle   \begin{aligned}  \frac{E^{k+1} - E^k}{\Delta t} &= f^k - a_E^k E^{k+1} \\  g^k p_0^{k+1} &= \phi^k E^k \\  m_0^{k+1}     &= g^k m_{n_1}^{k+1}  \end{aligned}

Re-arranging we get

\displaystyle   \begin{aligned}  -g^k\frac{\Delta t}{\Delta \mu}p_{i-1}^{k+1} +  \bigg(1 + g^k\frac{\Delta t}{\Delta \mu} - \Delta t \sigma_i^k\bigg)p_i^{k+1} &=  p_i^k \\  \frac{\Delta t}{\Delta \mu}m_{j-1}^{k+1} +  \bigg(1 + \frac{\Delta t}{\Delta \mu} + \Delta t \gamma_j^k\bigg)m_j^{k+1} &=  m_j^k  \end{aligned}


\displaystyle   \begin{aligned}  d_{1,i}^k &= 1 + g^k\frac{\Delta t}{\Delta \mu} - \Delta t \sigma_i^k \\  d_{2,i}^k &= 1 + \frac{\Delta t}{\Delta \nu} - \Delta t \gamma_i^k  \end{aligned}

We can express the above in matrix form

\displaystyle   \begin{bmatrix}  g^k & 0 & 0 & \ldots & 0 & 0 \\  -g^k\frac{\Delta t}{\Delta \mu} & d_{1,1}^k & 0 & \ldots & 0 & 0\\  0 & -g^k\frac{\Delta t}{\Delta \mu} & d_{1,2}^k & \ldots & 0 & 0 \\  \ldots & \ldots & \ldots & \ldots & \ldots & \ldots \\  0 & 0 & 0 & \ldots &\ -g^k\frac{\Delta t}{\Delta \mu} & d_{1,n_1}^k \\  \end{bmatrix}  \begin{bmatrix}  p_0^{k+1} \\  p_1^{k+1} \\  p_2^{k+1} \\  \ldots \\  p_{n_1}^{k+1}  \end{bmatrix}  =  \begin{bmatrix}  \phi^k E^k \\  p_1^k \\  p_2^k \\  \ldots \\  p_{n_1}^k \\  \end{bmatrix}

\displaystyle   \begin{bmatrix}  1 & 0 & 0 & \ldots & 0 & 0 \\  -\frac{\Delta t}{\Delta \mu} & d_{2,1}^k & 0 & \ldots & 0 & 0\\  0 & -\frac{\Delta t}{\Delta \mu} & d_{2,2}^k & \ldots & 0 & 0 \\  \ldots & \ldots & \ldots & \ldots & \ldots & \ldots \\  0 & 0 & 0 & \ldots &\ -\frac{\Delta t}{\Delta \mu} & d_{2,n_1}^k \\  \end{bmatrix}  \begin{bmatrix}  m_0^{k+1} \\  m_1^{k+1} \\  m_2^{k+1} \\  \ldots \\  m_{n_2}^{k+1}  \end{bmatrix}  =  \begin{bmatrix}  g^k p_{n_1}^{k+1} \\  m_1^k \\  m_2^k \\  \ldots \\  m_{n_1}^k \\  \end{bmatrix}

Finally we can write

\displaystyle   E^{k+1} = \frac{E^k + \Delta t f^k}{1 + a_E^k\Delta T}

A Haskell Implementation

> {-# OPTIONS_GHC -Wall #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE NoImplicitPrelude #-}
> {-# LANGUAGE FlexibleContexts #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeOperators #-}
> module Tribbles where
> import qualified Prelude as P
> import Numeric.Units.Dimensional.Prelude hiding (Unit)
> import Numeric.Units.Dimensional
> import Numeric.LinearAlgebra
> import Numeric.Integration.TanhSinh
> import Control.Monad.Writer
> import Control.Monad.Loops

Substances like erythropoietin (EPO) are measured in International Units and these cannot be converted to Moles (see Jelkmann (2009) for much more detail) so we have to pretend it really is measured in Moles as there seems to be no easy way to define what the dimensional package calls a base dimension. A typical amount for a person is 15 milli-IU / mill-litre but can reach much higher levels after loss of blood.

> muPerMl :: (Fractional a, Num a) => Unit 'NonMetric DConcentration a
> muPerMl = (milli mole) / (milli litre)
> bigE'0 :: Concentration Double
> bigE'0 = 15.0 *~ muPerMl

Let’s set up our grid. We take these from Ackleh et al. (2006) but note that J. J. Thibodeaux and Schlittenhardt (2011) seem to have T = 20.

> deltaT, deltaMu, deltaNu :: Time Double
> deltaT = 0.05 *~ day
> deltaMu = 0.01 *~ day
> deltaNu = 0.05 *~ day
> bigT :: Time Double
> bigT = 100.0 *~ day
> muF, nuF :: Time Double
> muF = 5.9 *~ day
> nuF = 120.0 *~ day
> bigK :: Int
> bigK = floor (bigT / deltaT /~ one)
> n1 :: Int
> n1 = floor (muF / deltaMu /~ one)
> n2 :: Int
> n2 = floor (nuF / deltaNu /~ one)
> ts :: [Time Double]
> ts = take bigK $ 0.0 *~ day : (map (+ deltaT) ts)

The birth rate for precursors

> betaThibodeaux :: Time Double ->
>                   Frequency Double
> betaThibodeaux mu
>   | mu < (0 *~ day) = error "betaThibodeaux: negative age"
>   | mu < (3 *~ day) = (2.773 *~ (one / day))
>   | otherwise       = (0.0 *~ (one /day))
> alphaThibodeaux :: Concentration Double ->
>                    Frequency Double
> alphaThibodeaux e = (0.5 *~ (muPerMl / day)) / ((1 *~ muPerMl) + e)
> sigmaThibodeaux :: Time Double ->
>                    Time Double ->
>                    Concentration Double ->
>                    Frequency Double
> sigmaThibodeaux mu _t e = gThibodeaux e * (betaThibodeaux mu - alphaThibodeaux e)

and an alternative birth rate

> betaAckleh :: Time Double -> Frequency Double
> betaAckleh mu
>   | mu < (0 *~ day) = error "betaAckleh: negative age"
>   | mu < (3 *~ day) = 2.773 *~ (one / day)
>   | otherwise       = 0.000 *~ (one / day)
> sigmaAckleh :: Time Double ->
>                Time Double ->
>                Concentration Double ->
>                Frequency Double
> sigmaAckleh mu _t e = betaAckleh mu * gAckleh e

J. J. Thibodeaux and Schlittenhardt (2011) give the maturation rate of precursors g as

> gThibodeaux :: Concentration Double  -> Dimensionless Double
> gThibodeaux e = d / n
>   where
>     n = ((3.02 *~ one) * e + (0.31 *~ muPerMl))
>     d = (30.61 *~ muPerMl) + e

and Ackleh et al. (2006) give this as

> gAckleh :: Concentration Double -> Dimensionless Double
> gAckleh _e = 1.0 *~ one

As in J. J. Thibodeaux and Schlittenhardt (2011) we give quantities in terms of cells per kilogram of body weight. Note that these really are moles on this occasion.

> type CellDensity = Quantity (DAmountOfSubstance / DTime / DMass)

Let’s set the initial conditions.

> p'0 :: Time Double -> CellDensity Double
> p'0 mu' = (1e11 *~ one) * pAux mu'
>   where
>     pAux mu
>       | mu < (0 *~ day) = error "p'0: negative age"
>       | mu < (3 *~ day) = 8.55e-6 *~ (mole / day / kilo gram) *
>                           exp ((2.7519 *~ (one / day)) * mu)
>       | otherwise       = 8.55e-6 *~ (mole / day / kilo gram) *
>                           exp (8.319 *~ one - (0.0211 *~ (one / day)) * mu)
> m_0 :: Time Double -> CellDensity Double
> m_0 nu' = (1e11 *~ one) * mAux nu'
>   where
>     mAux nu
>       | nu < (0 *~ day) = error "m_0: age less than zero"
>       | otherwise       = 0.039827  *~ (mole / day / kilo gram) *
>                           exp (((-0.0083) *~ (one / day)) * nu)

And check that these give plausible results.

> m_0Untyped :: Double -> Double
> m_0Untyped nu = m_0 (nu *~ day) /~ (mole / day / kilo gram)
> p'0Untyped :: Double -> Double
> p'0Untyped mu = p'0 (mu *~ day) /~ (mole / day / kilo gram)
ghci> import Numeric.Integration.TanhSinh
ghci> result $ relative 1e-6 $ parTrap m_0Untyped 0.001 (nuF /~ day)

ghci> result $ relative 1e-6 $ parTrap p'0Untyped 0.001 (muF /~ day)

We can now create the components for the first matrix equation.

> g'0 :: Dimensionless Double
> g'0 = gThibodeaux bigE'0
> d_1'0 :: Int -> Dimensionless Double
> d_1'0 i = (1 *~ one) + (g'0 * deltaT / deltaMu)
>           - deltaT * sigmaThibodeaux ((fromIntegral i *~ one) * deltaMu) undefined bigE'0
> lowers :: [Dimensionless Double]
> lowers = replicate n1 (negate $ g'0 * deltaT / deltaMu)
> diags :: [Dimensionless Double]
> diags = g'0 : map d_1'0 [1..n1]
> uppers :: [Dimensionless Double]
> uppers = replicate n1 (0.0 *~ one)

J. J. Thibodeaux and Schlittenhardt (2011) does not give a definition for \phi so we use the equivalent s_0 from Ackleh et al. (2006) which references Banks et al. (2003): “\times 10^{11} erythrocytes/kg body weight \times mL plasma/mU Epo/day”

> s_0 :: Time Double ->
>        Quantity (DAmountOfSubstance / DTime / DMass / DConcentration) Double
> s_0 = const ((1e11 *~ one) * (4.45e-7 *~ (mole / day / kilo gram / muPerMl)))
> b'0 :: [CellDensity Double]
> b'0 = (s_0 (0.0 *~ day) * bigE'0) : (take n1 $ map p'0 (iterate (+ deltaMu) deltaMu))

With these components in place we can now solve the implicit scheme and get the age distribution of precursors after one time step.

> p'1 :: Matrix Double
> p'1 = triDiagSolve (fromList (map (/~ one) lowers))
>                    (fromList (map (/~ one) diags))
>                    (fromList (map (/~ one) uppers))
>                    (((n1 P.+1 )><1) (map (/~ (mole / second / kilo gram)) b'0))

In order to create the components for the second matrix equation, we need the death rates of mature erythrocytes

> gammaThibodeaux :: Time Double ->
>                    Time Double ->
>                    Quantity (DAmountOfSubstance / DMass) Double ->
>                    Frequency Double
> gammaThibodeaux _nu _t _bigM = 0.0083 *~ (one / day)

We note an alternative for the death rate

> gammaAckleh :: Time Double ->
>                Time Double ->
>                Quantity (DAmountOfSubstance / DMass) Double ->
>                Frequency Double
> gammaAckleh _nu _t bigM = (0.01 *~ (kilo gram / mole / day)) * bigM + 0.0001 *~ (one / day)

For the intial mature erythrocyte population we can either use the integral of the initial distribution

> bigM'0 :: Quantity (DAmountOfSubstance / DMass) Double
> bigM'0 = r *~ (mole / kilo gram)
>  where
>    r = result $ relative 1e-6 $ parTrap m_0Untyped 0.001 (nuF /~ day)
ghci> bigM'0
  3.0260736659043414e11 kg^-1 mol

or we can use the sum of the values used in the finite difference approximation

> bigM'0' :: Quantity (DAmountOfSubstance / DMass) Double
> bigM'0' = (* deltaNu) $ sum $ map m_0 $ take n2 $ iterate (+ deltaNu) (0.0 *~ day)
ghci> bigM'0'
  3.026741454719976e11 kg^-1 mol

Finally we can create the components

> d_2'0 :: Int -> Dimensionless Double
> d_2'0 i = (1 *~ one) + (g'0 * deltaT / deltaNu)
>           + deltaT * gammaThibodeaux ((fromIntegral i *~ one) * deltaNu) undefined bigM'0
> lowers2 :: [Dimensionless Double]
> lowers2 = replicate n2 (negate $ deltaT / deltaNu)
> diags2 :: [Dimensionless Double]
> diags2 = (1.0 *~ one) : map d_2'0 [1..n2]
> uppers2 :: [Dimensionless Double]
> uppers2 = replicate n2 (0.0 *~ one)
> b_2'0 :: [CellDensity Double]
> b_2'0 = (g'0 * ((p'1 `atIndex` (n1,0)) *~ (mole / second / kilo gram))) :
>         (take n2 $ map m_0 (iterate (+ deltaNu) deltaNu))

and then solve the implicit scheme to get the distribution of mature erythrocytes one time step ahead

> m'1 :: Matrix Double
> m'1 = triDiagSolve (fromList (map (/~ one) lowers2))
>                    (fromList (map (/~ one) diags2))
>                    (fromList (map (/~ one) uppers2))
>                    (((n2 P.+ 1)><1) (map (/~ (mole / second / kilo gram)) b_2'0))

We need to complete the homeostatic loop by implmenting the feedback from the kidneys to the bone marrow. Ackleh and Thibodeaux (2013) and Ackleh et al. (2006) give f as

> fAckleh :: Time Double ->
>            Quantity (DAmountOfSubstance / DMass) Double ->
>            Quantity (DConcentration / DTime) Double
> fAckleh _t bigM = a / ((1.0 *~ one) + k * (bigM' ** r))
>   where
>     a = 15600 *~ (muPerMl / day)
>     k = 0.0382 *~ one
>     r = 6.96 *~ one
>     bigM' = ((bigM /~ (mole / kilo gram)) *~ one) * (1e-11 *~ one)

The much older Belair, Mackey, and Mahaffy (1995) gives f as

> fBelair :: Time Double ->
>            Quantity (DAmountOfSubstance / DMass) Double ->
>            Quantity (DConcentration / DTime) Double
> fBelair _t bigM = a / ((1.0 *~ one) + k * (bigM' ** r))
>   where
>     a = 6570 *~ (muPerMl / day)
>     k = 0.0382 *~ one
>     r = 6.96 *~ one
>     bigM' = ((bigM /~ (mole / kilo gram)) *~ one) * (1e-11 *~ one)

For the intial precursor population we can either use the integral of the initial distribution

result $ relative 1e-6 $ parTrap p'0Untyped 0.001 (muF /~ day)
> bigP'0 :: Quantity (DAmountOfSubstance / DMass) Double
> bigP'0 = r *~ (mole / kilo gram)
>  where
>    r = result $ relative 1e-6 $ parTrap p'0Untyped 0.001 (muF /~ day)
ghci> bigP'0
  1.0453999900927126e10 kg^-1 mol

or we can use the sum of the values used in the finite difference approximation

> bigP'0' :: Quantity (DAmountOfSubstance / DMass) Double
> bigP'0' = (* deltaMu) $ sum $ map p'0 $ take n1 $ iterate (+ deltaMu) (0.0 *~ day)
ghci> bigP'0'
  1.0438999930030743e10 kg^-1 mol

J. J. Thibodeaux and Schlittenhardt (2011) give the following for a_E

> a_E :: Quantity (DAmountOfSubstance / DMass) Double -> Frequency Double
> a_E bigP = ((n / d) /~ one) *~ (one / day)
>   where
>     n :: Dimensionless Double
>     n = bigP * (13.8 *~ (kilo gram / mole)) + 0.04 *~ one
>     d :: Dimensionless Double
>     d = (bigP /~ (mole / kilo gram)) *~ one + 0.08 *~ one

but from Ackleh et al. (2006)

The only biological basis for the latter is that the decay rate of erythropoietin should be an increasing function of the precursor population and this function remains in the range 0.50–6.65 \mathrm{days}^{-1}

and, given this is at variance with their given function, it may be safer to use their alternative of

> a_E' :: Quantity (DAmountOfSubstance / DMass) Double -> Frequency Double
> a_E' _bigP = 6.65 *~ (one / day)

We now further calculate the concentration of EPO one time step ahead.

> f'0 :: Quantity (DConcentration / DTime) Double
> f'0 = fAckleh undefined bigM'0
> bigE'1 :: Concentration Double
> bigE'1 = (bigE'0 + deltaT * f'0) / (1.0 *~ one + deltaT * a_E' bigP'0)

Having done this for one time step starting at t=0, it’s easy to generalize this to an arbitrary time step.

> d_1 :: Dimensionless Double ->
>        Concentration Double ->
>        Int ->
>        Dimensionless Double
> d_1 g e i = (1 *~ one) + (g * deltaT / deltaMu)
>           - deltaT * sigmaThibodeaux ((fromIntegral i *~ one) * deltaMu) undefined e
> d_2 :: Quantity (DAmountOfSubstance / DMass) Double ->
>        Int ->
>        Dimensionless Double
> d_2 bigM i = (1 *~ one) + deltaT / deltaNu
>            + deltaT * gammaThibodeaux ((fromIntegral i *~ one) * deltaNu) undefined bigM
> oneStepM :: (Matrix Double, Matrix Double, Concentration Double, Time Double) ->
>             Writer [(Quantity (DAmountOfSubstance / DMass) Double,
>                      Quantity (DAmountOfSubstance / DMass) Double,
>                      Concentration Double)]
>                    (Matrix Double, Matrix Double, Concentration Double, Time Double)
> oneStepM (psPrev, msPrev, ePrev, tPrev) = do
>   let
>     g  = gThibodeaux ePrev
>     ls = replicate n1 (negate $ g * deltaT / deltaMu)
>     ds = g : map (d_1 g ePrev)  [1..n1]
>     us = replicate n1 (0.0 *~ one)
>     b1'0 = (s_0 tPrev * ePrev) /~ (mole / second / kilo gram)
>     b1 = asColumn $ vjoin [scalar b1'0, subVector 1 n1 $ flatten psPrev]
>     psNew :: Matrix Double
>     psNew = triDiagSolve (fromList (map (/~ one) ls))
>                          (fromList (map (/~ one) ds))
>                          (fromList (map (/~ one) us))
>                          b1
>     ls2 = replicate n2 (negate $ deltaT / deltaNu)
>     bigM :: Quantity (DAmountOfSubstance / DMass) Double
>     bigM = (* deltaNu) $ ((sumElements msPrev) *~ (mole / kilo gram / second))
>     ds2 = (1.0 *~ one) : map (d_2 bigM) [1..n2]
>     us2 = replicate n2 (0.0 *~ one)
>     b2'0 = (g * (psNew `atIndex` (n1, 0) *~ (mole / second / kilo gram))) /~
>            (mole / second / kilo gram)
>     b2 = asColumn $ vjoin [scalar b2'0, subVector 1 n2 $ flatten msPrev]
>     msNew :: Matrix Double
>     msNew = triDiagSolve (fromList (map (/~ one) ls2))
>                          (fromList (map (/~ one) ds2))
>                          (fromList (map (/~ one) us2))
>                          b2
>     bigP :: Quantity (DAmountOfSubstance / DMass) Double
>     bigP = (* deltaMu) $ sumElements psPrev *~ (mole / kilo gram / second)
>     f :: Quantity (DConcentration / DTime) Double
>     f = fAckleh undefined bigM
>     eNew :: Concentration Double
>     eNew = (ePrev + deltaT * f) / (1.0 *~ one + deltaT * a_E' bigP)
>     tNew = tPrev + deltaT
>   tell [(bigP, bigM, ePrev)]
>   return (psNew, msNew, eNew, tNew)

We can now run the model for 100 days.

> ys :: [(Quantity (DAmountOfSubstance / DMass) Double,
>         Quantity (DAmountOfSubstance / DMass) Double,
>         Concentration Double)]
> ys = take 2000 $
>      snd $
>      runWriter $
>      iterateM_ oneStepM ((((n1 P.+1 )><1) (map (/~ (mole / second / kilo gram)) b'0)),
>                          (((n2 P.+ 1)><1) $ (map (/~ (mole / second / kilo gram)) b_2'0)),
>                          bigE'0,
>                          (0.0 *~ day))

And now we can plot what happens for a period of 100 days.


Ackleh, Azmy S., and Jeremy J. Thibodeaux. 2013. “A second-order finite difference approximation for a mathematical model of erythropoiesis.” Numerical Methods for Partial Differential Equations, no. November: n/a–n/a. doi:10.1002/num.21778.

Ackleh, Azmy S., Keng Deng, Kazufumi Ito, and Jeremy Thibodeaux. 2006. “A Structured Erythropoiesis Model with Nonlinear Cell Maturation Velocity and Hormone Decay Rate.” Mathematical Biosciences 204 (1): 21–48. doi:

Banks, H T, Cammey E Cole, Paul M Schlosser, and Hien T Tran. 2003. “Modeling and Optimal Regulation of Erythropoiesis Subject to Benzene Intoxication.”

Belair, Jacques, Michael C. Mackey, and Joseph M. Mahaffy. 1995. “Age-Structured and Two-Delay Models for Erythropoiesis.” Mathematical Biosciences 128 (1): 317–46. doi:

Gurtin, Morton E, and Richard C MacCamy. 1974. “Non-Linear Age-Dependent Population Dynamics.” Archive for Rational Mechanics and Analysis 54 (3). Springer: 281–300.

Hall, Adam J, Michael J Chappell, John AD Aston, and Stephen A Ward. 2013. “Pharmacokinetic Modelling of the Anti-Malarial Drug Artesunate and Its Active Metabolite Dihydroartemisinin.” Computer Methods and Programs in Biomedicine 112 (1). Elsevier: 1–15.

Jelkmann, Wolfgang. 2009. “Efficacy of Recombinant Erythropoietins: Is There Unity of International Units?” Nephrology Dialysis Transplantation 24 (5): 1366. doi:10.1093/ndt/gfp058.

Sawyer, Stephen T, SB Krantz, and E Goldwasser. 1987. “Binding and Receptor-Mediated Endocytosis of Erythropoietin in Friend Virus-Infected Erythroid Cells.” Journal of Biological Chemistry 262 (12). ASBMB: 5554–62.

Thibodeaux, Jeremy J., and Timothy P. Schlittenhardt. 2011. “Optimal Treatment Strategies for Malaria Infection.” Bulletin of Mathematical Biology 73 (11): 2791–2808. doi:10.1007/s11538-011-9650-8.

Torbett, Bruce E., and Jeffrey S. Friedman. 2009. “Erythropoiesis: An Overview.” In Erythropoietins, Erythropoietic Factors, and Erythropoiesis: Molecular, Cellular, Preclinical, and Clinical Biology, edited by Steven G. Elliott, Mary Ann Foote, and Graham Molineux, 3–18. Basel: Birkhäuser Basel. doi:10.1007/978-3-7643-8698-6_1.

by Dominic Steinitz at April 18, 2017 10:53 PM

April 16, 2017

Jasper Van der Jeugt

WebSockets 0.11


Today, I released version 0.11 of the Haskell websockets library. Minor changes include:

  • Support for IPv6 in the built-in server, client and tests (thanks to agentm).
  • Faster masking (thanks to Dmitry Ivanov).

But most importantly, this release adds support for the permessage-deflate extension as described in RFC 7692. A big thanks go out to Marcin Tolysz who first submitted patches for an implementation. Unfortunately, merging these patches turned out to be a rocky road.


After merging all these changes and improving upon them, I’m very happy that the library now passes the Autobahn Testsuite. This language-agnostic testsuite is very extensive and contains test cases covering most of the protocol surface.



When I started running this testsuite against the websockets library, it was very encouraging to learn that – apart from a few corner cases – it was already passing most of this testsuite without any additional work.

The majority of failing tests were caused by the problem that the Haskell websockets library was too lenient: it would accept invalid UTF-8 characters when reading the messages as a ByteString. The RFC, however, dictates that a server should immediately close the connection if the client sends invalid UTF-8.

This has now been rectified, but as an opt-in, in order not to break any existing applications using this library. For example, in order to enable the new compression and UTF-8 validation, you can use something like:

main :: IO ()
main = WS.runServerWith "" 9001 options application
    options = WS.defaultConnectionOptions
        { WS.connectionCompressionOptions =
            WS.PermessageDeflateCompression WS.defaultPermessageDeflate
        , WS.connectionStrictUnicode      = True

Note that if you are already decoding the incoming messages to Text values through the WebSocketsData interface, enabling connectionStrictUnicode should not add any additional overhead. On the other hand, if your application is a proxy which just takes the ByteStrings and sends them through, enabling UTF-8 validation will of course come at a price.

In a future release, permessage-deflate will be enabled by default.

Other things

I realise that this blog has been a little quiet lately. This is because (aside from work being busy) I’ve been involved in some other things:

  • I have been co-organising Summer of Haskell 2017. If you are a student, and you would like to make some money while contributing to the Haskell ecosystem this summer, please think about applying. If you are a (Haskell) project maintainer and you would like to mentor a student, please consider adding an idea for a proposal.

  • I am also co-organising ZuriHac 2017. It looks like this event will be the largest Haskell Hackathon ever, with over 250 participants. Unfortunately, the event is now full, but if you’re interested you can still register – we will add you to the waiting list. We’ve seen about 10% cancellations each year, so there is still a good chance of getting into the event.

  • Lastly, I have been playing the new Zelda game, which has of course been a blast.

by Jasper Van der Jeugt at April 16, 2017 12:00 AM

April 15, 2017

Don Stewart (dons)

Spring in the Air

I’m excited to announce I will be joining Facebook next month as part of the Infer team in London. Using FP and static analysis to find bugs across the Facebook estate.

by Don Stewart at April 15, 2017 01:57 PM

The Gentoo Haskell Team

GHC as a cross-compiler update


Gentoo’s dev-lang/ghc-8.2.1_rc1 supports both cross-building and cross-compiling modes! It’s useful for cross-compiling haskell software and initial porting of GHC itself on a new gentoo target.

Building a GHC crossompiler on Gentoo

Getting ${CTARGET}-ghc (crosscompiler) on Gentoo:

# # convenience variables:
# # Installing a target toolchain: gcc, glibc, binutils
crossdev ${CTARGET}
# # Installing ghc dependencies:
emerge-${CTARGET} -1 libffi ncurses gmp
# # adding 'ghc' symlink to cross-overlay:
ln -s path/to/haskell/overlay/dev-lang/ghc part/to/cross/overlay/cross-${CTARGET}/ghc
# # Building ghc crosscompiler:
emerge -1 cross-${CTARGET}/ghc
powerpc64-unknown-linux-gnu-ghc --info | grep Target
# ,("Target platform","powerpc64-unknown-linux")

Cross-building GHC on Gentoo

Cross-building ghc on ${CTARGET}:

# # convenience variables:
# # Installing a target toolchain: gcc, glibc, binutils
crossdev ${CTARGET}
# # Installing ghc dependencies:
emerge-${CTARGET} -1 libffi ncurses gmp
# # Cross-building ghc crosscompiler:
emerge-${CTARGET} --buildpkg -1 dev-lang/ghc
# # Now built packages can be used on a target to install
# # built ghc as: emerge --usepkg -1 dev-lang/ghc

Building a GHC crossompiler (generic)

That’s how you get a powerpc64 crosscompiler in a fresh git checkout:

$ ./configure --target=powerpc64-unknown-linux-gnu
$ cat mk/
# to speed things up
$ make -j$(nproc)
$ inplace/bin/ghc-stage1 --info | grep Target
,("Target platform","powerpc64-unknown-linux")


Below are details that have only historical (or backporting) value.

How did we get there?

Cross-compiling support in GHC is not a new thing. GHC wiki has a detailed section on how to build a crosscompiler. That works quite good. You can even target ghc at m68k: porting example.

What did not work so well is the attempt to install the result! In some places GHC build system tried to run ghc-pkg built for ${CBUILD}, in some places for ${CHOST}.

I never really tried to install a crosscompiler before. I think mostly because I was usually happy to make cross-compiler build at all: making GHC build for a rare target usually required a patch or two.

But one day I’ve decided to give full install a run. Original motivation was a bit unusual: I wanted to free space on my hard drive.

The build tree for GHC usually takes about 6-8GB. I had about 15 GHC source trees lying around. All in all it took about 10% of all space on my hard drive. Fixing make install would allow me to install only final result and get rid of all intermediate files.

I’ve decided to test make install code on Gentoo‘s dev-lang/ghc package as a proper package.

As a result a bunch of minor cleanups happened:

What works?

It allowed me to test various targets. Namely:

Target Bits Endianness Codegen
cross-aarch64-unknown-linux-gnu/ghc 64 LE LLVM
cross-alpha-unknown-linux-gnu/ghc 64 LE UNREG
cross-armv7a-unknown-linux-gnueabi/ghc 32 LE LLVM
cross-hppa-unknown-linux-gnu/ghc 32 BE UNREG
cross-m68k-unknown-linux-gnu/ghc 32 BE UNREG
cross-mips64-unknown-linux-gnu/ghc 32/64 BE UNREG
cross-powerpc64-unknown-linux-gnu/ghc 64 BE NCG
cross-powerpc64le-unknown-linux-gnu/ghc 64 LE NCG
cross-s390x-unknown-linux-gnu/ghc 64 BE UNREG
cross-sparc-unknown-linux-gnu/ghc 32 BE UNREG
cross-sparc64-unknown-linux-gnu/ghc 64 BE UNREG

I am running all of this on x86_64 (64-bit LE platform)

Quite a list! With help of qemu we can even test whether cross-compiler produces something that works:

$ cat hi.hs 
main = print "hello!"
$ powerpc64le-unknown-linux-gnu-ghc hi.hs -o hi.ppc64le
[1 of 1] Compiling Main             ( hi.hs, hi.o )
Linking hi.ppc64le ...
$ file hi.ppc64le 
hi.ppc64le: ELF 64-bit LSB executable, 64-bit PowerPC or cisco 7500, version 1 (SYSV), dynamically linked, interpreter /lib64/, for GNU/Linux 3.2.0, not stripped
$ qemu-ppc64le -L /usr/powerpc64le-unknown-linux-gnu/ ./hi.ppc64le 

Many qemu targets are slightly buggy and usually are very easy to fix!

A few recent examples:

  • epoll syscall is not wired properly on qemu-alpha: patch
  • CPU initialization code on qemu-s390x
  • thread creation fails on qemu-sparc32plus due to simple mmap() emulation bug
  • tcg on qemu-sparc64 crashes at runtime in static_code_gen_buffer()

Tweaking qemu is fun 🙂

by Sergei Trofimovich at April 15, 2017 11:05 AM

April 14, 2017

FP Complete

What pure functional programming is all about: Part 1

This is a technical post series about pure functional programming. The intended audience is general programmers who are familiar with closures and some functional programming.

We're going to be seeing how pure functional programming differs from regular "functional programming", in a significant way.

We're going to be looking at a little language theory, type theory, and implementation and practice of pure functional programming.

We'll look at correctness, architecture, and performance of pure programs.

We're going to look at code samples in C#, JavaScript and SQL. We're going to look at Haskell code. We're going to look at assembly language.

In closing we'll conclude that typed purely functional programming matters, and in a different way to what is meant by "functional programming".

Hold onto yer butts.

In this post

Firstly, we'll start with a pinch of theory, but not enough to bore you. We'll then look at how functional programming differs from "pure" functional programming. I'll establish what we mean by "side-effects". Finally, I'll try to motivate using pure languages from a correctness perspective.

Types and Functions

A function is a relation between terms. Every input term has exactly one output term. That's as simple as it gets.

In type theory, it's described in notation like this:

f : A → B

Inputs to f are the terms in type A, and outputs from f are the terms in type B. The type might be Integer and the terms might be all integers .., -2, -1, 0, 1, 2, ...

The type might be Character and the terms might be Homer, Marge, SideShowBob, FrankGrimes, InanimateCarbonRod, etc.

This is the core of functional programming, and without type theory, it's hard to even talk formally about the meaning of functional programs.

Get it? I thought so. We'll come back to this later.

Functional programming isn't

Functional programming as used generally by us as an industry tends to mean using first-class functions, closures that capture their environment properly, immutable data structures, trying to write code that doesn't have side-effects, and things like that.

That's perfectly reasonable, but it's distinct from pure functional programming. It's called "pure functional", because it has only functions as defined in the previous section. But why aren't there proper functions in the popular meaning of functional programming?

It's something of a misnomer that many popular languages use this term function. If you read the language specification for Scheme, you may notice that it uses the term procedure. Some procedures may implement functions like cosine, but not all procedures are functions, in fact most aren't. Any procedure can do cheeky arbitrary effects. But for the rest of popular languages, it's a misnomer we accept.

Let's look into why this is problematic in the next few sections.

Side-effects, mutation, etc.

What actually are side-effects, really? What's purity? I'll establish what I am going to mean in this series of blog posts. There are plenty of other working definitions.

These are some things you can do in source code:

  1. Mutate variables.
  2. Make side-effects (writing to standard output, connecting to a socket, etc.)
  3. Get the current time.

These are all things you cannot do in a pure function, because they're not explicit inputs into or explicit outputs of the function.

In C#, the expression DateTime.Now.TimeOfDay has type TimeSpan, it's not a function with inputs. If you put it in your program, you'll get the time since midnight when evaluating it. Why?

In contrast, these are side-effects that pure code can cause:

  1. Allocate lots of memory.
  2. Take lots of time.
  3. Loop forever.

But none of these things can be observed during evaluation of a pure functional language. There isn't a meaningful pure function that returns the current time, or the current memory use, and there usually isn't a function that asks if the program is currently in an infinite loop.

So I am going to use a meaning of purity like this: an effect is something implicit that you can observe during evaluation of your program.

Which languages are purely functional

So, a pure functional language is simply one in which a function cannot observe things besides its inputs. Given that, we can split the current crop of Pacman-complete languages up into pure and impure ones:

Pure languagesImpure languages

Haskell (we'll use Haskell in this series), PureScript and Idris are purely functional in this sense. You can't change variables. You can't observe time. You can't observe anything not constructed inside Haskell's language. Side effects like the machine getting hotter, swap space being used, etc. are not in Haskell's ability to care about. (But we'll explore how you can straight-forwardly interact with the real world to get this type of information safely in spite of this fact.)

We'll look at the theoretical and practical benefits of programming in a language that only has functions during this series.

Reasoning and function composition

In a pure language, every expression is pure. That means you can move things around without worrying about implicit dependencies. Function composition is a basic property that lets you take two functions and make a third out of them.

Calling back to the theory section above, you can readily understand what function composition is by its types. Lets say we have two functions, f : X → Y and g : Y → Z:

The functions f : X → Y and g : Y → Z can be composed, written f ∘ g, to yield a function which maps x in X to g(f(x)) in Z:

In JavaScript, f ∘ g is:

function(x){ return f(g(x)); }

In Haskell, f ∘ g is:

\x -> f (g x)

There's also an operator that provides this out of the box:

f . g

You can compare this notion of composition with shell scripting pipes:

sed 's/../../' | grep -v ^[0-9]+ | uniq | sort | ...

Each command takes an input and produces an output, and you compose them together with |.

We'll use this concept to study equational reasoning next.

A really simple example

Let's look at a really simple example of composition and reasoning about it in the following JavaScript code and its equivalent in Haskell:

> [1, 4, 9].map(Math.sqrt)
[1, 2, 3]
> [1, 4, 9].map(Math.sqrt).map(function(x){ return x + 1 });
[2, 3, 4]
> map sqrt [1,4,9]
> map (\x -> x + 1) (map sqrt [1,4,9])

There's a pattern forming here. It looks like this:
map second (map first xs)

The f and g variables represent any function you might use in their place.

Let's do equational reasoning

We know that map id ≣ id, that is, applying the identity function across a list yields the original list's value. What does that tell us? Mapping preserves the structure of a list. In JavaScript, this implies that, given id

var id = function(x){ return x; }

Then ≣ xs.

Map doesn't change the length or shape of the data structure.

By extension and careful reasoning, we can further observe that:

map second . map first    map (second . first)

In JavaScript, that's ≣{ return second(first(x)); })

For example, applying a function that adds 1 across a list, and then applying a function that takes the square root, is equivalent to applying a function across a list that does both things in one, i.e. adding one and taking the square root.

So you can refactor your code into the latter!

Actually, whether the refactor was a good idea or a bad idea depends on the code in question. It might perform better, because you put the first and the second function in one loop, instead of two separate loops (and two separate lists). On the other hand, the original code is probably easier to read. "Map this, map that ..."

You want the freedom to choose between the two, and to make transformations like this freely you need to be able to reason about your code.

But it doesn't work in JavaScript

Turning back to the JavaScript code, is this transformation really valid? As an exercise, construct in your head a definition of first and second which would violate this assumption.
→{ return second(first(x)); })

The answer is: no. Because JavaScript's functions are not mathematical functions, you can do anything in them. Imagine your colleague writes something like this:

var state = 0;
function first(i){ return state += i; }
function second(i){ return i `mod` state; }

You come along and refactor, only to find the following results:

> var state = 0;
  function first(i){ return state += i; }
  function second(i){ return i % state; }
[1, 3, 6, 0]
> var state = 0;
  function first(i){ return state += i; }
  function second(i){ return i % state; }
  [1,2,3,4].map(function(x){ return second(first(x)); })
[0, 0, 0, 0]

Looking at a really simple example, we see that basic equational reasoning, a fundamental "functional" idea, is not valid in JavaScript. Even something simple like this!

So we return back to the original section "Functional programming isn't", and why the fact that some procedures are functions doesn't get you the same reliable reasoning as when you can only define functions.

A benefit like being able to transform and reason about your code translates to practical pay-off because most people are changing their code every day, and trying to understand what their colleagues have written. This example is both something you might do in a real codebase and a super reduced down version of what horrors can happen in the large.


In this post I've laid down some terms and setup for follow up posts.

  • We've looked at what purity is and what it isn't.
  • We've looked at functions and function composition.
  • We've looked at how reasoning is easier if you only have functions. We'll circle back to this in coming posts when we get to more detailed reasoning and optimizations.

In the next post, we'll explore:

  • SQL as a pure language, which is a familiar language to almost everybody.
  • How pure languages deal with the real-world and doing side-effects, which are obviously practical things to do.
  • Evaluation vs execution, the generalization of pure vs impure languages.

After that, we'll explore the performance and declarative-code-writing benefits of pure functional languages in particular detail, looking at generated code, assembly, performance, etc.

April 14, 2017 05:44 PM

April 13, 2017

Functional Jobs

Senior Backend Engineer (Haskell) at Front Row Education (Full-time)


Senior Backend Engineer to join fast-growing education startup transforming the way 6.5+ million K-12 students learn Math, English, Social Studies and more.

What you tell your friends you do

“You know how teachers in public schools are always overworked and overstressed with 30 kids per classroom and never ending state tests? I make their lives possible and help their students make it pretty far in life”

What you really will be doing

Architect, design and develop new web applications, tools and distributed systems for the Front Row ecosystem in Haskell, Flow, PostgreSQL, Ansible and many others. You will get to work on your deliverable end-to-end, from the UX to the deployment logic

Mentor and support more junior developers in the organization

Create, improve and refine workflows and processes for delivering quality software on time and without incurring debt

Work closely with Front Row educators, product managers, customer support representatives and account executives to help the business move fast and efficiently through relentless automation.

How you will do this

You’re part of an agile, multidisciplinary team. You bring your own unique skill set to the table and collaborate with others to accomplish your team’s goals.

You prioritize your work with the team and its product owner, weighing both the business and technical value of each task.

You experiment, test, try, fail and learn all the time

You don’t do things just because they were always done that way, you bring your experience and expertise with you and help the team make the best decisions

What have we worked on in the last quarter

We have rewritten our business logic to be decoupled from the Common Core math standards, supporting US state-specific standards and international math systems

Prototyped and tested a High School Math MVP product in classrooms

Changed assigning Math and English to a work queue metaphor across all products for conceptual product simplicity and consistency

Implemented a Selenium QA test suite 100% in Haskell

Released multiple open source libraries for generating automated unit test fixtures, integrating with AWS, parsing and visualizing Postgres logs and much more

Made numerous performance optimization passes on the system for supporting classrooms with weak Internet bandwidth


We’re an agile and lean small team of engineers, teachers and product people working on solving important problems in education. We hyper-focus on speeds, communication and prioritizing what matters to our millions of users.


  • You’re smart and can find a way to show us.
  • A track record of 5+ years of working in, or leading, teams that rapidly ship high quality web-based software that provides great value to users. Having done this at a startup a plus.
  • Awesome at a Functional Programming language: Haskell / Scala / Clojure / Erlang etc
  • Exceptional emotional intelligence and people skills
  • Organized and meticulous, but still able to focus on the big picture of the product
  • A ton of startup hustle: we're a fast-growing, VC-backed, Silicon Valley tech company that works hard to achieve the greatest impact we can.


  • Money, sweet
  • Medical, dental, vision
  • Incredible opportunity to grow, learn and build lifetime bonds with other passionate people who share your values
  • Food, catered lunch & dinner 4 days a week + snacks on snacks
  • Room for you to do things your way at our downtown San Francisco location right by the Powell Station BART, or you can work remotely from anywhere in the US, if that’s how you roll
  • Awesome monthly team events + smaller get-togethers (board game nights, trivia, etc)

Get information on how to apply for this position.

April 13, 2017 08:56 PM

FP Complete

Hiring: Project Manager, Telecommute

FP Complete is an advanced software company specializing in sophisticated server applications performing complex computations. We are now hiring a project manager for an advanced engineering project in the cryptocurrency industry.

This is a fully remote/telecommute position, working with a globally distributed team, with the majority of engineers located around the European timezone. As the main coordinator of the engineering projects, you will work directly for our customer, coordinating engineering activities including their team, our team, and other vendors.

If you are interested in applying for this position, please send your CV or resume to


As project manager, you will be responsible for refining and implementing the development processes on an active project. Your typical tasks will include:

  • Defining development milestones
  • Gathering work estimates from engineers
  • Setting realistic deadlines for milestones
  • Tracking progress towards milestone completion
  • Communicating project status to management
  • Identifying and raising any red flags that may impact delivery
  • Identify components within the project requiring additional resources
  • Help identify gaps between business requirements, software specifications, and implementation

You will be working directly with and receiving instruction from the customer’s Director of Engineer, as well as their executive team.

While many tools and processes are in place currently, we are looking for a capable project manager to:

  • holistically review the current state of affairs
  • gather information on the state of engineering from engineers and engineering managers
  • coordinate with company management on improving milestone management, estimations, and planning

This is an opportunity to take a productive and energetic team and help greatly improve productivity. You will have significant influence on how the overall project is managed, and will be able to advise at a crucial juncture on tooling and process decisions.


  • 5+ years experience managing software projects
  • Experience with common project management and issue tracking tooling (e.g. JIRA, YouTrack)
  • Familiarity with common software development practices, including: source control management, Continuous Integration
  • Strong written and spoken English communication
  • Reliable internet connection
  • Ability to regularly communicate with team members from time zones spanning California to Tokyo

Nice to have

  • While we will consider candidates from all geographic locations, a Europe-centric time zone will provide the best ability to communicate with the engineers, and will be considered a plus
  • Understanding of cryptography or crypto-currencies
  • Experience working on academic or research projects
  • Experience working with a geographically distributed team
  • Functional programming familiarity

Why this position?

This position offers a unique opportunity to work in a cutting-edge problem domain (Cryptocurrency), with an accomplished team of advanced software engineers and researchers. You will be in a prime position to guide the team towards modern best practices in project management.

This project consists of a diverse collection of engineering work, from user interface creation to advanced cryptography. In addition, the focus on correctness in software and the strong research-based design of the work is a relatively unique blend in today's software world.

In addition to your direct work on managing this project, you will have an opportunity to work with FP Complete's world-class engineering team, with our extensive experience in multiple domains.

If you are interested in applying for this position, please send your CV or resume to

April 13, 2017 03:00 PM

Gabriel Gonzalez

Use Dhall to configure Bash programs

<html xmlns=""><head> <meta content="text/html; charset=utf-8" http-equiv="Content-Type"/> <meta content="text/css" http-equiv="Content-Style-Type"/> <meta content="pandoc" name="generator"/> <style type="text/css">code{white-space: pre;}</style> <style type="text/css">div.sourceCode { overflow-x: auto; } table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode { margin: 0; padding: 0; vertical-align: baseline; border: none; } table.sourceCode { width: 100%; line-height: 100%; } td.lineNumbers { text-align: right; padding-right: 4px; padding-left: 4px; color: #aaaaaa; border-right: 1px solid #aaaaaa; } td.sourceCode { padding-left: 5px; } code > { color: #007020; font-weight: bold; } /* Keyword */ code > span.dt { color: #902000; } /* DataType */ code > span.dv { color: #40a070; } /* DecVal */ code > { color: #40a070; } /* BaseN */ code > span.fl { color: #40a070; } /* Float */ code > { color: #4070a0; } /* Char */ code > { color: #4070a0; } /* String */ code > { color: #60a0b0; font-style: italic; } /* Comment */ code > span.ot { color: #007020; } /* Other */ code > { color: #ff0000; font-weight: bold; } /* Alert */ code > span.fu { color: #06287e; } /* Function */ code > { color: #ff0000; font-weight: bold; } /* Error */ code > span.wa { color: #60a0b0; font-weight: bold; font-style: italic; } /* Warning */ code > { color: #880000; } /* Constant */ code > { color: #4070a0; } /* SpecialChar */ code > span.vs { color: #4070a0; } /* VerbatimString */ code > { color: #bb6688; } /* SpecialString */ code > { } /* Import */ code > { color: #19177c; } /* Variable */ code > { color: #007020; font-weight: bold; } /* ControlFlow */ code > span.op { color: #666666; } /* Operator */ code > span.bu { } /* BuiltIn */ code > span.ex { } /* Extension */ code > span.pp { color: #bc7a00; } /* Preprocessor */ code > { color: #7d9029; } /* Attribute */ code > { color: #ba2121; font-style: italic; } /* Documentation */ code > { color: #60a0b0; font-weight: bold; font-style: italic; } /* Annotation */ code > { color: #60a0b0; font-weight: bold; font-style: italic; } /* CommentVar */ code > { color: #60a0b0; font-weight: bold; font-style: italic; } /* Information */ </style></head><body>

Dhall is a non-Turing-complete programming language for configuration files, and if you are new to Dhall you might want to read the Dhall tutorial which explains how to use Dhall and several of the language features.

Dhall is currently adding support for new languages and file formats such as:

... and now Dhall supports Bash, too! I'm releasing the dhall-bash package which you can use to configure Bash programs using a strongly typed configuration language. This lets you carve out a typed subset of Bash in your scripts and share your configuration files with other languages that support Dhall.

This package provides a dhall-to-bash executable which can convert Dhall expressions to either Bash expressions or Bash variable declarations. For example, you can convert simple Dhall values like Text, Integers, Natural numbers, or Bools to Bash expressions, like this:

$ dhall-to-bash <<< '"ABC"'
$ dhall-to-bash <<< '2'
$ dhall-to-bash <<< '+2'
$ dhall-to-bash <<< 'True'

The output is a valid Bash expression which you can use directly or assign to a Bash variable, like this:

$ FOO=$(dhall-to-bash <<< '"ABC"')
$ echo "${FOO}"

You can convert more complex values like lists, records, and optional values into Bash statements by passing the --declare flag to dhall-to-bash:

$ dhall-to-bash --declare BAR <<< '{ name = "John Doe", age = +23 }'
declare -r -A BAR=([age]=23 [name]=$'John Doe')
$ dhall-to-bash --declare BAR <<< '[1, 2, 3]'
declare -r -A BAR=(1 2 3)
$ dhall-to-bash --declare BAR <<< '[] : Optional Natural'
unset BAR
$ dhall-to-bash --declare BAR <<< '[+2] : Optional Natural'
declare -r -i BAR=2

The --declare flag emits a valid Bash statement that you can pass to eval, like this:

$ eval $(dhall-to-bash --declare LIST <<< '[1, 2, 3]')
$ for i in "${LIST[@]}"; do echo "${i}"; done
$ eval $(dhall-to-bash --declare RECORD <<< '{ name = "John Doe", age = +23 }')
$ echo "Name: ${RECORD[name]}, Age: ${RECORD[age]}"
Name: John Doe, Age: 23

Code distribution

Dhall is also distributed programming language, meaning that you can reference code fragments by URL, like this:

$ dhall-to-bash --declare LIST
let replicate =
in replicate +10 Bool True
declare -r -a LIST=(true true true true true true true true true true)

The above example illustrates how Dhall's Prelude is distributed over IPFS (which is like a distributed hashtable for the web).

You can also reference local code by path, too, just like Bash:

$ echo '"John Doe"' > ./name
$ echo '+23' > ./age
$ echo '{ name = ./name , age = ./age }' > ./config
$ dhall-to-bash --declare CONFIG <<< './config'
declare -r -A CONFIG=([age]=23 [name]=$'John Doe')
$ eval $(dhall-to-bash --declare CONFIG <<< './config')
$ echo "${CONFIG[age]}"
$ dhall-to-bash <<< './config .age'


Dhall is also a typed language that never crashes, never throws exceptions, and never endlessly loops because a configuration file should never "break". Try to break the language if you don't believe me!

The strong type system also comes with user-friendly type errors that are concise by default:

$ dhall-to-bash --declare FOO
let replicate =
in replicate 10 Bool True

replicate : ∀(n : Natural) → ∀(a : Type) → ∀(x : a)List a

Error: Wrong type of function argument

replicate 10


... but they can go into much more detail if you ask:

$ dhall-to-bash --declare FOO --explain
let replicate =
in replicate 10 Bool True

replicate : ∀(n : Natural) → ∀(a : Type) → ∀(x : a)List a

Error: Wrong type of function argument

Explanation: Every function declares what type or kind of argument to accept

For example:

│ λ(x : Bool)x : Bool → Bool │ This anonymous function only accepts
└───────────────────────────────┘ arguments that have type ❰Bool❱

The function's input type

│ Natural/even : Natural → Bool │ This built-in function only accepts
└───────────────────────────────┘ arguments that have type ❰Natural❱

The function's input type

│ λ(a : Type)a : Type → Type │ This anonymous function only accepts
└───────────────────────────────┘ arguments that have kind ❰Type❱

The function's input kind

│ List : Type → Type │ This built-in function only accepts arguments that
└────────────────────┘ have kind ❰Type❱

The function's input kind

For example, the following expressions are valid:

(λ(x : Bool)x) True │ ❰True❱ has type ❰Bool❱, which matches the type
└────────────────────────┘ of argument that the anonymous function accepts

Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of
└─────────────────┘ argument that the ❰Natural/even❱ function accepts,

(λ(a : Type)a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind
└────────────────────────┘ of argument that the anonymous function accepts

List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument
└───────────┘ that that the ❰List❱ function accepts

However, you can not apply a function to the wrong type or kind of argument

For example, the following expressions are not valid:

(λ(x : Bool)x) "A" │ ❰"A"has type ❰Text❱, but the anonymous function
└───────────────────────┘ expects an argument that has type ❰Bool❱

Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
└──────────────────┘ expects an argument that has type ❰Natural❱

(λ(a : Type)a) True │ ❰True❱ has type ❰Bool❱, but the anonymous
└────────────────────────┘ function expects an argument of kind ❰Type❱

List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
└────────┘ argument that has kind ❰Type❱

You tried to invoke the following function:


... which expects an argument of type or kind:


... on the following argument:


... which has a different type or kind:


Some common reasons why you might get this error:

You omit a function argument by mistake:

List/head [1, 2, 3] │

List/head❱ is missing the first argument,
which should be: ❰Integer❱

You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱

Natural/even 2 │

This should be ❰+2❱


replicate 10


These detailed explanations provide miniature language tutorials that help new users pick up the language basics as they go.


If you would like to use this project you can install dhall-bash from Hackage:

... or you can check out the original project on Github, too:

I'll continue to work on adding new Dhall integrations to other languages and file formats. If you would like to contribute there are already two projects started by others to provide native Dhall support in Rust and Scala:

... and if you're feeling more adventurous you can contribute Dhall bindings to a new programming language!


by Gabriel Gonzalez ( at April 13, 2017 01:37 PM

April 12, 2017

Chris Smith

CodeWorld and Summer of Haskell 2017

TL;DR: CodeWorld is sponsoring two student slots for Summer of Haskell this year.  Please encourage any college students you know to apply to this program.
Attention college students!  Do you want to:
  • Work on a serious Haskell project this summer?
  • Work closely with experienced Haskell developers?
  • Earn a living stipend for doing it?
  • Help give educational opportunities to kids at the same time?
If so, please consider applying to Summer of Haskell this summer, and consider submitting a proposal to work on CodeWorld.  If you are not a student, please spread the word to students you know.

What is Summer of Haskell?

Details are at  The short version is: you submit a proposal to contribute to an open source project that benefits the Haskell community.  The community chooses the top submissions.  Those students are assigned a mentor to guide them in their project, and a living stipend for the summer.

How is CodeWorld related to Summer of Haskell?

Summer of Haskell is funded by donations, and CodeWorld has donated funds to support two students this summer to work on CodeWorld specifically (or on projects in the surrounding Haskell ecosystem, such as GHCJS, that would benefit CodeWorld).

How do I get started?

The student application period doesn’t start until April 25th.  That said, though, the time to get involved is now!  Student proposals are far more likely to be accepted if the student is knowledgeable about the project and surrounding community and ecosystem, and known within the community.  Some examples of ways to jump in are:
  • Subscribe to and follow the codeworld-discuss mailing list.
  • Work through CodeWorld’s online Guide with the link at
  • Experiment with GHCJS and other related tools.
  • Form some opinions about what would help the community.
  • Blog about your learning experiences, and start conversations on the mailing list.
  • Contribute in minor ways, such as improving documentation or taking on small bugs.

What should I propose?

This is up to you.  There’s a wiki page on the project github site with more details on possible proposals, at — but you don’t have to propose something on that list, but you definitely can.  The important things to keep in mind are:
  • Shoot for something feasible to complete in a summer, but also ambitious.
  • Making things better for existing users usually beats building something for a brand new audience.
  • Pick something you feel confident working on, and are excited about.  You’ll be thinking about it for a long time.
  • It’s a good idea to try to understand the existing community needs and opportunities, too!

Can I get feedback on my proposal?

Yes, absolutely!  Most successful proposals are improved with community feedback, so don’t try to do it all alone and surprise everyone at the end.  It’s up to you whether you feel more comfortable sharing your ideas on the mailing list, where you might get broader feedback, or one on one by email.

How much of a commitment is this?

The expectation is that students are making a commitment similar to a full-time job or internship for the entire work period, just shy of three months.

How do I apply?

Not so fast!  Applications are accepted starting on April 25th.  This is the time to start preparing, exploring the system, and considering your options! :)

by cdsmith at April 12, 2017 08:07 AM

April 11, 2017

Douglas M. Auclair (geophf)

March 2017 1HaskellADay 1Liners

  • March 30th, 2017:
    divide :: (a -> Either b c) -> [a] -> ([b], [c])  This function is somewhere easy to get to, right?
    via @fmapE 
    • @fmapE: divide f = foldr (either (first . (:)) (second . (:)) . f) ([], []) 
    • SocialJusticeCleric @walkstherain divide f = Data.Either.partitionEithers . fmap f
    • andrus @andrus divide f = foldMap $ (swap . pure . pure ||| pure . pure) . f
    • matt @themattchan divide = partitionEithers ... map where ... = (.).(.)
  • March 13th, 2017:
    Palindromes have nothing to do with today's #haskell problem of anagrams. So what.

    palindrome :: String -> Bool
    • SocialJusticeCleric @walkstherain all id . (zipWith (==) =<< reverse)
      • SocialJusticeCleric added: TIL Data.Foldable.and
    • bazzargh @bazzargh ap (==) reverse?
  • March 13th, 2017:
    type Bag a = Map a Int

    anagram :: Ord a => [a] -> [a] -> Bool
    anagram src = (== Bag.fromList src) . Bag.fromList

    Redefine with <*>
    • Denis Stoyanov @xgrommx why not?
      anagram = (==) `on` Bag.fromList

by geophf ( at April 11, 2017 11:32 PM

Manuel M T Chakravarty

April 10, 2017

Functional Jobs

Software Engineer at Haskell Lovers Stealth Co. (Full-time)

Very well-funded startup seeking experienced Haskellers who would also enjoy coding exclusively in Haskell. Experienced team working on an exciting product. Competitive compensation. Interested in chatting? Email eulerconstantine [at] gmail [dot] com

Get information on how to apply for this position.

April 10, 2017 10:06 PM

April 09, 2017

Derek Elkins

Djinn in your browser

I couldn’t find an online version of Djinn, so I ran it through GHCJS with some tweaks, added a basic interface and hosted it here. It runs in your browser, so go crazy. If you want changes to the default settings or environment, feel free to suggest them. Right now everything is the default settings of the Djinn tool except that multiple results is enabled.

April 09, 2017 12:35 PM

Sandy Maguire

Don't Eff It Up

<article> <header>

Don't Eff It Up


<time>April 9, 2017</time> foo, bar

Don’t Eff It Up

I gave a talk at BayHac titled “Don’t Eff It Up: Freer Monads in Action”. As promised, I’ve posted the slides online here. A huge thanks to everyone who attended!


April 09, 2017 12:00 AM

April 07, 2017

FP Complete

Your CI build process should be in your code repository

It's always been clear to developers that a project's source code and how to build that source code are inextricably linked. After all, we've been including Makefiles (and, more recently, declarative build specifications like pom.xml for Maven and stack.yaml for Haskell Stack) with our source code since time immemorial (well, 1976).

What has been less clear is that the build process and environment are also important, especially when using Continuous Integration. First-generation CI systems such as Jenkins CI and Bamboo have you use a web-based UI in order to set up the build variables, jobs, stages, and triggers. You set up an agent/slave running on a machine that has tools, system libraries, and other prerequisites installed (or just run the builds on the same machine as the CI system). When a new version of your software needs a change to its build pipeline, you log into the web UI and make that change. If you need a newer version of a system library or tool for your build, you SSH into the build agent and make the changes on the command line (or maybe you use a configuration management tool such as Chef or Ansible to help).

New generation CI systems such as Travis CI, AppVeyor, and Gitlab's integrated CI instead have you put as much of this information as possible in a file inside the repository (e.g. named .travis.yml or .gitlab-ci.yml). With the advent of convenient cloud VMs and containerization using Docker, each build job can specify a full OS image with the required prerequisites, and the services it needs to have running. Jobs are fully isolated from each other. When a new version of your software needs a change to its build pipeline, that change is made right alongside the source code. If you need a newer version of a system library or tool for your build, you just push a new Docker image and instruct the build to use it.

Tracking the build pipeline and environment alongside the source code rather than through a web UI has a number advantages:

  • If a new version of your software needs a different build pipeline, or needs a newer system tool installed in order to build, that change is right alongside the new version of the source code.

  • You can make changes to the build pipeline and environment in a feature branch, test them there without risk of interfering with other branches, and then a simple merge applies those changes to the master branch. No need to carefully coordinate merge timing with making manual changes to the build pipeline and environment.

  • Building old versions of your project "just works" without needing to worry that the changes you made to support a newer version break building the old version, since the old version will build using the pipeline and environment that was in place at the time it was tagged.

  • Developers can manage the build pipeline and environment themselves, rather than having to ask a CI administrator to make changes for them.

  • There is no need to manage what is installed on build agent machines except for the bare minimum to support the agent itself, since the vast majority of build requirements are included in an image instead of directly on the machine.

  • Developers can more easily build and test locally in an environment that is identical that used by CI by reusing images and build scripts (although "inlined" scripts in a .gitlab-ci.yml or .travis.yml are not usable directly on a developer workstation, so the CI metadata should reference scripts stored elsewhere in the repo). However, for thorough testing (rather than rapid iteration) in a real environment, developers will often prefer to just push to a branch and let the CI system take care of building and deploying instead (especially using review apps).

  • A history of changes to the CI configuration are retained, and it's easy to revert bad changes. Web based UIs may keep an audit log, but this is harder to deal with than a Git commit history of a text file.

  • You can include comments with the CI configuration, which web based UIs usually don't have room for aside from perhaps a "description" textarea which is nowhere near the actual bit of configuration that the comment applies to.

  • Making changes to machine-readable text files is less error prone than clicking around a web UI.

  • It's easier to move your project to a different CI server, since most of the CI configuration does not need to be re-created on the new server since it is in the code repo. With a web UI, you end up spending a lot of time clicking around trying to make the new server's job configuration look the same as the old server's, copying-and-pasting various bits of text, and it's easy to miss something.

There are also potential pitfalls to be aware of:

  • You need to consider whether any aspects of the build pipeline may change "externally" and should therefore not be inside the repo itself. For example, you might decide to migrate your Docker images to a different registry, in which case having the docker registry's hostname hard-coded in your repo would make it complicated to build older versions. It is best to using your CI system's facility to pass variables to a build for any such external values.

  • Similarly, credentials should never be hard coded in your repo, and should always be passed in as variables from your CI system.

Of course, nothing described here is entirely new. You could be judicious about having the a first generation CI system only make very simple call-outs to scripts in your repo, and those scripts could use VMs or chrooted environments themselves. In fact, these have been long considered best practices. Jenkins has plug-ins to integrate with any VM or containerization environment you can think of, as well as plugins to support in-repo pipelines. The difference is that the newer generation of CI systems make this way of operating the default rather than something you have to do extra work to achieve (albeit with a loss of some of the flexibility of the first generation tools).

CI has always been a important part of the FP Complete development and DevOps arsenal, and these principles are at the core of our approach regardless of which CI system is being used. We have considerable experience converting existing CI pipelines to these principles in both first-generation and newer generation CI systems, and we offer consulting and training.

April 07, 2017 04:00 PM

April 06, 2017

Neil Mitchell

HLint 2.0 - with YAML configuration

Summary: I've just released HLint 2.0, which lets you configure the rules with a YAML file.

I've just released HLint 2.0 to Hackage. HLint has always been configurable by writing a specially crafted Haskell file (e.g. to ignore certain hints or add new ones). With HLint 2.0 we now support YAML configuration files, and moreover encourage them over the Haskell format.

New Features of 2.0

Perhaps the most useful feature of this version is that HLint will search the current directory upwards for a .hlint.yaml file containing configuration settings. If a project includes a .hlint.yaml in the root then you won't need to pass it on the command line, and there's a reasonable chance any editor integration will pick it up as well. This idea was shamelessly stolen from Stylish Haskell.

HLint configuration files have also moved from Haskell syntax with special interpretation to YAML syntax. The Haskell syntax had become quite overloaded and was increasingly confused. The YAML syntax gives a fresh start with a chance to properly specify configuration directly rather than encoding it as Haskell expressions. The YAML configuration format enables a few features in this release, and going forward should enable more. To create a template .hlint.yaml file run hlint --default > .hlint.yaml. HLint continues to work without a configuration file.

In addition to a bunch of little hints, there is now a hint to suggest giving modules explicit export lists. I tend to always favour export lists, using module Foo(module Foo) where in the rare case they seem genuinely too much work. If you object to the hint, simply add to .hlint.yaml:

- ignore: {name: Use module export list}

On the other extreme, if you always want to require a complete and explicit export list (banning the trick above) do:

- warn: {name: Use explicit module export list}

Which enables the off-by-default hint requiring an explicit list. To see which off-by-default hints your program triggers pass the command line argument --show.

The biggest new hint is that you can now mark certain flags/extensions/imports/functions as being restricted - maintaining either a whitelist or blacklist and exceptions. As an example, HLint itself contains the restrictions:

- functions:
- {name: unsafeInterleaveIO, within: Parallel}
- {name: unsafePerformIO, within: [Util.exitMessageImpure, Test.Util.ref]}
- {name: unsafeCoerce, within: []}

These unsafe functions can only be used in the modules/functions listed (or nowhere for unsafeCoerce), ensuring no code sneaks in unexpectedly. As another example:

- flags:
- default: false
- {name: [-fno-warn-incomplete-patterns, -fno-warn-overlapping-patterns]}

Here we have used default: false to say that any flags not explicitly allowed cannot be used. If someone accidentally checks in development code with {-# OPTIONS_GHC -w #-} then HLint will catch it. This restriction feature is particularly designed for code reviews.

What Might Have Broken

This release changes a lot of stuff. I am aware the following will no longer work:

  • The HLint2 API has been deleted - I don't think anyone was using it (the HLint and HLint3 ones remain unchanged). I'll continue to evolve the API in future releases.
  • The Haskell configuration file no longer has a way of importing other configuration files. At the same time I made it so the default configuration file and internal hints are always included, which I hopefully offsets most of the impact of ignoring hint imports.
  • I may have broken some other things by accident, but that's why there is a bug tracker.

At the moment the Haskell and YAML configuration files are both supported. However, I'll be phasing out the Haskell configuration in the future, and encourage people to move to the YAML. The conversion should be pretty simple.

by Neil Mitchell ( at April 06, 2017 08:48 PM

Wolfgang Jeltsch

Grapefruit now compatible with GHC 7.10.3

It turned out that Grapefruit could not be built with GHC 7.10.3, apparently because of a bug in the compiler. Now a new version of Grapefruit, version, is out, which works around this problem.

Tagged: FRP, GHC, Grapefruit, Haskell

by Wolfgang Jeltsch at April 06, 2017 06:30 PM

Twan van Laarhoven

A type theory based on indexed equality - Implementation

In this post I would like to present the type theory I have been working on, where the usual equality is replaced by an equality type indexed by the homotopy interval. This results in ideas very similar to those from the cubical system. I have a prototype implementation of this system in Haskell, which you can find on github. The system is unimaginatively called TTIE, a type theory with indexed equality. In this post I will focus on the introducing the type system and its implementation. I save the technical details for another post.

To recap: I have previously written about the 'indexed equality' type. The idea is that if we have the homotopy interval type with two points and a path between them,

-- Pseudo Agda notation
data Interval : Type where
  0 : Interval
  1 : Interval
  01 : Eq _ 0 1

then we can then define a type of equality, 'indexed' by the interval:

data Eq (A : Interval  Type) : A 0  A 1  Type where
  refl : (x : (i : Interval)  A i)  Eq A (x 0) (x 1)

Rather than using lambdas all the time in the argument of Eq and refl, in TTIE I write the bound variable in a subscript. So refli (x i) means refl (\i x i) and Eqi (A i) x y means Eq (\i A i) x y. If we represent all paths with this indexed equality type, then we can actually take 01 = refli i.

Now the (dependent) eliminator for the interval is

iv :  {A}  {x : A 0}  {y : A 1}  (xy : Eqi (A i) x y)  (i : Interval)  A i
iv {A} {x} {y} xy 0 = x
iv {A} {x} {y} xy 1 = y
iv {A} {x} {y} (refli (xy i)) i = xy i
refli (iv {A} {x} {y} xy i) = xy

For readability, I write iv xy i as xyi. This combination already makes it possible to prove, for instance, congruence of functions without needing to use substitution (the J rule):

cong :  {A B x y}  (f : A  B)  Eqi A x y  Eqi B (f x) (f y)
cong f xy = refli (f xyi)

this can be generalized to dependent types

cong :  {A B x y}  (f : (x : A)  B x)  (xy : Eqi A x y)  Eqi (B xyi) (f x) (f y)
cong f xy = refli (f xyi)

And we also get extensionality up to eta equality:

ext :  {A B f g}  ((x : A)  Eqi (B x) (f x) (g x))  Eqi ((x : A)  B x) (\x  f x) (\x  g x)
ext fg = refli (\x  (fg x)i)

So far, however, we can not yet represent general substitution. I have found that the most convenient primitive is

cast : (A : I  Type)  (i : Interval)  (j : Interval)  A i  A j

where casti A 0 0 x = x and casti A 1 1 x = x.

This generalized cast makes all kinds of proofs really convenient. For instance, we would like that cast A 1 0 cast A 0 1 = id. But it is already the case that cast A 0 0 cast A 0 0 = id. So we just have to change some of those 0s to 1s,

lemma :  {A : Type} {x}  Eq _ (casti A 1 0 (casti A 0 1 x)) x
lemma {A} {x} = castj (Eq _ (casti A j 0 (casti A 0 j x)) x) 0 1 (refli x)

As another example, most type theories don't come with a built in dependent or indexed equalty type. Instead, a common approach is to take

Eqi (A i) x y = Eq (A 0) x (casti (A i) 1 0 y)


Eqi (A i) x y = Eq (A 1) (casti (A i) 0 1 x) y

We can prove that these are equivalent:

lemma' :  {A} {x y}  Eq Type (Eq (A 0) x (casti (A i) 1 0 y)) (Eqi (A i) x y)
lemma' {A} {x} {y} = reflj (Eqk (A (j && k)) x (casti (A i) 1 j y))

where i && j is the and operator on intervals, i.e.

_&&_ : Interval  Interval  Interval
0 && j = 0
1 && j = j
i && 0 = 0
i && 1 = i

We can even go one step further to derive the ultimate in substitution, the J axiom:

J :  {A : Type} {x : A}  (P : (y : A)  Eq A x y  Type)
   (y : A)  (xy : Eq A x y)  P x (refl x)  P y xy
J P y xy pxy = casti (P xyi (reflj (xy^(j && i)))) 0 1 pxy

With the TTIE implementation, you can type check the all of the above examples. The implementation comes with a REPL, where you can ask for types, evaluate expressions, and so on. Expressions and types can have holes, which will be inferred by unification, like in Agda.

On the other hand, this is by no means a complete programming language. For example, there are no inductive data types. You will instead have to work with product types (x , y : A * B) and sum types (value foo x : data {foo : A; bar : B}). See the readme for a full description of the syntax.

April 06, 2017 11:15 AM

April 05, 2017

Douglas M. Auclair (geophf)

March 2017 1HaskellADay Problems and Solutions

by geophf ( at April 05, 2017 08:59 PM

Brent Yorgey

Submit to the Workshop on Type-Driven Development!

This year I am the co-chair (with Sam Lindley) of the Workshop on Type-Driven Development, affectionately known as TyDe1.

The workshop will be co-located with ICFP in Oxford, and is devoted to the use of “static type information…used effectively in the development of computer programs”, construed broadly (see the CFP for more specific examples of what is in scope). Last year’s workshop drew a relativey large crowd and had a lot of really great papers and talks, and I expect this year to be no different! Andrew Kennedy (Facebook UK) will also be giving an invited keynote talk.

Please consider submitting something! We are looking for both full papers as well as two-page extended abstracts reporting work in progress. The submission deadline for regular papers is 24 May, and 7 June for extended abstracts.

  1. Which I think (though I am not certain) that we decided is pronounced like “tidy”.

by Brent at April 05, 2017 03:27 AM

April 04, 2017

wren gayle romano

LJ is no more

LiveJournal changed their TOS recently and, well, I didn't really feel like reading it to see what changed so instead I've deleted my old LJ account. All the folks I used to follow on LJ have since moved on to other venues or stopped blogging entirely, and I've been using DW as my main blog for quite some time now, so it was just a matter of time. In the event you were still following the old LJ account, now's the time to switch.

comment count unavailable comments

April 04, 2017 03:21 AM

April 03, 2017

Ken T Takusagawa

[cpsjxejd] Implementing Goodstein

The Goodstein function is one of the fastest growing computable functions.  As best as I can tell, it grows faster than the Ackermann function and faster than Conway's chained arrow notation.  It is fairly straightforward to implement -- implementation is where the rubber meets the road when a function claims to be computable: source code in Haskell here.

Some excerpts of code, first demonstrating converting to and from Hereditary Base notation:

-- curiously, these Terms may be reordered, i.e., commutative, which is different from normal base N notation which is place value.
type HerditaryBase = [Term];

-- value is Integer * base ^ HerditaryBase. base is given exogenously.
data Term = Term Integer HerditaryBase deriving Show;

-- wrap Base in newtype to defend against accidentally mixing it up with a coefficient
newtype Base = Base Integer deriving (Show, Enum); -- Enum needed for succ

-- output is little-endian
int_to_hb :: Base -> Integer -> HerditaryBase;
int_to_hb base x = zipWith Term (radix_convert base x) (map (int_to_hb base) [0..]);
-- [0..] are the list of exponents

hb_to_int :: Base -> HerditaryBase -> Integer;
hb_to_int base = map (term_to_int base) >>> sum;

term_to_int :: Base -> Term -> Integer;
term_to_int _ (Term 0 _) = 0; -- optimization
term_to_int (Base base) (Term k x) = k * base ^ (hb_to_int (Base base) x);

-- input must be zero or positive. output is little-endian.
radix_convert :: Base -> Integer -> [Integer];
radix_convert (Base base) = unfoldr $ \n -> if n==0 then Nothing else Just $ swap $ divMod n base;

-- Compute the next value in a Goodstein sequence
goodstein_tuple :: (Base, Integer) -> (Base, Integer);
goodstein_tuple (base, x) = (succ base , int_to_hb base x & hb_to_int (succ base) & subtract 1);

goodstein_sequence_from :: (Base, Integer) -> [Integer];
goodstein_sequence_from = iterate goodstein_tuple >>> map snd >>> takeWhile (>=0);

goodstein_sequence :: Integer -> [Integer];
goodstein_sequence x = (Base 2,x) & goodstein_sequence_from;

goodstein :: Integer -> Integer;
goodstein = goodstein_sequence >>> genericLength;

goodstein {0, 1, 2, 3} will complete within a reasonable amount of time.  4 and larger are huge so will not terminate within a reasonable amount of time.  (This unfortunately limits the testcases available for testing whether the implementation is correct.) The full source code also demonstrates computing the first 6 steps in hereditary base notation of the evaluation of goodstein 19 (Comparing with Wikipedia).

Harvey Friedman's tree and subcubic graph numbers supposedly grow faster, but they are difficult to understand, difficult to understand that they are computable, and consequently difficult to implement.

by Ken ( at April 03, 2017 09:29 PM

April 02, 2017

Mark Jason Dominus

/dev/null Follies

A Unix system administrator of my acquaintance once got curious about what people were putting into /dev/null. I think he also may have had some notion that it would contain secrets or other interesting material that people wanted thrown away. Both of these ideas are stupid, but what he did next was even more stupid: he decided to replace /dev/null with a plain file so that he could examine its contents.

The root filesystem quickly filled up and the admin had to be called back from dinner to fix it. But he found that he couldn't fix it: to create a Unix device file you use the mknod command, and its arguments are the major and minor device numbers of the device to create. Our friend didn't remember the correct minor device number. The ls -l command will tell you the numbers of a device file but he had removed /dev/null so he couldn't use that.

Having no other system of the same type with an intact device file to check, he was forced to restore /dev/null from the tape backups.

by Mark Dominus ( at April 02, 2017 02:38 PM

April 01, 2017

Michael Snoyman

Enough with Backwards Compatibility

To get things started correctly, I'd like to define backwards compatibility as the following:

Maintaining the invariant that, amongst successive versions of a library or tool, software using that library or tool continues to build and execute with matching semantics (though perhaps different performance characteristics).

There is some wiggle room for defining if a change is properly backwards compatible. If we introduce a new identifier which conflicts with an old one, this may break a build, but most people accept this as "backwards compatible enough." Also, fixing a bug in an implementation may, in some cases, break something. But let's ignore the subtle cases, and instead just focus on the big picture: I released some new library, and it changed the type signature of a function, tweaked a data type, or significantly altered runtime behavior.

Let's just cut to the chase: striving for backwards compatibility is stupid, and we should stop doing it. I'm going to demonstrate why.

It doesn't stop bugs

Let's take as an assumption that you're actually writing proper changelogs for your libraries (seriously, please write proper changelogs for your libraries). If so, there's no reason why backwards compatibility is useful for preventing bugs.

When you are using a library, you're responsible for keeping up to date with new versions. When a new version of any dependency comes out, it's your sworn duty and sacred obligation to thoroughly review the changelog and ensure that any changes that may affect you are addressed in your code. It's just the bare minimum of good code maintenance.

I'll leave as a given that everyone is using some version of Semantic Versioning (SemVer), so breaking changes will never accidentally affect their code bases.

It's time well spent!

This may sound like a lot of time invested on a maintainers part. While it certainly takes some effort, this is an investment in your future, not just an expenditure. Requiring this maintenance level from library authors is a great forcing function:

  • It proves you're serious about maintaining your code. When I'm choosing between different libraries for a task, the library with regular updates to address changes in dependencies is always the higher quality one.
  • Conversely, a lack of frequent updates tells you that you shouldn't trust a piece of code. Bitrot is no joke; code gets bad over time! Having something that forces you to change code regularly is the best way to avoid bitrot.
  • It properly penalizes you for using too many dependencies. Encouraging decreased dependencies is a great way to avoid dependency problems!

Failure cases

I want to take as a case example two well-known cases of well maintained backwards compatibility, and demonstrate how destructive it is.


Java is well known as an ecosystem that prefers stability over elegance, and we can see that this has led to a completely dead, non-viable platform. When generics were added to Java, they had the choice to either break their existing containers APIs, or add a brand new API. As we know, they made the foolish choice to introduce a brand new API, creating clutter (we hate clutter!).

But worse: it allowed old code to continue to run unmodified. How can we trust that that code is any good if no one has been forced to update it to newer APIs? They wasted a great opportunity for a quality forcing function on the entire ecosystem.


Once again seriously: sqlite3 is probably the most well designed C API I've ever seen, and by far the best low-level database API I've seen. Everything seems great with it.

But unfortunately, a few functions were misdesigned. For example, the sqlite3_prepare function was designed in such a way, leading to degraded error reporting behavior. To rectify this situation, the author made the (misguided) decision to introduce a new API, sqlite3_prepare_v2, with a different type signature, which allows for better error reporting. (You can read the details yourself.)

This allows existing programs to continue to compile and run unmodified, even allowing them to upgrade to newer sqlite3 versions to get performance and stability enhancements. What a disaster!

  • There's nothing forcing programmers to use the newer, better API
  • The API just looks ugly. Who in the world wants a _v2 suffix? Terrible!
  • Someone might accidentally use the old version of the function. Sure, it's well documented in the API docs to use the new one, but unlike changelogs, no one actually reads API docs. Even in a language like Haskell with a deprecation mechanism it wouldn't matter, since everyone just ignores warnings.

Obviously, the right decision was to create a new major version of sqlite (sqlite4), rename all of the functions, update the changelog, and force everyone to update their codebases. Why the author didn't see this is beyond me.

Dynamically typed languages

Let's say you go ahead and make a breaking change to a library in a dynamically typed language. Obviously all of your users should just read the changelog and update their code appropriately. There's no compiler to enforce things of course, so it's more likely that things will fail at runtime. That's fine, if you're using a dynamically typed language you deserve to have your code break.

Statically typed

The story with statically typed languages is—as always—better. There are two kinds of breaking changes we should discuss.

Changed type signature

Or more broadly: things that lead to a compiler error. I don't even understand why people talk about these. The compiler tells you exactly what you need to do. This is redundant information with the changelog! How dense can you be! Just try to compile your code and fix things. It couldn't be easier. I can't even right now.

Semantic change

Sometimes a function keeps its signature but changes its behavior, leading to code which will compile but behave differently. Sure, that's bad, but if you're too lazy to read the changelog and meticulously go through your codebase to see if you're affected in any way, you shouldn't be writing software.


I hope we can put this silly discussion to bed already. Break APIs! Not only does it lead to more beautiful libraries, but the forced breakage is good for the ecosystem. I hope the software engineering community can finally start to take responsibility for doing proper software maintenance.

April 01, 2017 06:00 AM

March 28, 2017

Joachim Breitner

Birthday greetings communication behaviour

Randall Munroe recently mapped how he communicated with his social circle. As I got older recently, I had an opportunity to create a similar statistics that shows how people close to me chose to fulfil their social obligations (given the current geographic circumstances):

Communication variants

Communication variants

(Diagram created with the xkcd-font and using these two stackoverflow answers.)

In related news: Heating 3½ US cups of water to a boil takes 7 minutes and 40 seconds on one particular gas stove, but only 3 minutes and 50 seconds with an electric kettle, despite the 110V-induced limitation to 1.5kW.

(Diagram updated on March 30, as the actual mail is slower than the other channels.)

by Joachim Breitner ( at March 28, 2017 05:42 PM

FP Complete

Hiring: Devops Engineers (San Diego, Portland, Telecommute)

FP Complete is an advanced software company specializing in sophisticated server side applications performing scientific data computation. Our toolchain includes cutting-edge devops paired with modern functional programming. We feature a globally distributed team of world-class software and devops engineers, work with customers ranging from startups to Fortune 500 companies, and work in such varied industries as finance, pharma, and econometrics.

We are currently seeking to fill two positions, one in San Diego, California, and one in Portland, Oregon. These positions will be geared towards customer-focused devops engineering to roll out new build, deploy, and monitoring infrastructure for a highly-available web application in the biotech industry.

We will also be accepting applications from other locations for an opening that we expect later this spring.


You will be tasked with working directly with the customer, understanding their requirements, and rolling out a solution incorporating the needs of both the software developers and the production runtime system. You will work with FP Complete engineers in designing and implementing solutions, but will be the primary point of contact for our customer.


  • AWS (EC2, VPC, IAM, RDS, ElastiCache)
  • Ubuntu server
  • Experience with managing high-availability systems
  • Shell scripting and automation of routine tasks
  • Strong organizational skills
  • Experience hosting SaaS systems

Nice to have

  • Azure or other IaaS
  • Postgres
  • Docker
  • Service Discovery and HA architectures
  • Intrusion detection/prevention
  • Terraform
  • Kubernetes

Additionally, as we are a functional programming shop, we are most interested in candidates who are intrigued by functional programming, as functional programming is a strong part of our engineering team culture.

If you are interested in applying for this position, please send your CV or resume to

Why FP Complete?

FP Complete has a strong engineering culture, focusing on using the best tools to do the job the right way. Our team has wide ranging skills and experience, leading to a great interaction amongst engineers. We are also members of the open source community, prolifically contributing to a number of open source projects. Specifically, with our maintenance of projects like Stackage and Stack, we are leaders in the open source Haskell ecosystem.

As a company, we provide many opportunities for engineering growth. Cross-training in separate fields—like functional programming—is encouraged, and we are very open to engineers learning more about project management. Both our customer and internal projects cover a wide range of problem domains and technologies, leading to many opportunities to expand your horizons.

Most of our team work from home on a regular basis. While these specific openings will require in-person interactions with customers, most of our projects offer significant flexibility in hours and location.

March 28, 2017 04:03 PM