Planet Haskell

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

Neil Mitchell

Code Review Reviewed

Summary: I used to be mildly against code review on all merges. Now I'm for it. Code review is a good idea for knowledge sharing, not spotting bugs.

For my open-source projects, I accept pull requests from external contributors which I review, but my contributions are probably not routinely looked at by anyone else. I suspect most non-huge open-source projects follow the same pattern. For larger projects code review seems more common, but far from ubiquitous.

Until recently, I was in favour of occasional code review, e.g. towards the end of a project taking a look at the code. The problem with that approach is that it is hard to find the right time - at the end there is little appetite for large-scale refactoring and when the project is busy cranking out code there is no time and the code is still changing. While I was a fan of this idea in theory, it never worked in practice.

Some teams use code review on every merge to master, perhaps several times per person per day. That's something I used to disagree with, but I asked some smart people, and their explanations changed my opinion. The important realisation was thinking about what code review is for.

  • Checking the code works: NO. Code review is not about checking the code works and is bug free. I have tests, and leverage the type system, which is meant to convince me and other readers that my code is correct. For certain very sensitive bits a second set of eyes checking for bugs may be useful, but if all your code is that sensitive it will also be bug-ridden. However, code review may spot the absence or inadequacy of tests.
  • Checking simple rules and conventions: NO. Often projects have rules about which packages/extensions can be used, tab width and line length etc. While these checks can be carried out by a human, they are much better automated. Even when "code reviewing" students work at York University (aka marking) it quickly became clear that I was wasting time on trivialities, and thus wrote HLint to automate it.
  • High-level design: A BIT. Code review should think about the high-level design (e.g. should this be a web server or command line tool), but often the code is too detailed to properly elucidate these choices. High-level design should usually be done on a bug tracker or whiteboard before writing code.
  • Mid-level design: YES. Code review is often very good at challenging details around the mid-level design - e.g. does the choice of Text vs ByteString make sense, is there some abstraction that needs introducing. The author of some code is often heavily influenced by the journey they took to get to some point, by seeing code without that history a reviewer can often suggest a better approach.
  • Spreading knowledge: YES. Code review is great for spreading knowledge of the code to others in the team. Code review requires the code to be written in such a way that someone else can understand it, and ensures that there is someone else who is familiar with it. For larger projects that's invaluable when someone goes on holiday.
  • Team cohesion: YES Code review requires different members of the team to share their work with each other, and to have an appreciation of what other people are working through and the challenges it presents. It's all too easy to declare a problem "easy" without understanding the details, and code review removes that temptation.
  • Training: YES. Code review is also good for teaching new techniques and approaches to the submitter. As an example, some problems are trivial to solve with a generics library, yet some programmers aren't familiar with any - code review helps with ongoing training.

In contrast, I think the disadvantages of code review all revolve around the time required:

  1. It takes other peoples time to do the review, when they could be doing something else.
  2. It takes the submitters time waiting for a review - often the next step is hard to do without the previous step being agreed. As a result, I think code review work should be prioritised.
  3. As a consequence of the two previous issues, code review changes the "unit of work", leading to more changes in a single bundle.

These issues are real, but I think the benefit of knowledge sharing alone outweighs the cost.

by Neil Mitchell ( at April 03, 2017 05:59 AM

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

March 25, 2017

Christopher Allen

A review of Learn Python the Hard Way, 3rd ed

As a break from usual, I thought I would review Zed Shaw’s Learn Python the Hard Way. I’ve had several beginners to programming ask me what they should use to learn and Shaw’s book frequently comes up. I’ve looked over his materials before when they were a free website but I wanted to see what the current published version was like.

A note from the reviewer

This review will be self-indulgent. I make copious comparisons with Haskell Programming from First Principles.

I write about and primarily use Haskell in my work now. I used Python for about 7 years of my 10 year career so I am comfortable with Python-the-language even if I don’t keep up with the community any longer.

My final conclusions and recommendation are at the bottom of this review!

Comparing the physical version of Learn Python the Hard Way with the ebook

Skip this section if you only want to hear about the content.

Learn Python the Hard Way's cover

I bought the physical version from Amazon and the ebook from Zed Shaw directly. Below you’ll see a picture of the physical copy I got.

Learn Python the Hard Way physical book binding

The margins in the layout are good enough. The main problem with the paper version is that it is a paperback with a typical perfect-bound binding. As a result, the book cannot stay open even on the 88th page depicted in the photo above. Page 88 of the print book was not at all the same content as the ebook. Page 88 in the print book was halfway through Exercise 25, titled “Even More Practice.” Page 88 in the ebook was in Exercise 17, titled “More Files.” Exercise 25 in the book was located at page 114. The ebook appears to use a slightly less compact layout than the print book, so the page difference will not necessarily be a fixed constant.

The content itself seemed identical, but there were some formatting differences. Here’s an example using the common student questions from Exercise 25:

Learn Python the Hard Way physical formatting

In the physical version, typewriter text is monospaced, bold, and slightly larger than the bolded text surrounding it.

Learn Python the Hard Way ebook formatting Learn Python the Hard Way ebook formatting

In the digital version, it’s monospaced but seemingly not bold. It’s also the same size as the surrounding text. The result is that the typewriter text is more visually apparent in the ebook version.

Table of contents

Learn Python the Hard Way ebook table of contents

The physical version’s table of contents is conventional and clear with a clean layout. The structuring in terms of chapter/exercise, section, and then sub-section makes more sense than what I’ve seen in some tech books. Often in Manning books you’ll see “units” encompassing multiple chapters that serve no useful purpose. The physical version of LPTHW transitions to backmatter after the 52nd exercise and some comments on learning.

Learn Python the Hard Way ebook table of contents

Unfortunately, the formatting of the table of contents is broken in the ebook version. There are 15 exercises in the appendix of the physical version, enumerated as 1 through 15. The ebook version counts up to 55.17 for the command-line content. The ebook stops abruptly at 55.17 and there’s nothing after that. The physical version includes an index at the end which the ebook does not have. I think this is because Zed’s indexing was done manually by humans but not incorporated into the source text he renders the ebook from. For the Haskell Book Julie and I have always indexed things in the original LaTeX source. As a result, the eventual print version of Haskell Programming from First Principles should have the same index as the final version of the ebook.

Content review starts here


Zed is right here about learning to code and the importance of instruction. I haven’t said much about it publicly before this, but his work on Learn Python the Hard Way heavily influenced my earliest approaches to pedagogy and how I thought about the Haskell Book. Much changed as Julie and I learned more about what worked with reviewers, but the basic principle of guiding learners through cumulative exercises is extremely important.

The Hard Way Is Easier

Zed starts by explaining and justifying the process of learning code by typing code in, making it work, and learning to pay attention to detail. It’s a minimalistic approach to teaching a programming language, but for learning to code it would be difficult for me to improve on this. The Haskell Book took a lot more pages (over 1,000 to LPTHW’s ~300) because we were trying to convey concepts that would have lasting value in addition to teaching people to code in Haskell. Readers should take this section seriously and strive to follow Zed’s directions here.

The Setup

Zed goes into more excruciating detail on getting things setup than even most books written for children. That’s not say it’s necessarily easy, but he’s working harder to smooth the way than most. In older versions of the book Zed would recommend gedit. In the print version he recommends TextWrangler for Mac users, Notepad++ for Windows users. The ebook recommends Atom for users of all operating systems which I think is sound advice even if I am an inveterate Emacs user.

For a sense of how much detail Zed goes into, he tells you multiple possible names for your terminal program, to add it to your dock, run it, and not to expect it to look like much.

This section is followed by how to find answers on the internet using Google, which most working programmers understand to be 80% of what they’re paid for. He even includes a screenshot of his example search and the results.

Warnings for Beginners

Zed warns against some common but faulty programmer advice. I largely agree with him but I think his reasons for doing this bear some explaining.

If a programmer tells you to use vim or emacs, just say ”no.” These editors are for when you are a better programmer.

Practice some charity and ignore the, “for when you are a better programmer” bit. There are two important reasons to take this and the rest of his advice seriously.

  1. You cannot conquer all things at once. My coauthor Julie essentially learned Linux, the terminal, Git, LaTeX, and Haskell all at once when she first joined me on Haskell Book. I do not recommend doing this. Load-balancing your stress levels is important when you are a beginner.

  2. Programmers are more frequently pathologically impulsive and self-centered than I have seen in any other profession. They are not thinking of your needs as a beginner if they tell you to learn Python 3 instead of Python 2. They’re just cheering for red team vs. blue team or whatever other interest they might have. This is not to say I think Zed’s necessarily right to teach Python 3 instead of 2. (I don’t care) My point is that ignoring what programmers tell you is often sound advice.

Exercise 1, A Good First Program

I do not plan to review every exercise. I’d like to go to bed at a reasonable hour tonight and I plan to allot myself only one evening to write this review. If only because I owe my dogs Papuchon and Jack some couch/TV time.

This exercise opens with a warning not to skip the front matter and methodological commentary. I can tell he has paid some attention to how people use the book based on this.

The first exercise code opens with a series of print statements. The lines are enumerated in the code block formatting of both versions of the book. The ebook has syntax highlighting, the print version does not. I can’t blame Zed for making the print version monochrome, I’ve priced what it costs to print a color version of the Haskell Book and it was horrifying.

The ebook version only shows a single screenshot of the code in the Atom text editor. The print version shows (monochrome, natch) pictures of the code in TextWrangler on Mac OS X and Notepad++ on Windows.

After the picture(s) of the code in a text editor, both versions of the book show you what running the program should print in a Mac or Windows terminal. These images seemed identical in both versions of the book. Main thing I noticed is that Zed needs to fix his terminal font and anti-aliasing, but I am petty and finicky about type.

Anticipating a common typographical error in the code, Zed points out where the error might’ve happened and what the error would look like. He also anticipates and informs the reader on how to correct a potential problem with ASCII encodings.

Exercise 1 is bookended by study drills and common questions asked by students. I was able to two of the three drills in Zed’s instructions. I’m not sure what Zed was asking for with the first study drill, which is a little worrying as beginners will be using this. I will assume it’s something obvious that I missed.

The common student questions occur at the end of the exercises throughout the book. They are intended to catch failure modes. Zed’s approach here is more modular than the Haskell Book. I think this works because the individual exercises are brief and typically last a handful of pages. In HPFFP we treated it more like a linear stream of consciousness and address anticipated problems in media res.

Exercise 2-5

Zed goes over basic syntactic elements like comments as well as expanding what the learner can do semantically by covering basic arithmetic operations and variables. The progression here seems more focused on minimizing the novelty of what is introduced syntactically rather than in what is introduced semantically. This is an important pedagogical distinction in the approaches taken by Zed’s book and by ours. We ordered the book based on conceptual dependence and difficulty, not on syntactic elements. Syntax didn’t count for nothing, but we believed it was the less difficult category than semantics. Our experience bore this out but I don’t think this invalidates Zed’s method. To give you an idea of what I mean, here’s a snippet of progressions of the code samples:

# Ex1
print "Hello World!"

Side note: In the ebook, the source code has unicode quotation marks. This means if the reader attempts to copy-pasta the code from the ebook, it’ll break. I’m not certain if it was intentional or if it’s like our case where we intentionally don’t fix things that would make copying and pasting easier. The potential problem with LPTHW here is that someone familiar with unicode might believe they’re actually meant to use the fancy quotes and get stuck. Zed doesn’t address it in his student questions section that I could find.

print "I could have code like this." # and the comment after is ignored
# Ex3
print "Hens", 25 + 30 / 6
# Ex4
average_passengers_per_car = passengers / cars_driven

print "There are", cars, "cars available."
# Ex5
my_eyes = ’Blue’
my_hair = ’Brown’

print "He’s got %s eyes and %s hair." % (my_eyes, my_hair)

This should illuminate somewhat how Zed is adding to the syntactic elements demonstrated in each example as the reader progresses. The common student questions continue to be a strong point of this book in the potential problems they address.

Exercises 6-12

I will get briefer here as Zed’s approach seems consistent and I mostly just want to touch on what the book covers.

Zed covers printing in more detail, escape sequences, string concatenation, and requesting manual user (terminal) input.

Exercises 13-17

These exercises cover getting user input from the arguments passed to the python invocation at the command-line, combining this with input prompts and reading and writing text files. Getting the length of a string is demonstrated. The code written is still in a scripty top-level style.

Exercise 18

This is where defining functions begins. Zed doesn’t stage out increasing complexity of function definition. Instead, the first function the reader sees will be one that has a gather parameter like so:

# the use of * with the args parameter is called a gather parameter
def print_two(*args):
    arg1, arg2 = args
    print ”arg1: %r, arg2: %r” % (arg1, arg2)

I did a search through the ebook PDF with Skim and as far as I can tell Zed never mentions what this is called so that readers could learn more about what it is or what it does. Zed could’ve showed the user how you can define a parameter-less function that can be invoked multiple times to save on repetition, but chose not to. Odder still, the gather parameter example is subsumed by a simple two parameter function and the first is called out as useless in the context of the example.

Exercises 19-23

Zed begins by demonstrating the definition of variables along with passing them to functions as arguments. Exercise 18 only demonstrated passing string to functions as arguments. The usual carefulness with progression resumes here. This is followed by using files with functions, functions that return a result, a vocabulary overview, and an exercise in reading code.

Exercise 23 seems careless. The exercise suggests reading whatever Python code you can find on Github, Bitbucket, or Gitorious. There’s no real attempt to point people towards things they could understand at that point in the book. I suspect most readers don’t get very far with this.

Exercises 24-26

This sub-sequence begins with practice in writing code from the book which synthesizes the elements you’ve seen so far. The study drills ask you to describe the elements of the code in a manner not dissimilar from the “parts of speech” you might’ve done in a language lesson. The help function in the REPL is touched upon.

This sub-sequence ends with a quiz where the objective is to fix broken code. I think it would have been better had this exercise been littered throughout the book so that the readers would have more practice doing so. Approaching this decision charitably, it could be said the readers had enough mistakes of their own to fix, but we chose to have many more exercises in our book.

Exercises 27-31

Boolean logic, truth tables, boolean operators, expressions using boolean operators, and equality. This includes expressions like:

”test” == ”test”
”test” == 1

Python isn’t typed so Zed doesn’t seem to comment upon and equality comparison of values unequal types.

Followed by if-else statements and guarding blocks of code with if-statements. The progression is a cumulative synthesis like before.

Exercises 32-34

Loops and lists begin here and is the title of the 32nd exercise. Appending onto lists, while loops, and indexing into lists are also covered.

Exercise 35

This sub-sequence opens with branches within functions. What branch refers to here is the multiple “branches” of code which may or may not execute based on an if statement. The first example combines parameter-less functions, if-else statements, variables, user input, converting an integer from a string, printing, aborting the program, functions calling other functions, an infinite while loop, and having an initial function to kick off a script.

The author doesn’t wrap the start function in the usual if __name__ == "__main__" pablum you see in most Python scripts. I suspect he’s bucking it on purpose since these programs are not intended to be imported by other Python programs.

Exercises 36-38

Debugging (the basic process, not a tool), a review of symbols and syntax, reading code, popping and appending to lists, getting the length of a list, splitting strings based on a character divider, and concatenating a list of lists are demonstrated.

Exercise 39

The construction and basic manipulation of Python dictionaries is demonstrated here. The style is imperative and evocative of how the code’s been written through the book so far. There has been no lurch into a functional style yet.

Exercises 40-42

Modules, classes, and objects begin here. Zed touches on Python being referred to as an object-oriented programming language. This is also where import is principally demonstrated.

My problem is that Object-Oriented Program- ming (OOP) is just plain weird.

The above quote demonstrates the effort Zed put in to explaining OOP.

Treating modules like dictionaries, invoking functions within modules like methods, accessing top-level variables in a module like a property, and using classes in all these same ways are covered.

Object oriented terms qua Python are briefly explained. Basic subtyping with a typical Animal/Species hierarchy is demonstrated.

Exercises 43-44

This sub-sequence opens with basic object-oriented analysis and design. This is where things get much wordier than they had been up to this point. The objective is to write a simple game engine. The wordiness wouldn’t be unusual in some other books, but there’s a lot of upfront conceptual mapping and the basic approach isn’t demonstrated or justified with any smaller examples. This would be less jarring if it occurred in almost any other book.

Eventually Zed has the reader write a bunch of stubbed out classes and empty methods to plan out the API. A bit like…defining types. Anyway, they look like this:

class Scene(object):
    def enter(self):

class Engine(object):
    def __init__(self, scene_map):
    def play(self):

There’s some commentary on top-down vs. bottom-up design. The mapped out API is correctly described as top-down. This is followed by a listing of all the code that fills in the empty methods and classes for the game engine project. The usual “what you should see” sections and study drills follow. The study drill suggests changing the game, asks you fix a bug he left in the code, asks you to explain a piece of code, adding cheat codes, adding a small combat system, and mentions that the game engine is an example a finite state machine. He suggests reading about finite state machines on the web even if it might not make sense. It’s a little amusing to see these small gestures tossed out when he made little to no effort to point readers to further resources or examples earlier in the book. I suspect this time was different because some of Zed Shaw’s open source work entailed extensive use of finite state machines and he has an affectation for them.

Later, inheritance versus composition are covered. Composition here is simple methods-invoking-other-methods. He strongly recommends against using multiple inheritance. Nothing too objectionable here.

Exercise 45

The reader is asked to make their own game like the space game that was just demonstrated. There’s a lot of commentary on code style and syntactic elements. There’s no attempt at ameliorating the blank-slate problem for beginners making a project from scratch.

Exercises 46-49

Project structure, automated testing with assertions, nosetests, exceptions (very briefly), basic text processing with a lexicon, and basic parsing are covered.

Note that the first time exceptions were called out by name was in the overview of symbols but he’s been using try off and on throughout the book.

Exercises 50-51

Making a basic web application with (a locked version named lpthw.web), getting input from a web browser (HTML forms), HTML templates, and automated tests for forms are demonstrated. As you might imagine, the explanations of what makes a web app tick are briefly but my coauthor and I are no less guilty of this. It’s a huge topic.

Exercise 52

The task in this exercise is to refactor the game from exercise 43 into a web application. This covers the basics of refactoring code and web sessions. The reader is expected to do most of the work this time, including figuring out how to make user authentication work.

This one seems like a leap based on how much handholding there had been in the book so far. I felt uncomfortable with the final project in our book because it expects the reader to learn TCP sockets on their own, but I think the lacuna was not so bad there.

Zed’s Commentary

The book includes two bits of commentary separating the 52nd exercise and the content that goes over the command line. One is called “Next Steps” has a couple subsections. The first subsection of “Next Steps” is an overview of how to go deeper with Python, particularly in specific domains like data analysis. I believe this is partly because Zed is trying to empower people whose principal “job” isn’t software itself but which might by augmented by knowing how to code. The second subsection is titled, “How to learn any programming language.” The advice he gives here is sound and I recommend following it if you are learning Haskell with our book or not.

Appendix A: Command Line Crash Course

These are the exercises sectioned under “55”. This is the content I noted had a very different presentation in the table of contents of the print and ebook variants of LPTHW. The sequence introduces individual command line applications and builds on them iteratively. Examples are given for Linux/OS X and Windows in each exercise. Learning basic file and directory manipulation is the priority of this appendix.

A note on Python 2 vs. 3

I’ve reviewed the third edition of this book which uses Python 2 throughout. The next, unreleased fourth edition of the book will be using Python 3. It shouldn’t be an impediment for a beginner to learn Python 2 using this book and then move on to using Python 3 afterward, but you should be aware of this.

At present if you go to the purchase page for the ebook on Zed Shaw’s website, it’ll say

Learn Python The Hard Way, 3rd/4th Edition For $29.99

I believe this means purchasers of the ebook will get the eventual fourth edition when it is released even if they’re just buying the third for now. The downloads in my account for Learn Python the Hard Way included videos and the PDF for the third edition only. If you are uncertain and care a great deal about this, please ask Zed himself to confirm.

My conclusions

I think this book is positively influenced by Zed’s background as a painter and musician. I believe he’s studied education as a domain as well and it shows in his work.

Overall, I recommend this book as an introduction to learning to code and to Python specifically for new or early programmers. Evaluating the book on what I believe to be Zed’s own goals, the main flaws are in the sudden leaps from meticulously explained code examples to quizzes that expect you to do independent research and implementation. There wasn’t much in the way of “intermediate” tasks in the code drills. There’s some half-hearted name-dropping, but there’s not much guidance for readers who want to learn more than what’s covered in the book. To draw a contrast, we name things for what they are in the Haskell Book and footnote many references in addition to recommending further reading at the end of each chapter.

Shifting to my own priorities, I’d say my main dissatisfaction with this book is that I wished there was a “follow-on” book which used a lot of the same methods for teaching people the semantics of Python. Zed has a “More Python” book in the works but I don’t know anything about it. The approach in Learn Python the Hard Way is very mechanical but it’s very monkey-see monkey-do. I realize this would’ve exploded the length of the book had it all been in one text. I wouldn’t wish the authoring of a 1,000+ page technical tome on any but my worst enemies.

Of the formats of the book available, I recommend getting the ebook directly from Zed for the ergonomics of working side by side with the book, your text editor, and a terminal. This is also how we recommend working through the Haskell Book, but we’re preparing a print version anyway. I only glanced at the videos that came with my purchase of the ebook. They seemed like a fairly straight forward walkthrough of the ebook. I don’t rate videos very highly in an educational context except to demonstrate basic things like workflow, but your mileage may vary.

I did not review the Kindle version of this book! If I had to guess, it was prepared from the print version by the print version’s publisher. As a result, I would not expect it to have the same content as the ebook directly from Zed Shaw. Further, I mostly wrote this review while reading the ebook because it was faster for me. There may be differences between the print and ebook versions I failed to note! I believe Zed continues to update the electronic version.

Click here to get the print version of Learn Python the Hard Way on Amazon. (Affiliate link)

Click here to get the ebook version of Learn Python the Hard Way from Zed. (No affiliate link)

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!

March 25, 2017 12:00 AM

March 24, 2017

Philip Wadler

Explained Visually

As the creators put it
Explained Visually (EV) is an experiment in making hard ideas intuitive inspired the work of Bret Victor's Explorable Explanations. Sign up to hear about the latest.
I've found their explanations of Markov Chains and Eigenvectors and Eigenvalues both cool and clear.

by Philip Wadler ( at March 24, 2017 02:45 PM

March 23, 2017

Edwin Brady

Type Driven Development with Idris

Type Driven Development with Idris, published by Manning, is now in print.

There’s a couple of free sample chapters, and an excerpt from Chapter 3 (including a discount code for 37% off the book) on interactive development in Atom.

by edwinb at March 23, 2017 06:49 PM

March 21, 2017

Edward Z. Yang

Proposal: Suggest explicit type application for Foldable length and friends

tl;dr If you use a Foldable function like length or null, where instance selection is solely determined by the input argument, you should make your code more robust by introducing an explicit type application specifying which instance you want. This isn't necessary for a function like fold, where the return type can cross-check if you've gotten it right or not. If you don't provide this type application, GHC should give a warning suggesting you annotate it explicitly, in much the same way it suggests adding explicit type signatures to top-level functions.

Recently, there has been some dust kicked up about Foldable instances causing "bad" code to compile. The prototypical example is this: you've written length (f x), where f is a function that returns a list [Int]. At some future point in time, a colleague refactors f to return (Warnings, [Int]). After the refactoring, will length (f x) continue to type check? Yes: length (f x) will always return 1, no matter how long the inner list is, because it is using the Foldable instance for (,) Warnings.

The solution proposed in the mailing list was to remove Foldable for Either, a cure which is, quite arguably, worse than the disease. But I think there is definitely merit to the complaint that the Foldable instances for tuples and Either enable you to write code that typechecks, but is totally wrong.

Richard Eisenberg described this problem as the tension between the goals of "if it compiles, it works!" (Haskell must exclude programs which don't work) and general, polymorphic code, which should be applicable in as many situations as possible. I think there is some more nuance here, however. Why is it that Functor polymorphic code never causes problems for being "too general", but Foldable does? We can construct an analogous situation: I've written fmap (+2) (f x), where f once again returns [Int]. When my colleague refactors f to return (Warnings, [Int]), fmap now makes use of the Functor instance (,) Warnings, but the code fails to compile anyway, because the type of (+1) doesn't line up with [Int]. Yes, we can still construct situations with fmap where code continues to work after a type change, but these cases are far more rare.

There is a clear difference between these two programs: the fmap program is redundant, in the sense that the type is constrained by both the input container, the function mapping over it, and the context which uses the result. Just as with error-correcting codes, redundancy allows us to detect when an error has occurred; when you reduce redundancy, errors become harder to detect. With length, the only constraint on the selected instance is the input argument; if you get it wrong, we have no way to tell.

Thus, the right thing to do is reintroduce redundancy where it is needed. Functions like fold and toList don't need extra redundancy, because they are cross-checked by the use of their return arguments. But functions like length and null (and arguably maximum, which only weakly constrains its argument to have an Ord instance) don't have any redundancy: we should introduce redundancy in these places!

Fortunately, with GHC 8.0 provides a very easy way of introducing this redundancy: an explicit type application. (This was also independently suggested by Faucelme.) In this regime, rather than write length (f x), you write length @[] (f x), saying that you wanted length for lists. If you wanted length for maps, you write length @(Map _) (f x). Now, if someone changes the type of f, you will get a type error since the explicit type application no longer matches.

Now, you can write this with your FTP code today. So there is just one more small change I propose we add to GHC: let users specify the type parameter of a function as "suggested to be explicit". At the call-site, if this function is used without giving a type application, GHC will emit a warning (which can be disabled with the usual mechanism) saying, "Hey, I'm using the function at this type, maybe you should add a type application." If you really want to suppress the warning, you could just type apply a type hole, e.g., length @_ (f x). As a minor refinement, you could also specify a "default" type argument, so that if we infer this argument, no warning gets emitted (this would let you use the list functions on lists without needing to explicitly specify type arguments).

That's it! No BC-breaking flag days, no poisoning functions, no getting rid of FTP, no dropping instances: just a new pragma, and an opt-in warning that will let people who want to avoid these bugs. It won't solve all Foldable bugs, but it should squash the most flagrant ones.

What do people think?

by Edward Z. Yang at March 21, 2017 11:50 PM

March 20, 2017

Functional Jobs

Remote Haskell backend engineer at Health eFilings (Full-time)

Our backend engineering team manages the ingestion and normalization of data sets, from data extraction through to product delivery. We want to work smarter instead of harder, and create domain specific languages, meta-programming etc. where possible.

Our current code base is written in Ruby and Coffee Script, but some new modules are being written in Haskell. You will be on the front lines of creating a Haskell-based infrastructure that is maintainable and can scale to support our needs as we grow.


You will have ownership of an entire module, including responsibility for:

  • Creating new features in a clean and maintainable way
  • Re-factoring existing code to ensure that we stay agile
  • Reviewing teammates’ code and providing feedback
  • Keeping yourself focused and your projects on track
  • An “I can run through walls” mentality to ensure that goals are met


  • Autonomy to solve problems in the way you best see fit
  • A manager who is accountable for ensuring you meet your professional goals
  • A team who helps each other and always strives to improve
  • The time to focus on creating the right solution, instead of the easiest one


  • Professional experience as a software engineer
  • Experience with Haskell
  • A desire for continual self-improvement
  • An understanding of best practices regarding maintainability and scalability
  • Must have US work authorization and be located in the US (we cannot sponsor visas at this time)
  • There are no formal education requirements for this position


  • Experience with data scraping and parsing


This is expected to be a remote position, although our Madison, Wisconsin office is also available as a work location.

Get information on how to apply for this position.

March 20, 2017 11:47 PM

Vincent Hanquez

Efficient CStruct

Dealing with complex C-structure-like data in haskell often force the developer to have to deal with C files, and create a system that is usually a tradeoff between efficiency, modularity and safety.

The Foreign class doesn’t quite cut it, external program needs C files, Binary parsers (binary, cereal) are not efficient or modular.

Let’s see if we can do better using the advanced haskell type system.

First let define a common like C structure that we will re-use to compare different methods:

struct example {
    uint64_t a;
    uint32_t b;
    union {
        uint64_t addr64;
        struct {
            uint32_t hi;
            uint32_t low;
        } addr32;
    } addr;
    uint8_t data[16];

Dealing with C structure

The offset of each field is defined as a displacement (in bytes) from the beginning of the structure to point at the beginning of the field memory representation. For example here we have:

  • a is at offset 0 (relative to the beginning of the structure)
  • b is at offset 8
  • addr.addr64 is at offset 12
  • addr.addr32.hi is at offset 12
  • addr.addr32.low is at offset 16
  • data is at offset 20

The size of primitives is simply the number of bits composing the type; so a uint64_t, composed of 64 bits is 8 bytes. Union is a special construction where the different option in the union are overlayed on each other and the biggest element define its size. The size of a struct is defined recursively as the sum of all its component.

  • field pointed by a is size 8
  • field pointed by b is of size 4
  • field pointed by addr is size 8
  • field pointed by data is size 16
  • the whole structure is size 36

What’s wrong with Foreign

Here’s the usual Foreign definition for something equivalent:

data Example = Example
    { a    :: {-# UNPACK #-} !Word64
    , b    :: {-# UNPACK #-} !Word32
    , u    :: {-# UNPACK #-} !Word64
    , data ::                !ByteString

peekBs p ofs len = ...

instance Foreign Example
    sizeof _ = 36
    alignment _ = 8
    peek p = Example <$> peek (castPtr p)
                     <*> peek (castPtr (p `plusPtr` 8))
                     <*> peek (castPtr (p `plusPtr` 12))
                     <*> peekBs p 20 16
    poke p _ = ...

Given a (valid) Ptr, we can now get element in this by creating a new Example type by calling peek. This will materalize a new haskell data structure in the haskell GC-managed memory which have a copy of all the fields from the Ptr.

In some cases, copying all this values on the haskell heap is wasteful and not efficient. A simple of this use case, would be to quickly iterate over a block of memory to check for a few fields values repeatedly in structure.

The Foreign type classes and co is only about moving data between the foreign boundary, it’s not really about efficiency dealing with this foreign boundary.

In short:

  • Materialize values on the haskell side
  • Not modular: whole type peeking/poking or nothing.
  • Size and alignment defined on values, not type.
  • No distinction between constant size types and variable size types.
  • Often passing undefined :: SomeType to sizeof and alignment.
  • Usually manually created, not typo-proof.

What about Binary parsers

There’s many binary parser on the market: binary , cereal, packer, store.

Most of a binary parser job is taking a stream of bytes and efficiently turning those bytes into haskell value. One added job is dealing with chunking, since you may not have all the memory for parsing, you need to deal with values that are cut between memory boundaries and have to deal with resumption.

Here’s an example of a binary parser for example:

getExample :: Get Example
getExample =
    Example <$> getWord64Host
            <*> getWord32Host
            <*> getWord64Host
            <*> getByteString 16

However, intuitively this has the exact same problem as Foreign, you can’t selectively and modularly deal with the data, and this create also full copy of the data on the haskell side. This is clearly warranted when dealing with memory that you want processed in chunks, since you can’t hold on to the data stream to refer to it later.

Defining a C structure in haskell

Dealing with memory directly is error prone and it would be nice to able to simulate C structures overlay on memory without having to deal with size, offset and composition manually and to remain as efficient as possible.

First we’re gonna need a recent GHC (at least 8.0) and the following extensions:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

Then the following imports:

import GHC.TypeLits
import Data.Type.Bool
import Data.Proxy
import Data.Int
import Data.Word

We define a simple ADT of all the possible elements that you can find, and their compositions:

data Element =
    | FWord8
    | FInt16
    | FWord16
    | FInt32
    | FWord32
    | FInt64
    | FWord64
    | FFloat
    | FDouble
    | FLong
    | FArray Nat Element          -- size of the element and type of element
    | FStruct [(Symbol, Element)] -- list of of field * type
    | FUnion [(Symbol, Element)]  -- list of field * type

now struct example can be represented with:

type Example = 'FStruct
    '[ '( "a"   , 'FWord64)
     , '( "b"   , 'FWord32)
     , '( "addr", 'FUnion '[ '( "addr64", 'FWord64)
                           , '( "addr32", 'FStruct '[ '( "hi", 'FWord32)
                                                    , '( "low", 'FWord32) ])
     , '( "data", 'FArray 16 'FWord8 )

Calculating sizes

Size is one of the key thing we need to be able to do on element.

Using a type family we can define the Size type which take an Element and returns a Nat representing the size of the element.

type family Size (t :: Element) where

This is very easy for our primitives types:

    Size ('FInt8)       = 1
    Size ('FWord8)      = 1
    Size ('FInt16)      = 2
    Size ('FWord16)     = 2
    Size ('FInt32)      = 4
    Size ('FWord32)     = 4
    Size ('FInt64)      = 8
    Size ('FWord64)     = 8
    Size ('FFloat)      = 4
    Size ('FDouble)     = 8
    Size ('FLong)       = 8 -- hardcoded for example sake, but would be dynamic in real code

The array is simply the Size of the element multiplied by the number of elements:

    Size ('FArray n el) = n * Size el

For the constructed elements, we need to define extra recursive type families. The structure is recursively defined to be the sum of its component Size, and the union is recursively defined as the biggest element in it,.

    Size ('FStruct ls)  = StructSize ls
    Size ('FUnion ls)   = UnionSize ls

type family StructSize (ls :: [(Symbol, Element)]) where
    StructSize '[]            = 0
    StructSize ('(_,l) ': ls) = Size l + StructSize ls

type family UnionSize (ls :: [(Symbol, Element)]) where
    UnionSize '[] = 0
    UnionSize ('(_,l) ': ls) = If (Size l <=? UnionSize ls) (UnionSize ls) (Size l)

Almost there, we only need a way to materialize the Size type, to have a value that we can use in our haskell code:

getSize :: forall el . KnownNat (Size el) => Integer
getSize = natVal (Proxy :: Proxy (Size el))

This looks a bit magic, so let’s decompose this to make clear what happens; first getSize is a constant Integer, it doesn’t have any parameters. Next the el type variable represent the type that we want to know the size of, and the contraint on el is that applying the Size type function, we have a KnownNat (Known Natural). In the body of the constant function we use natVal that takes a Proxy of a KnownNat to materialize the value.

Given this signature, despite being a constant value, getSize need to determine the element on which it is applied. We can use the Type Application to effectively force the el element to be what we want to resolve to:

> putStrLn $ show (getSize @Example)

Zooming with accessors

One first thing we need to have an accessor types to represent how we represent part of data structures. For example in C, given the struct example, we want to be able to do:


in a case of a structure or a union, we use the field name to dereference the structure, but in case of an array, we use an integral index. This is really straighforward:

data Access = Field Symbol | Index Nat

A List of Access would represent the zooming inside the data structures. The previous example can be written in haskell with:

    '[ 'Field "a" ]
    '[ 'Field "addr", 'Field "addr32", 'Field "hi" ]
    '[ 'Field "data", 'Index 3 ]
    '[ 'Field "data" ]

Calculating Offset

Offset of fields is the next important step to have full capabilities in this system

We define a type family for this that given an Element and [Access] would get back an offset in Nat. Note that due to the recurvise approach we add the offset ofs to start from.

type family Offset (ofs :: Nat) (accessors :: [Access]) (t :: Element) where

When the list of accessors is empty, we have reach the element, so we can just return the offset we have calculated

    Offset ofs '[]          t                = ofs

When we have a non empty list we call to each respective data structure with:

  • the current offset
  • the name of field searched or the index searched
  • either the dictionary of symbol to element (represented by '[(Symbol, Element)]) or the array size and inner Element
    Offset ofs ('Field f:fs) ('FStruct dict) = StructOffset ofs f fs dict
    Offset ofs ('Field f:fs) ('FUnion dict)  = UnionOffset ofs f fs dict
    Offset ofs ('Index i:fs) ('FArray n t)   = ArrayOffset ofs i fs n t

Being a type enforced definition, it also mean that with this you can mix up trying to Index into a Structure, or trying to dereference a Field into an Array. the type system will (too) emphatically complain.

Both the Structure and Union will recursely match in the dictionary of symbol to find a matching field. If we reach the empty list, we haven’t found the right field and the developper is notified with a friendly TypeError, at compilation time, that the field is not present in the structure.

Each time an field is skipped in the structure the size of the element being skipped, is added to the current offset.

type family StructOffset (ofs :: Nat)
                         (field :: Symbol)
                         (rs :: [Access])
                         (dict :: [(Symbol, Element)]) where
    StructOffset ofs field rs '[]                =
        TypeError ('Text "offset: field "
             ':<>: 'ShowType field
             ':<>: 'Text " not found in structure")
    StructOffset ofs field rs ('(field, t) ': _) = Offset ofs rs t
    StructOffset ofs field rs ('(_    , v) ': r) = StructOffset (ofs + Size v) field rs r

type family UnionOffset (ofs :: Nat)
                        (field :: Symbo)
                        (rs :: [Access])
                        (dict :: [(Symbol, Element)]) where
    UnionOffset ofs field rs '[]                 =
        TypeError ('Text "offset: field "
             ':<>: 'ShowType field
             ':<>: 'Text " not found in union")
    UnionOffset ofs field rs ('(field, t) ': _)  = Offset ofs rs t
    UnionOffset ofs field rs (_            : r)  = UnionOffset ofs field rs r

In the case of the array, we can just make sure, at compilation time, that the user is accessing a field that is within bounds, otherwise we also notify the developer with a friendly TypeError.

type family ArrayOffset (ofs :: Nat)
                        (idx :: Nat)
                        (rs :: [Access])
                        (n :: Nat)
                        (t :: Element) where
    ArrayOffset ofs idx rs n t =
        If (n <=? idx)
            (TypeError ('Text "out of bounds : index is "
                  ':<>: 'ShowType idx
                  ':<>: 'Text " but array of size "
                  ':<>: 'ShowType n))
            (Offset (ofs + (idx * Size t)) rs t)

A simple example of how the machinery works:

> Offset ofs '[ 'Field "data", 'Index 2 ]) Example
> StructOffset ofs "data" ['Index 2 ]
               '[ '("a", ..), '("b", ..) , '("addr", ..), '( "data", ..) ]
> StructOffset (ofs + Size 'Word64) "data" ['Index 2]
               '[ '("b", ..) , '("addr", ..), '( "data", ..) ]
> StructOffset (ofs + 8 + Size 'Word32) "data" ['Index 2]
               '[ '("addr", ..), '( "data", ..) ]
> StructOffset (ofs + 12 + Size ('Union ..)) "data" ['Index 2 ]
               '[ '( "data", 'Farray 16 'FWord8) ]
> Offset (ofs + 20) ['Index 3] ('FArray 16 'FWord8)
> Offset (ofs + 20 + 3 * Size 'FWord8) [] 'FWord8
> ofs + 23

Now we can just calculate Offset of accessors in structure, we just need something to use it.

getOffset :: forall el fields . (KnownNat (Offset 0 fields el)) => Integer
getOffset = natVal (Proxy :: Proxy (Offset 0 fields el))

Again same magic as getSize, and we also define a constant by construction. We also start counting the offset at 0 since we want to calculate absolute displacement, but we could start at some other points depending on need, and prevent a runtime addition if we were to know the starting offset at compilation for example.

> putStrLn $ show (getOffset @Example @('[])
> putStrLn $ show (getOffset @Example @('[ 'Field "a"]))
> putStrLn $ show (getOffset @Example @('[ 'Field "b"]))
> putStrLn $ show (getOffset @Example @('[ 'Field "addr, 'Index "addr32", 'Field "lo" "]))
> putStrLn $ show (getOffset @Example @('[ 'Field "data, 'Index 3 ]))


One nice aspect on this is that you can efficiently nest structure, and you can without a problem re-use the same field names for structure.

You can also define at compilation all sorts of different offsets and sizes that automatically recalculate given their structures, and combine together.

With this primitive machinery, it’s straighforward to define an efficient, safe, modular accessors (e.g. peek & poke) functions on top of this.


You can find the code:


  1. Packing & Padding

In all this code I consider the C structure packed, and not containing any padding. While the rules of alignment/padding could be added to the calculation types, I chose to ignore the issue since the developper can always from a packed structure definition, add the necessary padding explicitely in the definition. It would also be possible to define special padding types that automatically work out their size given how much padding is needed.

  1. Endianness

I completely ignore endianness for simplicity purpose, but a real library would likely and simply extend the definitions to add explicit endianness for all multi-bytes types.

  1. Nat and Integer

It would be nice to be able to generate offset in machine Int or Word, instead of unbounded Integer. Sadly the only capability for Nat is to generate Integer with natVal. The optimisation is probably marginal considering it’s just a constructor away, but it would prevent an unnecessary unwrapping and possibly even more efficient code.

March 20, 2017 12:00 AM

March 17, 2017

Edward Z. Yang

Prio: Private, Robust, and Scalable Computation of Aggregate Statistics

I want to take the opportunity to advertise some new work from a colleague of mine, Henry Corrigan-Gibbs (in collaboration with the venerable Dan Boneh) on the subject of preserving privacy when collecting aggregate statistics. Their new system is called Prio and will be appearing at this year's NSDI.

The basic problem they tackle is this: suppose you're Google and you want to collect some statistics on your users to compute some aggregate metrics, e.g., averages or a linear regression fit:


A big problem is how to collect this data without compromising the privacy of your users. To preserve privacy, you don't want to know the data of each of your individual users: you'd like to get this data in completely anonymous form, and only at the end of your collection period, get an aggregate statistic.

This is an old problem; there are a number of existing systems which achieve this goal with varying tradeoffs. Prio tackles one particularly tough problem in the world of private aggregate data collection: robustness in the face of malicious clients. Suppose that you are collecting data for a linear regression, and the inputs your clients send you are completely anonymous. A malicious client could send you a bad data point that could skew your entire data set; and since you never get to see the individual data points of your data set, you would never notice:


Thus, Prio looks at the problem of anonymously collecting data, while at the same time being able to validate that the data is reasonable.

The mechanism by which Prio does this is pretty cool, and so in this post, I want to explain the key insights of their protocol. Prio operates in a regime where a client secret shares their secret across a pool of servers which are assumed to be non-colluding; as long as at least one server is honest, nothing is revealed about the client's secret until the servers jointly agree to publish the aggregate statistic.

Here is the problem: given a secret share of some hidden value, how can we efficiently check if it is valid? To answer this question, we first have to explain a little bit about the world of secret sharing.

A secret sharing scheme allows you to split a secret into many pieces, so that the original secret cannot be recovered unless you have some subset of the pieces. There are amazingly simple constructions of secret sharing: suppose that your secret is the number x in some field (e.g., integers modulo some prime p), and you want to split it into n parts. Then, let the first n-1 shares be random numbers in the field, the last random number be x minus the sum of the previous shares. You reconstruct the secret by summing all the shares together. This scheme is information theoretically secure: with only n-1 of the shares, you have learned nothing about the underlying secret. Another interesting property of this secret sharing scheme is that it is homomorphic over addition. Let your shares of x and y be [x]_i and [y]_i: then [x]_i + [y]_i form secret shares of x + y, since addition in a field is commutative (so I can reassociate each of the pairwise sums into the sum for x, and the sum for y.)

Usually, designing a scheme with homomorphic addition is easy, but having a scheme that supports addition and multiplication simultaneously (so that you can compute interesting arithmetic circuits) is a bit more difficult. Suppose you want to compute an arithmetic circuit on some a secret shared value: additions are easy, but to perform a multiplication, most multiparty computation schemes (Prio uses Beaver's MPC protocol) require you to perform a round of communication:


While you can batch up multiplications on the same "level" of the circuit, so that you only to do as many rounds as the maximum depth of multiplications in the circuit, for large circuits, you may end up having to do quite a bit of communication. Henry tells me that fully homomorphic secret sharing has been the topic of some research ongoing research; for example, this paper about homomorphic secret sharing won best paper at CRYPTO last year.

Returning to Prio, recall that we had a secret share of the user provided input, and we would like to check if it is valid according to some arithmetic circuit. As we've seen above, we could try using a multi-party computation protocol to compute shares of the output of the circuit, reveal the output of the circuit: if it says that the input is valid, accept it. But this would require quite a few rounds of communication to actually do the computation!

Here is one of the key insights of Prio: we don't need the servers to compute the result of the circuit--an honest client can do this just fine--we just need them to verify that a computation of the circuit is valid. This can be done by having the client ship shares of all of the intermediate values on each of the wires of the circuit, having the servers recompute the multiplications on these shares, and then comparing the results with the intermediate values provided to us by the client:


When we transform the problem from a computation problem to a verification one, we now have an embarrassingly parallel verification circuit, which requires only a single round to multiply each of the intermediate nodes of the circuit.

There is only one final problem: how are we to check that the recomputed multiplies of the shares and the client provided intermediate values are consistent? We can't publish the intermediate values of the wire (that would leak information about the input!) We could build a bigger circuit to do the comparison and combine the results together, but this would require more rounds of communication.

To solve this problem, Prio adopts an elegant trick from Ben-Sasson'12 (Near-linear unconditionally-secure multiparty computation with a dishonest minority): rather than publish the entire all of the intermediate wires, treat them as polynomials and publish the evaluation of each polynomial at a random point. If the servers behave correctly, they reveal nothing about the original polynomials; furthermore, with high probability, if the original polynomials are not equal, then the evaluation of the polynomials at a random point will also be not equal.

This is all very wonderful, but I'd like to conclude with a cautionary tale: you have to be very careful about how you setup these polynomials. Here is the pitfall: suppose that a malicious server homomorphically modifies one of their shares of the input, e.g., by adding some delta. Because our secret shares are additive, adding a delta to one of the share causes the secret to also be modified by this delta! If the adversary can carry out the rest of the protocol with this modified share, when the protocol finishes running, he finds out whether or not the modified secret was valid. This leaks information about the input: if your validity test was "is the input 0 or 1", then if you (homomorphically) add one to the input and it is still valid, you know that it definitely was zero!

Fortunately, this problem can be fixed by randomizing the polynomials, so that even if the input share is shifted, the rest of the intermediate values that it computes cannot be shifted in the same way. The details are described in the section "Why randomize the polynomials?" I think this just goes to show how tricky the design of cryptographic systems can be!

In any case, if this has piqued your interest, go read the paper! If you're at MIT, you can also go see Henry give a seminar on the subject on March 22 at the MIT CSAIL Security Seminar.

by Edward Z. Yang at March 17, 2017 11:35 PM

March 14, 2017

Philip Wadler

Papers We Love: John Reynolds, Definitional Interpreters for Higher-Order Languages, now in Haskell

I suggested at Papers We Love that someone might like to recode John Reynolds's definitional interpeter, and I'm pleased to say that Rein Henrichs has done so.

by Philip Wadler ( at March 14, 2017 10:54 AM

March 13, 2017

Holden Karau

Strata San Jose 2017

I'm excited for Strata San Jose this week. I'll be giving two talks, on Wednesday Spark Structured Streaming for ML with Seth and on Thursday Debugging Apache Spark with Joey :) I'm also going to be back on theCUBE  just before the Thursday talk if anyone wants to watch the livestream of that.

I might also do un-official office hours if I find a good coffee shop near the venue (San Jose friends - where is good coffee?)

If you want to chat about Spark come find me or ping me :)

by Holden Karau ( at March 13, 2017 05:56 PM

Douglas M. Auclair (geophf)

January 2017 1HaskellADay 1Liners

  • January 31st, 2017:
    You have d = "3.461497957769017000D+07"
    define parseDouble :: String -> Double
    (n.b.: (read d) :: Double throws an error)
    • bazzargh @bazzargh uncurry (*) (bimap read ((10^).read.(dropWhile(`elem`"0+D"))) (break (=='D') d))::Double
  • January 31st, 2017: Given
    e :: FilePath -> [String] -> [Epoch]

    readEpochs :: FilePath -> IO [Epoch]
    readEpochs f = e f . lines <$> readFile f

    point-free-itize readEpochs
    • Astynax Pirogov @alex_pir uncurry fmap . (((. lines) . e) &&& readFile
  • January 30th, 2017: Given

    parseNum :: String -> Maybe (Float, String)

    define: dropNum'' :: String -> Maybe String

    points-free in terms of parseNum
    • matt @themattchan dropNum" = fmap snd . parseNum
  • January 30th, 2017: For

    parseHeader :: String -> Maybe String
    parseHeader str = match "Start " str <|> match "Finish " str

    eliminate redundancies
    • mconcat . ([match] <*> ["Start ", "Finish "] <*>) . pure
    • Nickolay Kudasov @crazy_fizruk If you're allowed to use Monoid instead of Alternative, how about this version?
      foldMap match ["Start", "Finish"]
    • Andreas Källberg @Anka213  My solution was
      parseHeader str = foldr1 (<|>) . map (`match` str) $ ["Start", "Finish"]
      But that's longer than the original.
  • January 25th, 2017:
    given f is type: f :: Int -> a -> Bool

    for: g :: a -> Bool
    g = (||) . f 2 <*> f 27

    rewrite g using f only once in the definition
    • Denis Stoyanov @xgrommx ugly version but
      (liftA2 . liftA2) (||) ($2) ($27) f
  • January 19th, 2017:
    import Data.Tree.Merkle

    mkleaf :: Show a => a -> Leaf a
    mkleaf = uncurry Leaf . (show . hashDatum &&& id)

    redefine using (<*>)
    • Denis Stoyanov @xgrommx smth like
      mkleaf = uncurry Leaf . show . (hashDatum <$> (,) <*> id)
      mkleaf = uncurry Leaf . show . (liftA2 (,) hashDatum id)
  • January 19th, 2017:
    mkbranch1 :: Leaf a -> Branch a
    mkbranch1 = uncurry Twig . (uncurry childrenHash . (dataHash &&& dataHash) &&& id)

    redefine using (<*>)s(?)

by geophf ( at March 13, 2017 03:32 PM

Ken T Takusagawa

[dwvcvceg] Colors

We explore the range of RGB colors (the sRGB gamut) projected into CIE L*a*b* (CIElab, Lab) color space, as implemented in the Haskell colour package.

The first image below is a slice of the CIE L*a*b* color solid through the plane L = 50, halfway between 0 (black) to 100 (white). The "a" and "b" coordinates have range ±128. The shape is slightly different from -- the bottom is slightly narrower than -- the image of the slice at L=50 on Wikipedia, so I wonder what is going on. It might be the choice of white point. We chose white_point=Data.Colour.CIE.Illuminant.d65 for everything in this discussion.

(Most of the images on this page have been scaled down with HTML. Right click and View Image to embiggen.)

cielab lightness 50

The inside of the cross section is kind of boring being mostly grayish, so in the image below we fill the cross section by connecting the origin (a=0, b=0) with line segments of the color at edge. We do this because we are mostly interested in the extent (outer edge) of the sRGB gamut in CIE L*a*b*. And it makes the pictures more striking.

cielab lightness 50

Finding the edge of the cross section, i.e., the last representable color still within the sRGB gamut, was an exercise in root finding.

Below are 13 other slices colored similarly. The lightness values are as follows.

  1. Lightness 16.149085003423885, halfway between black and the lightness of fully saturated blue.
  2. Lightness 32.29817000684777, the lightness of fully saturated blue.
  3. Lightness 42.767524268618665, halfway between blue and red.
  4. Lightness 53.23687853038956, the lightness of fully saturated red. We switch to a black background as colors approach white in order to better be able to see the edge of the shape.
  5. Lightness 56.779166162118884, halfway between red and magenta.
  6. Lightness 60.32145379384821, the lightness of fully saturated magenta.
  7. Lightness 74.02883222725823, halfway between magenta and green.
  8. Lightness 87.73621066066826, the lightness of fully saturated green.
  9. Lightness 89.42553101260378, halfway between green and cyan.
  10. Lightness 91.11485136453929, the lightness of fully saturated cyan.
  11. Lightness 94.12695165179927, halfway between cyan and yellow.
  12. Lightness 97.13905193905926, the lightness of fully saturated yellow.
  13. Lightness 98.56952596952962, halfway between yellow and white.

It might be fun to 3D print or or render the solid with 3D graphics someday. It seems to have a complicated shape. For 3D graphics, it would be most natural for the rendered color of the solid at each surface point to be the actual color of the solid, incorporating no reflected lights or shadows. However, such a lighting model will probably prevent the solid's sharp edges from being easily visible.

Above, we presented only 13 slices of the CIE L*a*b* color space. The first image below depicts the outer edge colors of 1024 slices. The vertical axis is lightness (L). The horizontal axis is the angle from the a-b origin. On my monitor, there are curious ridges corresponding to the saturated colors. I suspect it has to do with gamma.

However, the appeal of the CIE L*a*b* color space is perceptual uniformity; that is, perceptual differences in color can be calculated by Euclidean distance. The second image above has each row individually rescaled for perceptural uniformity. In other words, the horizontal axis is the proportion of the perimeter of cross section.

Marching along the perimeter of the cross section was another exercise in root finding. At each step, we seek the next point on the perimeter a constant distance away (and remember that finding any point on the perimeter itself requires root finding). Because we don't know the perimeter of a cross section in advance, we arbitrarily choose a small step size, achieving a set of points separated by that step size (except from the final point to initial point), then crudely rescale the those points into 1024 steps.

The image above on the right was the "magnum opus" of this project, taking days to compute. Here is a raw data file of the (a,b) coordinates of the perimeter at 1023 levels of lightness. Some combination of Implicit Differentiation and Automatic Differentiation might have computed this more efficiently.

We can take any row of this image to extract a band of uniform lightness and uniform rate of color change. Below on the top row is two copies of the band at L = 53.3203125, the lightness with the longest perimeter. This happens to be very close to the lightness of pure red. On the bottom row is the same band shifted 25 pixels. The color distance between the rows is roughly constant, so ideally there should be equally sharp contrast along the entire boundary. (But on my monitor this appears not to be the case: we will explore this more further below.)

We can sample this band at multiples of phi (the golden ratio) to get an infinite palette of colors widely spaced from each other, all at the same lightness.

Palette entries 0, 5, 8, 13 are similar because the Fibonacci sequence approximates the golden ratio.

For a fixed size palette, one can probably do slightly better by particle repulsion on the cross section itself, though I have not implemented this.

Next, abandon the constraint of equal lightness and instead focus on the saturated RGB colors. The outline of next image projects has only the saturated RGB colors projected orthogonally to the a-b plane. The edge colors are then radially connected to the origin as before. Someday, it might be fun to render this in 3D as a minimal surface.

saturated RGB colors projected to the a-b plane of the CIE Lab color space

I discovered that the appearance of the above image on my LCD display radically changes depending on the position of my head: the width of the colors changes. (CRTs I suspect do not have this problem.) The image below may better illustrate the effect. Move your head up and down (or left and right) and notice how (or if) the color sectors change in width. I especially notice it in the blues. Also, here is a webpage with the same circles tiling the background.

saturated RGB colors projected to the ab plane of the CIE Lab color space

The first image below shows the saturated colors scaled in distance for perceptual uniformity. The second image is without correction, a typical color palette moving in RGB space at constant speed, using all the saturated colors of the rainbow.

The upper image below gives the same perceptually uniform rainbow except extended (looped) a bit to better see the region around red. The lower image is the same, except shifted by 20 pixels. The color distance between the rows is roughly constant, so ideally there should be a boundary line of constant contrast across the whole width. On my monitor, this appears not to be the case: the rows blend in the red-magenta area. As before, on LCD displays, the contrast may depend on the viewing angle.


The above two colors are separated by a distance of 18.9955 according to this online color distance calculator, whose results are in close (but not exact) agreement with my code. On my monitor, the colors appear quite different.


The above two colors are separated by a distance of 18.89. On my monitor, they appear similar.


The above two colors are separated by a distance of 19.108. On my monitor, they appear similar.

Based on the above examples, I'm less than convinced that L*a*b* space is good for defining perceptual color distance. Or, my monitor is bad at displaying colors.

Here is the program used to generate the images, and alternate download location for the inline images.

by Ken ( at March 13, 2017 04:05 AM

Tweag I/O

Linear types make performance more predictable

Jean-Philippe Bernardy and Arnaud Spiwack   |   13 March 2017

We’re extending GHC with linear types.

Ever since Jean-Yves Girard discovered linear logic in 1986, researchers around the world have been going “wow! resource tracking, this must be useful for programming languages”. After all, any real computation on a real machine takes resources (memory pages, disk blocks, interrupts, buffers etc) that then aren’t available anymore unless restored somehow. But despite this match apparently made in heaven, research on this subject has remained largely theoretical. It was becoming easy to just give up and assume this nut was simply too tough to crack. We ourselves have been there, but we recovered: we’re having a go at extending GHC with linear types.

Great! But why is this useful in a high-level programming language like Haskell? You’ll find the long of it in the paper we just submitted to ICFP’17 with Mathieu Boespflug, Ryan Newton and Simon Peyton Jones. In this blog post, we’ll briefly discuss (more in the paper) how we’re trying to achieve more predictable performance at a smaller memory footprint in Haskell, and give you a preview of what you might expect in your favourite compiler in the not-so-distant future.

A bit of history

Once upon a time, Jean-Yves Girard was playing with ways to describe the semantics of a λ-calculus with types, when he realised that from a semantic perspective there was nothing essential about the arrow type (the type for functions): it could be described in terms of two simpler constructions. He followed this thread through and came up with a strange beast he called linear logic.

Two of everything

Linear logic had two of everything: two ways of building conjunctions and disjunctions, two notions of truth, falsehood and two ways to negate. It’s a strange system, but perhaps not moreso than the zoo of cute names and symbols Girard conferred to every construct. For the purposes of this post, we’ll only need one new symbol from this zoo: , which reads lollipop (also called linear arrow, or lolly for close friends).

If we transpose linear logic to describing the behaviour of programs (by which point we talk about linear types), the linear arrow says this: a function that has type A ⊸ B is a function that has an A available to compute with, but it can only use it once. Not twice, not zero times: just once. It turns out that this property, which has come to be known as linearity, is very useful for compilers of functional programs.

Typing resources

Programming language researchers quickly took notice. It was not long before Yves Lafont proposed a language with safe memory management yet without needing a garbage collector, thanks to linear types. Philip Wadler piled on a few years later with a system also supporting state update while retaining the properties of a pure language. Recently, researchers have even pushed linear logic towards making it possible to reason about pointer aliasing (the absence or presence of aliasing matters a lot in the optimization and the correctness of C programs).

But despite all these early promises (and many more since then), linear types didn’t catch on in the mainstream. Mind you, there have been workarounds. It turns out linear types are also useful to model effects, but Haskell preferred monads for that purpose instead. Clean wanted safe mutable state, but eschewed monads, using uniqueness types instead. More recently, Rust rose to popularity with a system of ownership which is not unlike Clean’s uniqueness types. Both are complex systems that permeate the entire language and ecosystem in ways that make the learning curve pretty steep.

Linear types as an extension

What if you could enjoy all your favourite goodies from your favourite programming language, and yet be able to leverage linear types for precise resource management exactly where it matters (as Lafont did by avoiding garbage collection)? The result won’t be as good as Rust for what Rust does: it’s a different trade-off where we assume that such precision is only needed in small key areas of a program that otherwise freely uses functional programming abstractions as we know them today.

This is what we are proposing: a simple, unintrusive design that can be grafted to your favourite functional language at no cost for the programmer. We’re working on GHC, but this would work just as well in your favourite ML flavour.

So why are we doing this?

Among our many projects, we are working together with Seagate and a number of consortium partners on the SAGE platform, an EU funded R&D project exploring how to store massive amounts of data (in excess of one exabyte) and query this data efficiently. We use Haskell as a prototyping language to fail fast when we’re heading towards a dead end, backtrack and explore a different direction at low cost, and refactor our existing code easily when we commit to a different direction.

On this and other systems level projects, maintaining predictable latencies is key. Pusher recently documented how this matters to them too, to the point where they’ve been looking elsewhere for good latencies. Our use cases share the same characteristics. We decided to solve the problem by asking less of the GC, while extending Haskell to make working outside of the GC just as memory safe. You will find much more details in the paper, but in summary linear types help in two ways:

  • We can use linear types to manually, yet safely, manage data with malloc: because linearity forces the programmer using a value at least once, we can ensure that the programmer eventually calls free. And because it forces to use a value at most once, we can make sure that free-d data is never used (no use-after-free or double-free bugs). Anything that we malloc explicitly doesn’t end up on the GC heap, so doesn’t participate in increasing GC pause times.
  • Linear types can make fusion predictable and guaranteed. Fusion is crucial to writing programs that are both modular and high-performance. But a common criticism, one that we’ve seen born out in practice, is that it’s often hard to know for sure whether the compiler seized the opportunity to fuse intermediate data structures to reduce allocations, or not. This is still future work, but we’re excited about the possibilities: since fusion leans heavily on inlining, and since linear functions are always safe to inline without duplicating work because they only use their argument once, it should be possible with a few extra tricks to get guaranteed fusion.

But the story gets better still. Linear types aren’t only useful for performance, they can also be key to correctness. SAGE is a complex project with many communicating components. Linear types allow us to model these interactions at the type level, to statically rule out bugs where some component doesn’t respect the protocol that was agreed upon with others. We don’t talk about that much in the paper, but we’ll touch on that here.

What it will look like

Let’s start slow, with the fst function projecting the first component from a pair:

fst :: (a,b) -> a
fst (x,_) = x

So far, so standard. Now here is a new thing you cannot do:

fst :: (a,b) ⊸ a
fst (x,_) = x

This is the linear arrow: the type of functions which must use their arguments exactly once. The first projection is not linear, since a part of the pair is silently dropped. So the type checker will reject this program. It will also reject the diagonal, which uses its argument twice:

dup :: a ⊸ (a,a)
dup x = (x,x)

On the surface, this is almost the entire story: the linear arrow allows you to reject more programs, of which fst and dup are prototypical examples.

With that in mind, there’s a lot that linear types can be used for. One example is strongly typed protocols that check applications in a distributed system interact as expected. We’ll need a little bit of kit first:

data S a
data R a

newCaps :: (R a ⊸ S a ⊸ IO ()) ⊸ IO ()
send :: S a ⊸ a ⊸ IO ()
receive :: R a ⊸ (a ⊸ IO ()) ⊸ IO ()

In this API, S is a send capability: it gives the ability to send a message. R is a receive capability. A pair of corresponding capabilities is allocated by newCaps. The important thing to notice is that since both capabilities are linear, both must be consumed exactly once by a send and a receive respectively. Conversely, you can’t send/receive without having a corresponding send/receive capability on hand.

As a first example, let’s consider a protocol where a server expects two integers and returns the sum to the client. A simple function, except happening across a wire. This protocol is fully captured by the type (Int, Int, Int ⊸ IO ()), which reads: receive two Int’s, then send an Int. Using ⊸ IO () switches between “send” and “receive”.

To implement a protocol P, one has to write an implementation (a function) of type P ⊸ IO (). The other side of the wire (the client) must implement the dual protocol P ⊸ IO (), with a function of type (P ⊸ IO ()) ⊸ IO ():

type P = (Int, Int, IntIO ())

server :: PIO ()
server (n, p, k) = k (n + p)

client :: (PIO ()) ⊸ IO ()
client sendToSrvr = newCaps $ \r s -> do
  sendToSrvr (42, 57, send s)
  receive r (\n -> print n)

We can see how typing works: client must create a function Int ⊸ IO () for the server to send its result to. So it creates an S/R pair, into which the server will be able to send exactly one result. The r capability must also be consumed exactly once. Therefore, the client must call receive and do something with the result (in this case, it boringly prints it on a console).

Of course, one can replace all the linear arrows with regular arrows -> and the program stays well-typed. But the value of linear types lies in what they do not allow: client cannot forget to call receive, resulting in the server blocking on send; similarly, the server is not allowed to return twice to k (e.g. k (n+p) >> k (n*p) is not well-typed). This prevents all sort of bad behaviours. It is not a novel idea; see the paper’s “related work” section if you’re interested in the references.

To run the server and the client, we must assume an initial S/R pair s0/r0 (known only to the runner, for safety):

runServer :: IO ()
runServer = receive r0 server

runClient :: IO ()
runClient = client (send s0)

We can make more complex examples by alternating the ⊸ IO () construction to sequence the steps of the protocol. For instance, the following asks first for a number, then the word “apple” singular or pluralized, depending on the number, and returns a sentence:

copyInt :: Int ⊸ (Int,Int) -- such a function exists for every data type

data Number = Singular | Plural
type P = (Int, (Number, (String, StringIO ()) ⊸ IO ()) ⊸ IO ())

server :: PIO ()
server (n, k) =
    newCaps $ \r s -> do
    k (num, send s)
    receive r $ \(apples, k') -> do
      k' ("I have " ++ show n2 ++ apples)
    (n1,n2) = copyInt n
    num = if n1 == 1 then Singular else Plural

client :: (PIO ()) ⊸ IO ()
client k =
    newCaps $ \r s -> do
      k (42,send s)
      receive r $ \(num,k') ->
        newCaps $ \r' s' -> do
          let apples
                | Singular <- num = "apple"
                | Plural <- num = "apples"
          k' (apples, send s')
          receive r' $ \sentence ->
            print sentence

Running the server and client will result in the client printing the deliciously healthy sentence “I have 42 apples”. Again, the value is in what is rejected by the compiler, such as listening to r a second time in the client rather than to r'.

An important takeaway is how haskelly this all looks: just replace -> by and linearity kicks in. Usual datatypes, including tuples, take a linear meaning in a linear context. The technical details of how this is achieved are exposed in the article. Edsko de Vries wrote a blog post where he compares the trade-offs of related type systems; he comes in favour of a system where types are segregated into linear types and unrestricted types, but our position is that such a system, perhaps more flexible, would be more complex to implement, especially if we want good sharing of code between linear and non-linear contexts.

One thing that the article does not have, however, is a good description of how our prototype implementation (and type inference) works.

Did you say prototype?

Yes! There is a branch of GHC where we are implementing the above proposal. At the time of writing the prototype is still a bit crude: it handles the λ-calculus fragment properly, but case and data do not have full support yet. We believe we have the hard part behind us though: modifying the arrow type so that arrows carry an annotation discriminating whether they are regular arrows (->) or linear arrows ().

Indeed, GHC uses and abuses the arrow type all over the type inference mechanism. So making a change there required changes across many files. As it turns out, however, the changes are rather systematic and innocuous. The patch is currently under 1000 lines long. We are targeting a merge by the time of the 8.4 release of GHC.

In a future post, we’ll delve into what the paper doesn’t cover, to show how inferring linear types works.

Stay tuned!

by Engineering team at Tweag I/O at March 13, 2017 12:00 AM

March 12, 2017

Brandon Simmons

Almost inline ASM in haskell with foreign import prim

With help from Reid Barton in questions here and here I discovered it’s pretty easy to call assembly from GHC haskell with minimal overhead, so I cleaned up an example of this technique and posted it here:

This is especially useful if you want to return multiple values from a foreign procedure, where otherwise with the traditional FFI approach you would have to do some allocation and stuff the values into a struct or something. I find the above more understandable in any case.

Here’s an example of the dumped ASM from the Main in the example above:

    call newCAF
    addq $8,%rsp
    testq %rax,%rax
    je _c73k
    movq $stg_bh_upd_frame_info,-16(%rbp)
    movq %rax,-8(%rbp)
    movq $block_info,-24(%rbp)
    movl $4,%edi
    movl $3,%esi
    movl $2,%r14d
    movl $1,%ebx
    addq $-24,%rbp
    jmp sipRound_s_x3
    movq $104,904(%r13)
    movq $block_info,-32(%rbp)
    movq %r14,-24(%rbp)
    movq %rsi,-16(%rbp)
    movq %rdi,-8(%rbp)
    movq %rbx,(%rbp)
    addq $-32,%rbp

You can see we just prepare argument registers, do whatever with the stack pointer, do a jump, and then push the return values onto the stack. For my purposes this was almost too much overhead to make this worthwhile (you can look at notes in the code).

I thought about sketching out a ghc proposal about a way to formalize this, maybe make it safer, and maybe somehow more efficient but I don’t have the time right now and don’t really have the expertise to know if this is even a good idea or how it could work.

March 12, 2017 06:08 PM

March 11, 2017

Edward Z. Yang

Designing the Backpack signature ecosystem

Suppose you are a library writer interested in using Backpack. Backpack says that you can replace a direct dependency on a function, type or package with one or more signatures. You typecheck against a signature and your end user picks how they want to eventually implement the signature.

Sounds good right? But there's a dirty little secret: to get all of this goodness, you have to write a signature--you know, a type signature for each function and type that you want to use in your library. And we all know how much Haskellers hate writing signatures. But Backpack has a solution to this: rather than repeatedly rewrite signatures for all your packages, a conscientious user can put a signature in a package for reuse in other packages.

For the longest time, I thought that this was "enough", and it would be a simple matter of sitting down and writing some tutorials for how to write a signature package. But as I sat down and started writing signature packages myself, I discovered that there was more than one way to set things up. In the post, I want to walk through two different possible designs for a collection of signature packages. They fall out of the following considerations:

  • How many signature packages for, e.g., bytestring, should there be? There could be exactly one, or perhaps a separate package for each API revision?
  • Should it be possible to post a new version of a signature package? Under what circumstances should this be allowed?
  • For developers of a library, a larger signature is more convenient, since it gives you more functionality to work with. For a client, however, a smaller signature is better, because it reduces the implementation burden. Should signature packages be setup to encourage big or small signatures by default?

A signature package per release

Intuitively, every release of a package is also associated with a "signature" specifying what functions that release supports. One could conclude, then, that there should be a signature package per release, each package describing the interface of each version of the package in question. (Or, one could reasonably argue that GHC should be able to automatically infer the signature from a package. This is not so easy to do, for reasons beyond the scope of this post.)

However, we have to be careful how we perform releases of each of these signatures. One obvious but problematic thing to do is this: given bytestring-, also release a bytestring-sig- The problem is that in today's Haskell ecosystem, it is strongly assumed that only one version of a package is ever selected. Thus, if I have one package that requires bytestring-sig ==, and another package that requires bytestring-sig ==, this will fail if we try to dependency solve for both packages at the same time. We could make this scheme work by teaching Cabal and Stack how to link against multiple versions of a signature package, but at the moment, it's not practical.

An easy way to work around the "multiple versions" problem is to literally create a new package for every version of bytestring. The syntax for package names is a bit irritating (alphanumeric characters plus hyphens only, and no bare numbers between a hyphen), but you could imagine releasing bytestring-v1008, bytestring-v1009, etc., one for each version of the API that is available. Once a signature package is released, it should never be updated, except perhaps to fix a mistranscription of a signature.

Under semantic versioning, packages which share the same major version are supposed to only add functionality, not take it away. Thus, these successive signature packages can also be built on one another: for example bytestring-v1009 can be implemented by inheriting all of the functions from bytestring-v1008, and only adding the new functions that were added in 0.10.9.

A signature package per major release series

There is something very horrible about the above scheme: we're going to have a lot of signature packages: one per version of a package! How awful would it be to have in the Hackage index bytestring-v900, bytestring-v901, bytestring-v902, bytestring-v1000, bytestring-v1002, bytestring-v1004, bytestring-v1006 and bytestring-v1008 as package choices? (With perhaps more if there exist patch releases that accidentally changed the API.) Thus, it is extremely tempting to try to find ways to reduce the number of signature packages we need to publish.

Here is one such scheme which requires a signature package only for major releases; e.g., for bytestring, we would only have bytestring-v9 and bytestring-v10:

  • The latest version of bytestring-v9 should correspond to the "biggest" API supported by the 0.9 series. Thus, bytestring-v9, every minor version release of bytestring, there is a new release of bytestring-v9: e.g., when bytestring- is released, we release bytestring-v9-1.0. Each of the releases increases the functionality recorded in the signature, but is not permitted to make any other changes.
  • When depending on the signature package, we instead provide a version bound specifying the minimum functionality of the signature required to build our package; e.g., bytestring-v9 >= 1.0. (Upper bounds are not necessary, as it assumed that a signature package never breaks backwards compatibility.)

There is one major difficulty: suppose that two unrelated packages both specify a version bound on bytestring-v9. In this case, the ultimate version of the signature package we pick will be one that is compatible with both ranges; in practice, the latest version of the signature. This is bad for two reasons: first, it means that we'll always end up requiring the client to implement the full glory of bytestring-v9, even if we are compatible with an earlier version in the release series. Second, it means that whenever bytestring-v9 is updated, we may bring more entities into scope: and if that introduces ambiguity, it will cause previously compiling code to stop compiling.

Fortunately, there is a solution for this problem: use signature thinning to reduce the required entities to precisely the set of entities you need. For example, suppose that bytestring-v9-0.0 has the following signature:

signature Data.ByteString where
    data ByteString
    empty :: ByteString
    null :: ByteString -> Bool

As a user, we only needed ByteString and empty. Then we write in our local ByteString signature:

signature Data.ByteString (ByteString, empty) where

and now no matter what new functions get added to bytestring-v9-0.0, this signature will only ever require ByteString and empty. (Another way of thinking about signature thinning is that it is a way to centralize explicit import lists.) Notice that this scheme does not work if you don't have a separate package per major release series, since thinning can't save you from a backwards incompatible change to the types of one of the functions you depend on.

These signature thinning headers can be automatically computed; I've written a tool (ghc-usage) which does precisely this. Indeed, signature thinning is useful even in the first design, where they can be used to reduce the requirements of a package; however, with a signature package per major release, they are mandatory; if you don't use them, your code might break.


So, what design should we adopt? I think the first scheme (a signature package per release) is more theoretically pure, but I am very afraid of the "too many packages" problem. Additionally, I do think it's a good idea to thin signatures as much as possible (it's not good to ask for things you're not going to use!) which means the signature thinning requirement may not be so bad. Others I have talked to think the first scheme is just obviously the right thing to do.

Which scheme do you like better? Do you have your own proposal? I'd love to hear what you think. (Also, if you'd like to bikeshed the naming convention for signature packages, I'm also all ears.)


After publishing this post, the comments of several folks made me realize that I hadn't motivated why you would want to say something about the API of bytestring-0.10.8; don't you just want a signature of strings? So, to address this comment, I want to describe the line of reasoning that lead me down this path.

I started off with a simple goal: write a signature for strings that had the following properties:

  1. Be reasonably complete; i.e., contain all of the functions that someone who wanted to do "string" things might want, but
  2. Be reasonably universal; i.e., only support functions that would be supported by all the major string implementations (e.g., String, strict/lazy Text, strict/lazy Word8/Char8 ByteString and Foundation strings.)

It turned out that I needed to drop quite a number of functions to achieve universality; for example, transpose, foldl1, foldl1', mapAccumL/R, scanl, replicate, unfoldr, group, groupBy, inits, tails are not implemented in Foundation; foldr', foldr1', scanl1, scanr, scanr1, unfoldN, spanEnd, breakEnd, splitOn, isInfixOf are not implemented by the lazy types.

This got me thinking that I could provide bigger signatures, if I didn't require the signature to support all of the possible implementations; you might have a signature that lets you switch between only the strict variants of string types, or even a signature that just lets you swap between Word8 and Char8 ByteStrings.

But, of course, there are combinatorially many different ways one could put signatures together and it would be horrible to have to write (and name) a new signature package for each. So what is the minimal unit of signature that one could write? And there is an obvious answer in this case: the API of a specific module (say, Data.ByteString) in a specific version of the package. Enter the discussion above.

Appendix 2

Above, I wrote:

But, of course, there are combinatorially many different ways one could put signatures together and it would be horrible to have to write (and name) a new signature package for each. So what is the minimal unit of signature that one could write? And there is an obvious answer in this case: the API of a specific module (say, Data.ByteString) in a specific version of the package.

I think there is an alternative conclusion to draw from this: someone should write a signature containing every single possible function that all choices of modules could support, and then have end-users responsible for paring these signatures down to the actual sets they use. So, everyone is responsible for writing big export lists saying what they use, but you don't have to keep publishing new packages for different combinations of methods.

I'm pursuing this approach for now!

by Edward Z. Yang at March 11, 2017 11:40 AM

Manuel M T Chakravarty

Do-It-Yourself Functional Reactive Programming @ iOSCon in London

End of this month, I will talk at iOSCon 2017 in London (30 & 31 March). I am very much looking forward to get to know the vibrant iOS dev community in London as well as to meet the other speakers. The line up of talks looks awesome, promising plenty of both breadth and depth.

In my own talk, I will deconstruct functional reactive programming (FRP) to show that it is based on a few simple ideas and holds the potential to improve the architecture of iOS apps. We will discuss questions, such as what is the purpose of FRP, how do you use it to structure your application, and how can you implement it yourself?

One of the things that I love about Swift is that it enables us to conveniently use functional programming concepts to write clearer and more robust code. The ease with which we can implement and use FRP is a great example of that capability.

See you in London @ iOSCon 2017!

March 11, 2017 10:27 AM

March 10, 2017

Roman Cheplyaka

Haskell without GMP

When you compile a Haskell program with GHC, by default your program is linked against the GMP (GNU Multiple Precision Arithmetic) library. GHC uses GMP to implement Haskell’s arbitrary-precision Integer type.

Because GMP is distributed under the L/GPL licenses, this presents a problem if you want to link the executable statically and distribute it without the implications of LGPL.

Here I’ll show how to compile a Haskell program without GMP. The process consists of two steps:

  1. Install a GHC compiled with integer-simple instead of GMP. You may need to compile such a GHC yourself.
  2. Make sure your dependencies do not use GMP.

These instructions are geared towards stack, but it should be clear how to adapt them to other workflows.

Install GHC with integer-simple

integer-simple is a pure Haskell implementation of the subset of GMP functionality.

Because the Integer type is provided by the base library, and the base library is compiled at the same time as GHC itself, we need a different build of GHC to support integer-simple — although that may change at some point.

At the time of writing, FP Complete distributes integer-simple builds for several recent versions of GHC, but only for Windows. To check, look at the current version of stack-setup-2.yaml and search for “integersimple”.

Thus, on Windows you can say

stack setup --ghc-variant=integersimple 8.0.2

and it will download and install the GHC 8.0.2 based on integer-simple.

As part of my work for nstack, I also prepared builds of GHC 8.0.2 with integer-simple for Linux and macOS. You can download them from, or you can just say

stack setup --ghc-variant=integersimple --setup-info-yaml= 8.0.2

If you are inside a stack project, add

ghc-variant: integersimple

to stack.yaml so that stack knows which compiler flavor to use. Also, in this case you don’t need to give stack setup the GHC version or --ghc-variant; these will be taken from stack.yaml.

If there is no precompiled integer-simple GHC for your platform or desired GHC version, you’ll have to build it yourself as I describe below.

Compile GHC with integer-simple

These instructions were tested with GHC 8.0.2 on Linux and macOS.

  1. Check the system requirements
  2. Get the GHC source by either cloning the git repo or downloading the source tarball.

  3. Save the template mk/ as mk/

    cp mk/ mk/

    Now, add the following line somewhere in mk/


    While editing that file, also choose the build profile by uncommenting one of the BuildFlavour = lines.

    • To test the process, use BuildFlavour = quick.
    • Once you are happy with the result, run make distclean and rebuild with BuildFlavour = perf.

    Another option I found useful to set in mk/ is


    Otherwise, I get errors because I don’t have various exotic TeX packages installed.

  4. Follow the standard build instructions, except the final make install command.

  5. Run make binary-dist to generate the release tarball.

  6. Download the current stack-setup-2.yaml and add a record for your release, such as

            url: "/home/user/ghc/ghc-8.0.2-x86_64-unknown-linux.tar.xz"
            content-length: 114017964
            sha1: ad38970c4431d44fef38c4696847ba491ef24332

Now you can follow the instructions from the previous section, except replace the stack-setup-2.yaml url with the path or url of your own stack-setup-2.yaml file.

Make sure your dependencies do not use GMP

Some packages depend on GMP through the integer-gmp package.

Fortunately, such packages usually have a Cabal flag to remove this dependency or replace it with integer-simple. The flag itself is usually called integer-gmp or integer-simple.

There are different ways to set these flags. With stack, you can declare the flags in stack.yaml as follows:

- text-
- hashable-
- scientific-
- integer-logarithms-1.0.1
- cryptonite-0.22

    integer-simple: true
    integer-gmp: false
    integer-simple: true
    integer-gmp: false
    integer-gmp: false

The above YAML snippet can be easily turned into a custom snapshot and shared among multiple stack projects if needed.


  1. LGPL licensing restrictions on Windows because of integer-gmp
  2. How to use different ghc builds with stack?

March 10, 2017 08:00 PM

FP Complete

Partial patterns in do blocks: let vs return

This blog post is about a pattern (pun not intended) I've used in my code for a while, and haven't seen discussed explicitly. A prime example is when doing simplistic parsing using the functions in Data.Text.Read. (And yes, this is a contrived example, and using parsec or attoparsec would be far better.)

Full versions of the code below are available as a Github Gist, and embedded at the end of this post.

The example: consider a file format encoding one person per line, indicating the name, height (in centimeters), age (in years), and bank balance (in your favorite currency). I have no idea why anyone would have such a collection of information, but let's roll with it:

Alice 165cm 30y 15
Bob 170cm 35y -20
Charlie 175cm 40y 0

And we want to convert this into a list of Person values:

data Person = Person
    { name    :: !Text
    , height  :: !Int
    , age     :: !Int
    , balance :: !Int
    deriving Show

Using the Data.Text and Data.Text.Read APIs, this isn't too terribly painful:

parseLine :: Text -> Maybe Person
parseLine t0 = do
    let (name, t1) = T.break (== ' ') t0
    t2 <- T.stripPrefix " " t1
    (height, t3) <-
        case decimal t2 of
            Right (height, t3) -> Just (height, t3)
            Left _ -> Nothing
    t4 <- T.stripPrefix "cm " t3
    (age, t5) <-
        case decimal t4 of
            Right (age, t5) -> Just (age, t5)
            Left _ -> Nothing
    t6 <- T.stripPrefix "y " t5
    balance <-
        case signed decimal t6 of
            Right (balance, "") -> Just balance
            _ -> Nothing
    Just Person {..}

We start off with the original value of the line, t0, and continue to bite off pieces of it in the format we want. The progression is:

  1. Use break to grab the name (everything up until the first space)
  2. Use stripPrefix to drop the space itself
  3. Use the decimal function to parse out the height
  4. Use stripPrefix to strip off the cm after the height
  5. Use decimal and stripPrefix yet again, but this time for the age and the trailing y
  6. Finally grab the balance using signed decimal. Notice that our pattern match is slightly different here, insisting that the rest of the input be the empty string to ensure no trailing characters

If we add to this a pretty straight-forward helper function and a main function:

parseLines :: Text -> Maybe [Person]
parseLines = mapM parseLine . T.lines

main :: IO ()
main =
    case parseLines input of
        Nothing -> error "Invalid input"
        Just people -> mapM_ print people

We get the output:

Person {name = "Alice", height = 165, age = 30, balance = 15}
Person {name = "Bob", height = 170, age = 35, balance = -20}
Person {name = "Charlie", height = 175, age = 40, balance = 0}

And if we corrupt the input (such as by replacing 175cm with x175cm), we get the output:

v1.hs: Invalid input
CallStack (from HasCallStack):
  error, called at v1.hs:49:20 in main:Main

This works, and the Data.Text.Read API is particularly convenient for grabbing part of an input and then parsing the rest. However, all of those case expressions really break up the flow, feel repetitive, and make it difficult to follow the logic in that code. Fortunately, we can clean this up with some lets and partial pattern matches:

parseLine :: Text -> Maybe Person
parseLine t0 = do
    let (name, t1) = T.break (== ' ') t0
    t2 <- T.stripPrefix " " t1
    let Right (height, t3) = decimal t2
    t4 <- T.stripPrefix "cm " t3
    let Right (age, t5) = decimal t4
    t6 <- T.stripPrefix "y " t5
    let Right (balance, "") = signed decimal t6
    Just Person {..}

That's certainly easier to read! And our program works... assuming we have valid input. However, let's try running against our invalid input with x175cm:

v2.hs: v2.hs:27:9-39: Irrefutable pattern failed for pattern Right (height, t3)

We've introduced partiality into our function! Instead of being well behaved and returning a Nothing, our program now creates an impure exception that blows up in our face, definitely not what we wanted with a simple refactoring.

The problem here is that, when using let, an incomplete pattern match turns into a partial value. GHC will essentially convert our:

let Right (height, t3) = decimal t2


let Right (height, t3) = decimal t2
    Left _ = error "Irrefutable pattern failed"

What we really want is for that Left clause to turn into a Nothing value, like we were doing explicitly with our case expressions above. Fortunately, we've got one more trick up our sleeve to do exactly that:

parseLine :: Text -> Maybe Person
parseLine t0 = do
    let (name, t1) = T.break (== ' ') t0
    t2 <- T.stripPrefix " " t1
    Right (height, t3) <- Just $ decimal t2
    t4 <- T.stripPrefix "cm " t3
    Right (age, t5) <- Just $ decimal t4
    t6 <- T.stripPrefix "y " t5
    Right (balance, "") <- Just $ signed decimal t6
    Just Person {..}

To make it abundantly clear, we've replaced:

let Right (height, t3) = decimal t2


Right (height, t3) <- Just $ decimal t2

We've replaced our let with the <- feature of do-notation. In order to make things type-check, we needed to wrap the right hand side in a Just value (you could also use return or pure, I was just trying to be explicit in the types). But we've still got an incomplete pattern on the left hand side, so why is this better?

When, within do-notation, you have an incomplete pattern match, GHC does something slightly different. Instead of using error and creating an impure exception, it uses the fail function. While generally speaking there are no guarantees that fail is a total function, certain types - like Maybe - due guarantee totality, e.g.:

instance Monad Maybe where
  fail _ = Nothing

Voila! Exactly the behavior we wanted, and now we've achieved it without some bulky, repetitive cases. My general advice around these techniques:

  • Don't define partial patterns in lets, cases, or function definitions.
  • Only use partial patterns within do-notation if you know that the underlying type defines a total fail function.

For completeness, you can also achieve this with more explicit conversion to a Maybe with the either helper function:

parseLine :: Text -> Maybe Person
parseLine t0 = do
    let (name, t1) = T.break (== ' ') t0
    t2 <- T.stripPrefix " " t1
    (height, t3) <- either (const Nothing) Just $ decimal t2
    t4 <- T.stripPrefix "cm " t3
    (age, t5) <- either (const Nothing) Just $ decimal t4
    t6 <- T.stripPrefix "y " t5
    (balance, t7) <- either (const Nothing) Just $ signed decimal t6
    guard $ T.null t7
    Just Person {..}

While this works, personally I'm not as big a fan:

  • It feels bulkier, hiding the main information I want to express
  • It doesn't handle the issue of ensuring no content is left over after parsing the balance, so we need to add an explicit guard. You could just use (balance, "") <-, but that's just going back to using the partial pattern rules of do-notation.

Hopefully you found this little trick useful. Definitely not earth shattering, but perhaps a fun addition to your arsenal. If you want to learn more, be sure to check out our Haskell Syllabus.

The four versions of the code mentioned in this post are all available as a Github Gist:

<script src=""></script>

March 10, 2017 05:44 PM