Planet Haskell

July 25, 2016

Neil Mitchell

Maintainer required for Derive

Summary: I'm looking for a maintainer to take over Derive. Interested?

The Derive tool is a library and set of definitions for generating fragments of code in a formulaic way from a data type. It has a mechanism for guessing the pattern from a single example, plus a more manual way of writing out generators. It supports 35 generators out of the box, and is depended upon by 75 libraries.

The tool hasn't seen much love for some time, and I no longer use it myself. It requires somewhat regular maintenance to upgrade to new versions of GHC and haskell-src-exts. There are lots of directions the tool could be taken, more derivations, integration with the GHC Generic derivation system etc. There's a few generic pieces that could be broken off (translation between Template Haskell and haskell-src-exts, the guessing mechanism).

Anyone who is interested should comment on the GitHub ticket. In the absence of any volunteers I may continue to do the regular upgrade work, or may instead have it taken out of Stackage and stop upgrading it.

by Neil Mitchell ( at July 25, 2016 02:45 PM

Dimitri Sabadie

luminance-0.6.0 sample

It’s been two weeks luminance is at version 0.6.0. I’m very busy currently but I decided to put some effort into making a very minimalistic yet usable sample. The sample uses luminance and luminance-gl (the OpenGL 3.3 backend being the single one available for now).

You’ll find it here. The code is heavily commented and you can of course clone the repository and and run the executable with cargo.

I’ll post a more detailed blog post about the application I’m building with luminance right now later on.

Keep the vibe! :)

by Dimitri Sabadie ( at July 25, 2016 09:40 AM

Ken T Takusagawa

[leijaltq] Typeof as a type

Wherever one can specify a type, let it be possible to use "TYPE_OF(EXPRESSION)" instead.  For example, it can be used in type signatures and declarations of type synonyms.  Here is an example with syntax similar to Haskell:

A library has functions

f1 :: Int -> Foo;
f1 i = ...
f2 :: Foo -> Int;
f2 f = ...

The user's code importing the library might do something like

type MyFoo = TYPE_OF(f1 undefined);
intermediate :: MyFoo;
intermediate = f1 42;

consume_intermediate :: Int;
consume_intermediate = f2 intermediate;

If a new version of the library were to rename Foo into Bar, the user's code would still work unmodified.  (It is irrelevant whether the library exports Foo, later Bar, though not exporting the type would force the user to use TYPE_OF or avoid explicit type signatures, which seems silly.)

This feature could be useful during development if the names of things are not yet decided (bike shedding), but we do know how we want to use them.

The compiler will have to flag errors of circular references of TYPE_OF.

by Ken ( at July 25, 2016 03:03 AM

July 24, 2016

Richard Eisenberg

Dependent types in Haskell: Progress Report

It was drawn to my attention that there is an active Reddit thread about the future of dependent types in Haskell. (Thanks for the heads up, @thomie!) Instead of writing a long response inline in Reddit, it seems best to address the (very knowledgeable, respectful, and all around heartening) debate here.

When can we expect dependent types in GHC?

The short answer: GHC 8.4 (2018) at the very earliest. More likely 8.6 or 8.8 (2019-20).

Here is the schedule as I see it:

  • GHC 8.2: Clean up some of the lingering issues with -XTypeInType. As I will be starting a new job (Asst. Prof. at Bryn Mawr College) this fall, I simply won’t have the opportunity to do more than some cleanup work for the next release. Also, quite frankly, I need a release cycle off from the challenge of putting in a large new feature. Polishing up -XTypeInType for release took probably an extra full month of unexpected work time! I don’t regret this in the slightest, but I could use a cycle off.
  • GHC 8.4: This depends on what other research opportunities come up in the next year and how much more attention -XTypeInType needs. If all goes well this fall and I can get a few publications out in the next year (certainly possible – I have several in the works), then I could conceivably start primary implementation of -XDependentTypes next summer. The odds that it will be in a state to merge for 8.4 are slim, however.
  • GHC 8.6: We’re now talking about a real possibility here. Assuming I start the implementation next summer, this would give me a year and a half to complete it. I desperately wish to avoid merging late in the cycle (which is what made -XTypeInType so stressful) so perhaps merging soon after GHC 8.4 comes out is a good goal. If this slips, GHC 8.8 seems like quite a likely candidate.

Regardless of the schedule, I have every intention of actually doing this work.

One major oversight in the schedule above: I have completely discounted the possibility of collaborators in coding this up. Do you wish to help make this a reality? If so, let’s talk. I’ll admit that there may be a bit of a hill for an outside collaborator to climb before I really start collaborating in earnest, so be prepared to show (or create!) evidence that you’re good at getting your hands dirty in the greasy wheels of GHC’s typechecker without very much oversight. I’ve encouraged several of you on Trac/Phab – you know who you are, I hope. For others who have not yet contributed to GHC: you’re likely best served starting smaller than implementing dependent types! But let’s talk anyway, if you’re interested.

What is the design of dependent types in Haskell?

I expect to hand in my dissertation in the next two weeks. While I am developing it in the public eye (and warmly welcome issues to be posted), there is no publicly available PDF build. Building instructions are in the README. I will post a built PDF when I hand in my draft to my thesis committee. I will be defending on September 1 and will likely make some revisions (as suggested by my committee) afterward.

Readers here will likely be most interested in Chapters 3 and 4. Chapter 3 will contain (I’m still writing it!) numerous examples of dependent types in Haskell and how they might be useful. Chapter 4 presents the design of dependent types in Haskell as a diff over current Haskell. This design is not yet up to the standard of the Haskell Reports, mostly because it is unimplemented and seems not worth the effort of formalization until we know it is implementable. For the overly curious, Chapter 5 contains a new intermediate language (to replace GHC Core) and Chapter 6 contains the type inference algorithm that will deal with dependent types. Happy summer reading!

Responses to particular comments on the Reddit thread

  • @elucidatum: How radical of a change and how much of a challenge will it be to refactor existing codebases?

    No change is necessary. All code that currently compiles with -XTypeInType will compile with -XDependentTypes. (The only reason I have to set -XTypeInType as my baseline is because of the parsing annoyance around *, which must be imported to be used with -XTypeInType.) Any refactoring will be around how much you, as the Haskell author, wish to take advantage of dependent types.

  • @jlimperg: Pervasive laziness in Haskell means that we like to use a lot of coinductive types. But this is really annoying for proof purposes because coinduction, despite the nice duality with induction, is a lot less pleasant to work with.

    Yes, this is true. My approach is, essentially, to pretend that types are inductive, not coinductive. One consequence of this decision is that proofs of type equality will have to be run. This means that including dependent types will slow down your running program. Sounds horrible, doesn’t it? It doesn’t have to, though.

    Suppose you have a function proof :: ... -> a :~: b. The function proof provides a proof that type a equals type b. If this function terminates at all, it will always produce Refl. Thus, if we knew that the function terminated, then we wouldn’t have to run it. We can’t know whether it terminates. But you, the programmer, can assert that it terminates, like this: {-# RULES "proof" proof ... = unsafeCoerce Refl #-} Now, GHC will replace any use of proof with Refl directly. Note that GHC still type-checks your proof. All this RULE does is assert termination.

    “But,” you say, “I don’t want to have to merely assert termination! If I wanted to assert correctness instead of prove it, I wouldn’t use dependent types.” My response: “Touché.” Haskell indeed is less powerful than those other dependently typed languages in this regard. Nevertheless, by using dependent types in Haskell, you still get a whole lot more compile-time guarantees than you get without dependent types. You just don’t get termination. You thus have a choice: “prove” termination at runtime by actually running your proofs, or assert it at compile time and keep your dependently typed program efficient, and still with lots of guarantees. Recall that we Haskellers have never proved termination of anything, ever, so not proving termination of a function named proof shouldn’t be all that alarming.

    Note: If RULES such as the one above become pervasive, perhaps a compiler flag can make them automatic, effectively (and concisely) assuming termination for all proofs in a module.

  • @jlimperg: Proving is hard

    Yes, it is. Typechecker plugins may help here. It is easy enough, however, to implement dependent types without this advanced support. As we work through the consequences of dependent types in Haskell, I’m confident the community (including me) will come up with ways to make it easier.

  • @jlimperg: As is well-known, a dependent type system is inconsistent (i.e. everything can be proven) unless all computations terminate, which is obviously not the case for general Haskell.

    Yes, this is true. Dependent types in Haskell will be inconsistent, when we view Haskell as a logic. Dependent types will still remain type-safe however. (This is because we run the proofs!) I just wish to point out here that @jlimperg suggests a syntactic check for termination: this, sadly, will not work. Haskell has too many ways for a computation to diverge, and a syntactic check can rule out only general recursion and partial pattern matches. Haskell also has infinite data types, non-strictly-positive datatypes, TypeRep (which can be abused to cause a loop), Type :: Type, and likely more back doors. I’d love to see a termination checker for Haskell, but I’m not holding my breath.

  • @jlimperg: This point is very speculative, but I strongly dislike the current flavour of ‘almost-dependent’ type-level programming in Haskell.

    So do I. Singletons are an abomination. I hate them. These are gone with my design for dependent types, and I think the resulting language has the niceties we all want in a dependently typed language (modulo termination checking).

  • @dogodel: I think it will take a while for the change to percolate into better design. … I think the most immediate benefit will be for (no surprise) expressive DSL, which are actually quite common in any modest codebase, but maybe not the “core” of the project.

    Agreed completely. It will take time for us to figure out the best way to use dependent types.

  • @sinyesdo: The best summary I can offer is that “totality” is really really important for DT languages

    This is true for those other dependently typed languages, but not for Haskell. See my response to the first of @jlimperg’s points quoted here.

  • @ccasin: The main reasons to care that your programming language is total are to make the type system consistent as a logic and to make type checking decidable. But we’ve already given up both these things in Haskell, and it’s possible to have dependent types without them.

    Agreed in full, and with @ccasin’s full post.

  • @jmite: If you want fully Dependent-Type types, why not use Idris, Agda, Coq, or F*?

    I’m in broad agreement with the responses to this point on Reddit: basically, that none of these languages have Haskell’s ecosystem or optimizing compiler. See also Section 3.3 of my dissertation.

  • @tactics: What does “fully dependent types” even mean for something like Haskell? You would have to rework the core language entirely.

    Yes, precisely. This is Chapter 5 of my dissertation.


I hope this information helps. Do keep an eye out for my finished dissertation sometime in the next few months. And, as always, this is all a work in progress and no one should take anything as set in stone. If there’s a design decision you disagree with, please speak up!

by Richard Eisenberg at July 24, 2016 06:27 PM

July 22, 2016

Neil Mitchell

me :: Standard Chartered -> Barclays

Summary: I've left Standard Chartered and will be starting at Barclays shortly.

I've been working at Standard Chartered for almost 8 years, but a few weeks ago I handed in my notice. While at Standard Chartered I got to work with some very smart people, on some very interesting projects. I have learnt a lot about whether Haskell works at large scales (it does!), what mistakes you can make and how to avoid those mistakes. My work at Standard Chartered lead to the Shake build system, along with 100's of other projects that alas remain locked in proprietary banking world. I've used our in-house strict Haskell (Mu) to write lots of systems, and cemented my opinion of whether languages should be strict or lazy (lazy!). I've taught many people Haskell, and sold the values of functional programming to everyone I met.

After all that, I've decided to take a job at Barclays and will be starting mid-August. In this new role I plan to use real GHC-Haskell, all the advanced features that enables (existentials, laziness etc), with Cabal/Stack to leverage all of Hackage. My experience of building on top of C/C++ libraries for the last 8 years has made me envious of the amazing quality of Haskell libraries (to a first approximation, they might be a little slower than the C/C++ on average, but they won't leak, are multithread safe, and someone has thought about the corner cases). With any luck, I'll also be able to contribute some more of these libraries back to the community.

Once I officially start at Barclays I'll be hiring a team of London-based Haskell programmers to work with. More details to follow in a few weeks. For now, I will say that for hiring decisions I'm really interested in seeing actual code. If you are interested in a Haskell job anywhere you should probably have a GitHub account with some code on it. If you've done any fun projects, hacked around with an encoding of de-Bruijn indicies with type families, or tried to implement a JavaScript parser using only functions from base which have at most 1 vowel, shove it up. Having libraries on Hackage is even better. I judge people by their best code, not their worst, so more code is always better.

In case people are curious, here are a few questions I expect to be asked:

  • Does this mean Standard Chartered is going to stop using Haskell? No. Standard Chartered has lots of Haskell programmers and will be continuing with Mu (aka the Haskell language, but not the GHC implementation).
  • What does this mean for my open source libraries? For most, it means nothing, or they will improve because I might be using them in my day job. I don't think Standard Chartered is the biggest user of any of my libraries anymore. The one exception is Bake, which was designed quite specifically to address the needs of Standard Chartered. I may continue to work on it, I may pass maintainership over to someone at Standard Chartered, or I may do nothing further with it. Time will tell, but the source will remain available indefinitely.
  • I got a call from a headhunter for Barclays, is that you? No. Currently Barclays are recruiting someone to work on FPF using Haskell. That's a totally different team. My primary method of recruitment will be this blog, not headhunters. Anyone who ever wants a job with me should talk to me, not people who suggest they are working on my behalf :).
  • Are you hiring right now? No. I will be on the 15th of August once I join.

by Neil Mitchell ( at July 22, 2016 12:03 PM

Robin KAY

HsQML released: From Zürich

Last night I arrived in Zürich for ZuriHac 2016 and, in the brief space between finding my way from the airport and falling asleep, released HsQML You can download the latest release of this Haskell binding to the Qt Quick GUI framework from Hackage as usual.

This is purely a bug-fix release, fixing building with newer versions of Cabal (1.24, GHC 8) and Qt (5.7+). It also resolves some difficulties with building the library on MacOS and I've revised the MacOS install documentation with more information.

In other news, I've decommissioned the old Trac bug-tracker as I accidentally broke it some time ago during a server upgrade and failed to notice. I take this as a bad sign for its effectiveness, so please just e-mail me with any issues instead. I enjoy hearing from people trying to use the library and I always try to reply with assistance as quickly as possible, so don't be shy.

release- - 2016.07.21

  * Added support for Cabal 1.24 API.
  * Fixed linking shared builds against MacOS frameworks (needs Cabal 1.24+).
  * Fixed building with Qt 5.7.

by Robin KAY ( at July 22, 2016 08:22 AM

July 21, 2016

Mark Jason Dominus

A hack for getting the email address Git will use for a commit

Today I invented a pretty good hack.

Suppose I have branch topic checked out. It often happens that I want to

    git push origin topic:mjd/topic

which pushes the topic branch to the origin repository, but on origin it is named mjd/topic instead of topic. This is a good practice when many people share the same repository. I wanted to write a program that would do this automatically.

So the question arose, how should the program figure out the mjd part? Almost any answer would be good here: use some selection of environment variables, the current username, a hard-wired default, and the local part of Git's configuration setting, in some order. Getting is easy (git config get but it might not be set and then you get nothing. If you make a commit but have no, Git doesn't mind. It invents an address somehow. I decided that I would like my program to to do exactly what Git does when it makes a commit.

But what does Git use for the committer's email address if there is no set? This turns out to be complicated. It consults several environment variables in some order, as I suggested before. (It is documented in git-commit-tree if you are interested.) I did not want to duplicate Git's complicated procedure, because it might change, and because duplicating code is a sin. But there seemed to be no way to get Git to disgorge this value, short of actually making a commit and examining it.

So I wrote this command, which makes a commit and examines it:

    git log -1 --format=%ce $(git-commit-tree HEAD^{tree} < /dev/null)

This is extremely weird, but aside from that it seems to have no concrete drawbacks. It is pure hack, but it is a hack that works flawlessly.

What is going on here? First, the $(…) part:

    git-commit-tree HEAD^{tree} < /dev/null

The git-commit-tree command is what git-commit uses to actually create a commit. It takes a tree object, reads a commit message from standard input, writes a new commit object, and prints its SHA1 hash on standard output. Unlike git-commit, it doesn't modify the index (git-commit would use git-write-tree to turn the index into a tree object) and it doesn't change any of the refs (git-commit would update the HEAD ref to point to the new commit.) It just creates the commit.

Here we could use any tree, but the tree of the HEAD commit is convenient, and HEAD^{tree} is its name. We supply an empty commit message from /dev/null.

Then the outer command runs:

    git log -1 --format=%ce $(…)

The $(…) part is replaced by the SHA1 hash of the commit we just created with git-commit-tree. The -1 flag to git-log gets the log information for just this one commit, and the --format=%ce tells git-log to print out just the committer's email address, whatever it is.

This is fast—nearly instantaneous—and cheap. It doesn't change the state of the repository, except to write a new object, which typically takes up 125 bytes. The new commit object is not attached to any refs and so will be garbage collected in due course. You can do it in the middle of a rebase. You can do it in the middle of a merge. You can do it with a dirty index or a dirty working tree. It always works.

(Well, not quite. It will fail if run in an empty repository, because there is no HEAD^{tree} yet. Probably there are some other similarly obscure failure modes.)

I called the shortcut git-push program git-pusho but I dropped the email-address-finder into git-get, which is my storehouse of weird “How do I find out X” tricks.

I wish my best work of the day had been a little bit more significant, but I'll take what I can get.

[ Addendum: Twitter user @shachaf has reminded me that the right way to do this is


which prints out something like

    Mark Jason Dominus (陶敏修) <> 1469102546 -0400

which you can then parse. @shachaf also points out that a Stack Overflow discussion of this very question contains a comment suggesting the same weird hack! ]

by Mark Dominus ( at July 21, 2016 08:25 AM

July 18, 2016

Neil Mitchell

Why did Stack stop using Shake?

Summary: Stack originally used Shake. Now it doesn't. There are reasons for that.

The Stack tool originally used the Shake build system, as described on the page about Stack's origins. Recently Edward Yang asked why doesn't Stack still use Shake - a very interesting question. I've taken the information shared in that mailing list thread and written it up, complete with my comments and distortions/inferences.

Stack is all about building Haskell code, in ways that obey dependencies and perform minimal rebuilds. Already in Haskell the dependency story is somewhat muddied. GHC (as available through ghc --make) does advanced dependency tracking, including header includes and custom Template Haskell dependency directives. You can also run ghc in single-shot mode, compiling a file at a time, but the result is about 3x slower and GHC will still do some dependency tracking itself anyway. Layered on top of ghc --make is Cabal which is responsible for tracking dependencies with .cabal files, configured Cabal information and placing things into the GHC package database. Layered on top of that is Stack, which has multiple projects and needs to track information about which Stackage snapshot is active and shared build dependencies.

Shake is good at taking complex dependencies and hiding all the messy details. However, for Stack many of these messy details were the whole purpose of the project. When Michael Snoyman and Chris Done were originally writing Stack they didn't have much experience with Shake, and opted to go for simplicity and directly managing the pieces, which they viewed to be less risky.

Now that Stack is written, and works nicely, the question changes to if it is worth changing existing working code to make use of Shake. Interestingly, at the heart of Stack there is a "Shake-lite" - see Control.Concurrent.Execute. This piece could certainly be replaced by Shake, but what would the benefit be? Looking at it with my Shake implementers hat on, there are a few things that spring to mind:

  • This existing code is O(n^2) in lots of places. For the size of Stack projects, compared to the time required to compile Haskell, that probably doesn't matter.

  • Shake persists the dependencies, but the Stack code does not seem to. Would that be useful? Or is the information already persisted elsewhere? Would Shake persisting the information make stack builds which had nothing to do go faster? (The answer is almost certainly yes.)

  • Since the code is only used on one project it probably isn't as well tested as Shake, which has a lot of tests. On the other hand, it has a lot less features, so a lot less scope for bugs.

  • The code makes a lot of assumptions about the information fed to it. Shake doesn't make such assumptions, and thus invalid input is less likely to fail silently.

  • Shake has a lot of advanced dependency forms such as resources. Stack currently blocks when simultaneous configures are tried, whereas Shake would schedule other tasks to run.

  • Shake has features such as profiling that are not worth creating for a single project, but that when bundled in the library can be a useful free feature.

In some ways Stack as it stands avoids a lot of the best selling points about Shake:

  • If you have lots of complex interdependencies, Shake lets you manage
    them nicely. That's not really the case for Stack, but is in large
    heterogeneous build systems, e.g. the GHC build system.

  • If you are writing things quickly, Shake lets you manage
    exceptions/retries/robustness quickly. For a project which has the
    effort invested that Stack does, that's less important, but for things
    like MinGHC (something Stack killed), it was critically important because no one cared enough to do all this nasty engineering.

  • If you are experimenting, Shake provides a lot of pieces (resources,
    parallelism, storage) that help explore the problem space without
    having to do lots of work at each iteration. That might mean Shake is
    more of a benefit at the start of a project than in a mature project.

If you are writing a version of Stack from scratch, I'd certainly recommend thinking about using Shake. I suspect it probably does make sense for Stack to switch to Shake eventually, to simplify ongoing maintenance, but there's no real hurry.

by Neil Mitchell ( at July 18, 2016 05:57 PM

Edward Z. Yang

What Template Haskell gets wrong and Racket gets right

Why are macros in Haskell terrible, but macros in Racket great? There are certainly many small problems with GHC's Template Haskell support, but I would say that there is one fundamental design point which Racket got right and Haskell got wrong: Template Haskell does not sufficiently distinguish between compile-time and run-time phases. Confusion between these two phases leads to strange claims like “Template Haskell doesn’t work for cross-compilation” and stranger features like -fexternal-interpreter (whereby the cross-compilation problem is “solved” by shipping the macro code to the target platform to be executed).

The difference in design can be seen simply by comparing the macro systems of Haskell and Racket. This post assumes knowledge of either Template Haskell, or Racket, but not necessarily both.

Basic macros. To establish a basis of comparison, let’s compare how macros work in Template Haskell as opposed to Racket. In Template Haskell, the primitive mechanism for invoking a macro is a splice:

{-# LANGUAGE TemplateHaskell #-}
module A where
val = $( litE (intPrimL 2) )

Here, $( ... ) indicates the splice, which runs ... to compute an AST which is then spliced into the program being compiled. The syntax tree is constructed using library functions litE (literal expression) and intPrimL (integer primitive literal).

In Racket, the macros are introduced using transformer bindings, and invoked when the expander encounters a use of this binding:

#lang racket
(define-syntax macro (lambda (stx) (datum->syntax #'int 2)))
(define val macro)

Here, define-syntax defines a macro named macro, which takes in the syntax stx of its usage, and unconditionally returns a syntax object representing the literal two (constructed using datum->syntax, which converts Scheme data into ASTs which construct them).

Template Haskell macros are obviously less expressive than Racket's (an identifier cannot directly invoke a macro: splices are always syntactically obvious); conversely, it is easy to introduce a splice special form to Racket (hat tip to Sam Tobin-Hochstadt for this code—if you are not a Racketeer don’t worry too much about the specifics):

#lang racket
(define-syntax (splice stx)
    (syntax-case stx ()
        [(splice e) #'(let-syntax ([id (lambda _ e)]) (id))]))
(define val (splice (datum->syntax #'int 2)))

I will reuse splice in some further examples; it will be copy-pasted to keep the code self-contained but not necessary to reread.

Phases of macro helper functions. When writing large macros, it's frequently desirable to factor out some of the code in the macro to a helper function. We will now refactor our example to use an external function to compute the number two.

In Template Haskell, you are not allowed to define a function in a module and then immediately use it in a splice:

{-# LANGUAGE TemplateHaskell #-}
module A where
import Language.Haskell.TH
f x = x + 1
val = $( litE (intPrimL (f 1)) ) -- ERROR
-- A.hs:5:26:
--     GHC stage restriction:
--       ‘f’ is used in a top-level splice or annotation,
--       and must be imported, not defined locally
--     In the splice: $(litE (intPrimL (f 1)))
-- Failed, modules loaded: none.

However, if we place the definition of f in a module (say B), we can import and then use it in a splice:

{-# LANGUAGE TemplateHaskell #-}
module A where
import Language.Haskell.TH
import B (f)
val = $( litE (intPrimL (f 1)) ) -- OK

In Racket, it is possible to define a function in the same file you are going to use it in a macro. However, you must use the special-form define-for-syntax which puts the function into the correct phase for a macro to use it:

#lang racket
(define-syntax (splice stx)
    (syntax-case stx ()
        [(splice e) #'(let-syntax ([id (lambda _ e)]) (id))]))
(define-for-syntax (f x) (+ x 1))
(define val (splice (datum->syntax #'int (f 1))))

If we attempt to simply (define (f x) (+ x 1)), we get an error “f: unbound identifier in module”. The reason for this is Racket’s phase distinction. If we (define f ...), f is a run-time expression, and run-time expressions cannot be used at compile-time, which is when the macro executes. By using define-for-syntax, we place the expression at compile-time, so it can be used. (But similarly, f can now no longer be used at run-time. The only communication from compile-time to run-time is via the expansion of a macro into a syntax object.)

If we place f in an external module, we can also load it. However, we must once again indicate that we want to bring f into scope as a compile-time object:

(require (for-syntax f-module))

As opposed to the usual (require f-module).

Reify and struct type transform bindings. In Template Haskell, the reify function gives Template Haskell code access to information about defined data types:

{-# LANGUAGE TemplateHaskell #-}
module A where
import Language.Haskell.TH
data Single a = Single a
$(reify ''Single >>= runIO . print >> return [] )

This example code prints out information about Single at compile time. Compiling this module gives us the following information about List:

TyConI (DataD [] A.Single [PlainTV a_1627401583]
   [NormalC A.Single [(NotStrict,VarT a_1627401583)]] [])

reify is implemented by interleaving splices and typechecking: all top-level declarations prior to a top-level splice are fully typechecked prior to running the top-level splice.

In Racket, information about structures defined using the struct form can be passed to compile-time via a structure type transformer binding:

#lang racket
(require (for-syntax racket/struct-info))
(struct single (a))
(define-syntax (run-at-compile-time stx)
  (syntax-case stx () [
    (run-at-compile-time e)
      #'(let-syntax ([id (lambda _ (begin e #'(void)))]) (id))]))
  (print (extract-struct-info (syntax-local-value (syntax single)))))

Which outputs:

'(.#<syntax:3:8 struct:single> .#<syntax:3:8 single>
   .#<syntax:3:8 single?> (.#<syntax:3:8 single-a>) (#f) #t)

The code is a bit of a mouthful, but what is happening is that the struct macro defines single as a syntax transformer. A syntax transformer is always associated with a compile-time lambda, which extract-struct-info can interrogate to get information about the struct (although we have to faff about with syntax-local-value to get our hands on this lambda—single is unbound at compile-time!)

Discussion. Racket’s compile-time and run-time phases are an extremely important idea. They have a number of consequences:

  1. You don’t need to run your run-time code at compile-time, nor vice versa. Thus, cross-compilation is supported trivially because only your run-time code is ever cross-compiled.
  2. Your module imports are separated into run-time and compile-time imports. This means your compiler only needs to load the compile-time imports into memory to run them; as opposed to Template Haskell which loads all imports, run-time and compile-time, into GHC's address space in case they are invoked inside a splice.
  3. Information cannot flow from run-time to compile-time: thus any compile-time declarations (define-for-syntax) can easily be compiled prior to performing expanding simply by ignoring everything else in a file.

Racket was right, Haskell was wrong. Let’s stop blurring the distinction between compile-time and run-time, and get a macro system that works.

Postscript. Thanks to a tweet from Mike Sperber which got me thinking about the problem, and a fascinating breakfast discussion with Sam Tobin-Hochstadt. Also thanks to Alexis King for helping me debug my extract-struct-info code.

Further reading. To learn more about Racket's macro phases, one can consult the documentation Compile and Run-Time Phases and General Phase Levels. The phase system is also described in the paper Composable and Compileable Macros.

by Edward Z. Yang at July 18, 2016 03:19 PM

July 16, 2016

JP Moresmau

Another Web-based Haskell IDE

After giving up on EclipseFP, I've worked a bit on haskell-ide-engine and leksah, contributing little things here and there to try to make the Haskell IDE ecosystem a little bit better. But at some point, I tried to update the GTK libraries on my Ubuntu machine to get leksah to run, and broke my whole desktop. Hours of fun followed to get back to a working system. So I thought again at my efforts last year to have a web based IDE for Haskell, because using the browser as the UI saves users a lot of pain, no UI libraries to install or update!

I started another little effort that I call "reload", both because it's another take on something I had started before and of course because it issues ":reload" commands to ghci when you change files. I have changes the setup, though. Now I use Scotty for the back end, with a REST API, and I use a pure Javascript front-end, with the Polymer library providing the web component framework and material design. I also use a web socket to send back GHCi results from the back end to the browser. I still use ghcid for the backend, maybe one day when haskell-ide-engine is released I can use that instead.

The functionality is fairly simple yet: there is a file browser on the left, and the editor (I'm using the ACE web editor) on the right. There is no save button, any change is automatically saved to disk (you use source version control, right?). On the server, there is a GHCi session for each cabal component in your project, and any change causes a reload, and you can see the errors/warnings in a menu and in the editor's annotations. You can build, run tests and benchmarks, and I've just added ":info" support. The fact that we're using GHCi makes it fast, but I'm sure there's loads of wrinkles to iron out still.

Anyway, if you're interested in a test ride, just clone from Github and get going!

by JP Moresmau ( at July 16, 2016 02:16 PM

July 15, 2016


Announcing MuniHac

We are happy to announce


Friday, September 2 – Sunday, September 4, 2016, Munich

This Hackathon is intended for everyone who is interested to write programs in Haskell, whether beginner or expert, whether hobbyist or professional.

In the tradition of other Haskell Hackathons such as ZuriHac, HacBerlin, UHac and many more, the plan is to bring together up to a hundred of Haskell enthusiasts to work together on any Haskell-related projects they like, to share experiences, and to learn new things.

This Hackathon is organized by TNG Technology Consulting GmbH and Well-Typed LLP.

Attendance is free of charge, but there is a limited capacity, so you must register!

We are going to set up a mentor program and special events for Haskell newcomers. So if you are a Haskell beginner, you are very much welcome! And if you’re an expert, we’d appreciate if you’d be willing to spend some of your time during the Hackathon mentoring newcomers. We will ask you about this during the registration process.

We’re also planning to have a number of keynote talks at the Hackathon. We’re going to announce these soon.

We hope to see you in Munich!

by andres at July 15, 2016 06:31 PM

Douglas M. Auclair (geophf)

1HaskellADay 1Liners June 2016

  • June 13th, 2016:
    You want this list: [1, -1, 1, -1, ...]
    How would you produce this value in #Haskell ?
    • Wai Lee Chin Feman @wchinfeman
      (set plop to be identity, and set transformstate to be (*) -1)
    • Philipp Maier @AkiiZedd `iterate negate 1
    • Patrick Mylund @pmylund concat $ repeat [1, (-1)]
      • Gary Fixler @gfixler No need for the parens in a list.
    • Jeff Foster @fffej and Kevin Meredith @Gentmen
      iterate (* (- 1)) 1
    • Spencer Janssen @spencerjanssen and Андреев Кирилл @nonaem00
      cycle [1, -1]
      • Philipp Maier @AkiiZedd:
        I’m curious: Since concat is O(n) wouldn’t it take more and more time depending on how many items you take?
      • Patrick Mylund @pmylund Looks like they compile to the same thing
      • Philipp Maier @AkiiZedd I’m actually surprised the compiler can optimise this away :o Thanks for showing me ddump-simpl!
      • Eyal Lotem @EyalL concat is foldr (++), not foldl. O(1) work is done to produce the next item. [1,-1]++([1,-1]++(...
    • David Turner @DaveCTurner I'd actually write 'cycle [1,-1]' but I like the elegant, alliterative obscurity of   'iterate negate 1'
    • Fatih Karakurt @karakfa alt=1:[-x|x<-alt]

by geophf ( at July 15, 2016 03:22 AM

July 14, 2016

Mark Jason Dominus

Surprising reasons to use a syntax-coloring editor

[ Danielle Sucher reminded me of this article I wrote in 1998, before I had a blog, and I thought I'd repatriate it here. It should be interesting as a historical artifact, if nothing else. Thanks Danielle! ]

I avoided syntax coloring for years, because it seemed like a pretty stupid idea, and when I tried it, I didn't see any benefit. But recently I gave it another try, with Ilya Zakharevich's `cperl-mode' for Emacs. I discovered that I liked it a lot, but for surprising reasons that I wasn't expecting.

I'm not trying to start an argument about whether syntax coloring is good or bad. I've heard those arguments already and they bore me to death. Also, I agree with most of the arguments about why syntax coloring is a bad idea. So I'm not trying to argue one way or the other; I'm just relating my experiences with syntax coloring. I used to be someone who didn't like it, but I changed my mind.

When people argue about whether syntax coloring is a good idea or not, they tend to pull out the same old arguments and dust them off. The reasons I found for using syntax coloring were new to me; I'd never seen anyone mention them before. So I thought maybe I'd post them here.

Syntax coloring is when the editor understands something about the syntax of your program and displays different language constructs in different fonts. For example, cperl-mode displays strings in reddish brown, comments in a sort of brick color, declared variables (in my) in gold, builtin function names (defined) in green, subroutine names in blue, labels in teal, and keywords (like my and foreach) in purple.

The first thing that I noticed about this was that it was easier to recognize what part of my program I was looking at, because each screenful of the program had its own color signature. I found that I was having an easier time remembering where I was or finding that parts I was looking for when I scrolled around in the file. I wasn't doing this consciously; I couldn't describe the color scheme any particular part of the program was, but having red, gold, and purple blotches all over made it easier to tell parts of the program apart.

The other surprise I got was that I was having more fun programming. I felt better about my programs, and at the end of the day, I felt better about the work I had done, just because I'd spent the day looking at a scoop of rainbow sherbet instead of black and white. It was just more cheerful to work with varicolored text than monochrome text. The reason I had never noticed this before was that the other coloring editors I used had ugly, drab color schemes. Ilya's scheme won here by using many different hues.

I haven't found many of the other benefits that people say they get from syntax coloring. For example, I can tell at a glance whether or not I failed to close a string properly—unless the editor has screwed up the syntax coloring, which it does often enough to ruin the benefit for me. And the coloring also slows down the editor. But the two benefits I've described more than outweigh the drawbacks for me. Syntax coloring isn't a huge win, but it's definitely a win.

If there's a lesson to learn from this, I guess it's that it can be valuable to revisit tools that you rejected, to see if you've changed your mind. Nothing anyone said about it was persuasive to me, but when I tried it I found that there were reasons to do it that nobody had mentioned. Of course, these reasons might not be compelling for anyone else.

Addenda 2016

Looking back on this from a distance of 18 years, I am struck by the following thoughts:

  1. Syntax higlighting used to make the editor really slow. You had to make a real commitment to using it or not. I had forgotten about that. Another victory for Moore’s law!

  2. Programmers used to argue about it. Apparently programmers will argue about anything, no matter how ridiculous. Well okay, this is not a new observation. Anyway, this argument is now finished. Whether people use it or not, they no longer find the need to argue about it. This is a nice example that sometimes these ridiculous arguments eventually go away.

  3. I don't remember why I said that syntax highlighting “seemed like a pretty stupid idea”, but I suspect that I was thinking that the wrong things get highlighted. Highlighters usually highlight the language keywords, because they're easy to recognize. But this is like highlighting all the generic filler words in a natural language text. The words you want to see are exactly the opposite of what is typically highlighted.

    Syntax highlighters should be highlighting the semantic content like expression boundaries, implied parentheses, boolean subexpressions, interpolated variables and other non-apparent semantic features. I think there is probably a lot of interesting work to be done here. Often you hear programmers say things like “Oh, I didn't see the that the trailing comma was actually a period.” That, in my opinion, is the kind of thing the syntax highlighter should call out. How often have you heard someone say “Oh, I didn't see that while there”?

  4. I have been misspelling “arguments” as “argmuents” for at least 18 years.

by Mark Dominus ( at July 14, 2016 03:15 PM

July 13, 2016

Christoph Breitkopf

IntervalMap Retrospective

IntervalMap, my package for containers with intervals as keys, has gone through several changes since its inception in late 2011. As is often the case, I had a concrete problem to solve and the initial code did that and only that. Going public on Hackage made some changes necessary. Others cropped up later in the desire to get closer to the interface and performance of the other base containers. Some were even requested by users. Here's a rough history:
0.12011-12Initial version
0.22011-12Name changes; Hackage release
0.32012-08Split into lazy and strict
0.42014-08Interval type class
0.4.12015-12IntervalSet added
0.52016-01Make interval search return submaps/subsets where appropriate

Looking back at this, what bugs me most is the late addition of sets, which were only added after a user requested it. Why didn't his come up right at the start? “interval-containers” would have been a better and more general package name.

The really big change - supporting user-defined intervals via a type class - was caused by my initial distrust of nonstandard language extensions. The result of this is one more level in the module structure for the now-preferred generic version, e.g.:

    import qualified Data.IntervalMap.Generic.Strict as IVM

What it still unclear is where to put the Interval type class. There are many useful interval data structures and using Data.Interval for this particular purpose would not be acceptable. But having it under IntervalMap does not seem right either. One option would be a name change:


Another is to use a general module:


Or even put everything under that module:


None of these seems clearly preferable, so the best option is probably to leave the package name and module structure as is.

Data Structure

Preferring simplicity, I based the implementation on Red-Black trees. While this is in general competitive with size balanced binary trees as used by the base containers, there is one caveat: with plain red-black trees, it is not possible to implement a hedge-union algorithm or even simple optimizations for the very common “union of huge set and tiny set” operation unless one would use an additional redundant size field in the node.

This has become somewhat more pressing since version 0.5 where the search operations return subsets/submaps.


My initial fixed type implementation of intervals allowed mixing intervals with different openness, and type class has inherited this “feature”. I highly suspect that no one actually uses this - that is, all in instances of Interval, leftClosed and rightClosed ignore their argument and have a constant value.

If I'm wrong, and someone does use this, please let me know!

That design has a negative impact on performance, though. It turns up in the ordering of intervals and their endpoints. For example, a lower bound is actually lower than the identical lower bound of a second interval, if the first interval is closed and the second open.

Unless the compiler does whole-program optimization, it will not be able to eliminate the Interval dictionaries, and can do very little optimization. That's the reason Interval has many members that could also have been defined as module-level functions: above, below, contains, ... These functions are heavily used by the map and set implementations, and it seems that GHC at least is much better at optimizing these functions when they are defined as members (this is just an observation of mine - I don't know in detail why this should be the case). The disadvantage is that it's possible to break a lot of invariants if you actually define these members in an instance. That would not be possible if they were defined as regular functions. At least, I'm in good company, because the same applies to Eq, Ord, and Monad to name just a few.

Data.Map tries to work around this by declaring many functions to be inlinable, effectively getting a bit closer to whole-program optimization. This does not seem feasible for IntervalMap, because the functions are used as deeper nesting, and in particular when constructing nodes.

As far as GHC is concerned, good performance is very dependent on inlining, especially when type classes and their dictionaries are involved. Any improvements in this would certainly benefit IntervalMap. One idea: it might be useful to be able to provide strictness information in type classes. In the case of Interval for example, lowerBound and upperBound always evaluate their argument (disregarding really pathological instances), but there is no way to indicate this to the compiler. Only the instance declarations allow inferring strictness information, and that's not available when compiling library code.


Whether a big refactoring or rewrite should be done really depends on the users of the package: you. Please let me know about missing features or performance issues, either via mail, a github issue, or a comment here.

by Christoph Breitkopf ( at July 13, 2016 10:45 AM

July 12, 2016

Mark Jason Dominus

A simple but difficult arithmetic puzzle

Lately my kids have been interested in puzzles of this type: You are given a sequence of four digits, say 1,2,3,4, and your job is to combine them with ordinary arithmetic operations (+, -, ×, and ÷) in any order to make a target number, typically 24. For example, with 1,2,3,4, you can go with $$((1+2)+3)×4 = 24$$ or with $$4×((2×3)×1) = 24.$$

We were stumped trying to make 6,6,5,2 total 24, so I hacked up a solver; then we felt a little foolish when we saw the solutions, because it is not that hard. But in the course of testing the solver, I found the most challenging puzzle of this type that I've ever seen. It is:

Given 6,6,5,2, make 17.

There are no underhanded tricks. For example, you may not concatenate 2 and 5 to make 25; you may not say and and concatenate 1 and 7 to make ; you may not interpret the 17 as a base 12 numeral, etc.

I hope to write a longer article about solvers in the next week or so.

by Mark Dominus ( at July 12, 2016 07:13 PM

July 11, 2016

Mark Jason Dominus

Addenda to recent articles 201607

Here are some notes on posts from the last couple of months that I couldn't find better places for.

  • I wrote a long article about tracking down a system bug. At some point I determined that the problem was related to Perl, and asked Frew Schmidt for advice. He wrote up the details of his own investigation, which pick up where mine ended. Check it out. I 100% endorse his lament about ltrace.

  • There was a Hacker News discussion about that article. One participant asked a very pertinent question:

    I read this, but seemed to skip over the part where he explains why this changed suddenly, when the behavior was documented?

    What changed to make the perl become capable whereas previously it lacked the low port capability?

    So far, we don't know! Frew told me recently that he thinks the TMPDIR-losing has been going on for months and that whatever precipitated my problem is something else.

  • In my article on the Greek clock, I guessed a method for calculating the (approximate) maximum length of the day from the latitude: $$ A = 360 \text{ min}\cdot(1-\cos L).$$

    Sean Santos of UCAR points out that this is inaccurate close to the poles. For places like Philadelphia (40° latitude) it is pretty close, but it fails completely for locations north of the Arctic Circle. M. Santos advises instead:

    $$ A = 360 \text{ min}\cdot \frac{2}{\pi}\cdot \sin^{-1}(\tan L\cdot \tan\epsilon)$$

    where ε is the axial tilt of the Earth, approximately 23.4°. Observe that when is above the Arctic Circle (or below the Antarctic) we have (because ) so the arcsine is undefined, and we get no answer.

by Mark Dominus ( at July 11, 2016 05:39 PM

Robert Harper

PCLSRING in Semantics

PCLSRING is an operating system kernel design technique introduced in ITS for managing interruptions of long-running synchronous system calls.  It was mentioned in an infamous diatribe by Dick Gabriel, and is described in loving detail by Allen Bawden in an article for the ages.

Discussions of PCLSRING usually center on fundamental questions of systems design.  Is the ITS approach better than the Unix approach?   Should the whole issue be avoided by using asynchronous system calls, as in VMS?  And weren’t the good old days better than the bad new days anyway?

Let’s set those things aside for now and instead consider what it is, rather than what it’s for or whether it’s needed.  The crux of the matter is this.  Suppose you’re working with a system such as Unix that has synchronous system calls for file I/O, and you initiate a “large” read of n bytes into memory starting at address a.  It takes a while to perform the transfer, during which time the process making the call may be interrupted for any number of reasons.  The question is, what to do about the process state captured at the moment of the interrupt?

For various reasons it doesn’t make sense to snapshot the process while it is running inside the kernel.  One solution is to simply stop the read “in the middle” and arrange that, when the process resumes, it returns from the system call indicating that some m<=n bytes have been read.  You’re supposed to check that m=n yourself anyway, and restart the call if not.  (This is the Unix solution.)  It is all too easy to neglect the check, and the situation is made the worse because so few languages have sum types which would make it impossible to neglect the deficient return.

PCLSRING instead stops the system call in place, backs up the process PC to the system call, but with the parameters altered to read n-m bytes into location a+m, so that when the process resumes it simply makes a “fresh” system call to finish the read that was so rudely interrupted.  The one drawback, if it is one, is that your own parameters may get altered during the call, so you shouldn’t rely on them being anything in particular after it returns.  (This is all more easily visualized in assembly language, where the parameters are typically words that follow the system call itself in memory.)

While lecturing at this year’s OPLSS, it occurred to me that the dynamics of Modernized Algol in PFPL, which is given in Plotkin’s style, is essentially the same idea.  Consider the rule for executing an encapsulated command:

if mm’, then bnd(cmd(m);x.m”)bnd(cmd(m’);x.m”)

(I have suppressed the memory component of the state, which is altered as well.)  The expression cmd(m) encapsulates the command m.  The bnd command executes m and passes its result to another command, m”, via the variable x.  The above rule specifies that a step of execution of m results in a reconstruction of the entire bnd, albeit encapsulating m’ , the intermediate result, instead of m.  It’s exactly PCLSRING!  Think of m as the kernel code for the read, think of cmd as the system call, and think of the bnd as the sequential composition of commands in an imperative language.  The kernel only makes partial progress executing m before being interrupted, leaving m’ remaining to be executed to complete the call.  The “pc” is backed up to the bnd, albeit modified with m’ as the new “system call” to be executed on the next transition.

I just love this sort of thing!  The next time someone asks “what the hell is PCLSRING?”, you now have the option of explaining it in one line, without any mention of operating systems.  It’s all a matter of semantics.



Filed under: Programming, Research, Teaching Tagged: operating systems, pclsring, structural operational semantics

by Robert Harper at July 11, 2016 05:34 PM

July 09, 2016

The GHC Team

Rethinking GHC's approach to managing proposals

Recently there has been a fair bit of discussion around the mechanisms by which proposed changes to GHC are evaluated. While we have something of a formal proposal protocol, it is not clearly documented, inconsistently applied, and may be failing to serve a significant fraction of GHC's potential contributor pool.

Over the last few weeks, I have been doing a fair amount of reading, thinking, and discussing to try to piece together a proposal scheme which better serves our community.

The resulting proposal is strongly inspired by the RFC process in place in the Rust community, the leaders of which have thought quite hard about fostering community growth and participation. While no process is perfect, I feel like the Rust process is a good starting point for discussion, offering enough structure to guide new contributors through the process while requiring only a modest investment of developer time.

To get a sense for how well this will work in our community, I propose that we attempt to self-host the proposed process. To this end I have setup a ghc-proposals repository and opened a pull request for discussion of the process proposal. Let's see how this goes.


~ Ben

by bgamari at July 09, 2016 08:41 PM

July 08, 2016

Roman Cheplyaka

Debugging a CUPS Forbidden error

When I try to install a printer on a fresh Fedora 24 system through the CUPS web interface (http://localhost:631/admin/), I get

Add Printer Error

Unable to add printer:


Here’s the relevant part of the config file, /etc/cups/cupsd.conf:

<Limit CUPS-Add-Modify-Printer CUPS-Delete-Printer CUPS-Add-Modify-Class CUPS-Delete-Class CUPS-Set-Default CUPS-Get-Devices>
  AuthType Default
  Require user @SYSTEM
  Order deny,allow

Now look at man cupsd.conf for the explanation:

Require user {user-name|@group-name} ...
     Specifies  that  an authenticated user must match one of the named
     users or be a member of one of the named groups.  The  group  name
     "@SYSTEM" corresponds to the list of groups defined by the System‐
     Group directive in the cups-files.conf(5) file.   The  group  name
     "@OWNER" corresponds to the owner of the resource, for example the
     person that submitted a print job.

Let’s look at /etc/cups/cups-files.conf and find out what those groups are:

SystemGroup sys root

Alright, so the solution is:

sudo usermod -a -G sys feuerbach

(where feuerbach is my username).

Frankly, I think it’s a bug that an admin user cannot add a printer by default, but luckily it’s not hard to fix.

July 08, 2016 08:00 PM

Brent Yorgey

Eastman maximal comma-free codes in Haskell

This past January I watched a video of Don Knuth’s most recent annual Christmas lecture. Typically his Christmas lectures have been about trees, but breaking with tradition, he gave this lecture about comma-free codes, and presented an implementation of an interesting algorithm due to Willard Eastman. Of course his implementation was written in CWEB, and during the course of the lecture he noted that his algorithm was iterative, and he didn’t know of a nice way to write it recursively (or something like that). Naturally, that sounded like a challenge, so I implemented it in Haskell, and I think it came out quite nicely. (It still uses “iteration” in the sense of the iterate function, but of course that uses recursion, so…?) Unfortunately, that was in January, it is now July, and I don’t really remember how it works. So I decided I had better write about it now, before I forget even more about how it works.

A comma-free code is a set C of strings such that if you concatenate any two strings in C, the result does not contain any elements of C as internal substrings. The term “comma-free” refers to the fact that sequences of strings from C can be unambiguously concatenated, without the need for separators like commas. Even if you start reading somewhere in the middle of a message, you can unambiguously figure out how to partition the message into codewords. For example, {bear, like} is a comma-free code, but {bear, like, earl} is not, since bearlike contains earl as a substring. A comma-free code also obviously cannot contain any periodic strings (that is, strings which consist of repeated copies of some shorter string), like abcabc, since concatenating such a string with itself produces a string containing the same string as an internal prefix.

Given a fixed alphabet and codeword length, one is naturally led to ask how large a comma-free code can possibly be. Eastman solved this problem for odd codeword lengths, by showing how to construct a maximal commafree code. To understand Eastman’s solution, consider the set S of all aperiodic strings of length n over an alphabet \Sigma (we have already seen that periodic strings cannot be part of a comma-free code). Consider two strings equivalent if they are rotations of each other. For example, bear, earb, arbe, and rbea are all equivalent. This is an equivalence relation on strings, and so it defines a partition of S into classes of equivalent strings. Note that we can never have two equivalent strings as part of the same comma-free code, since if we concatenate a string with itself, the result contains all other equivalent strings as substrings. For example, bearbear contains earb, arbe, and rbea. So at most a comma-free code could contain one string from each equivalence class.

In fact, Eastman shows that for odd n there are comma-free codes that contain exactly one string from each equivalence class! What’s more, his proof is constructive: he shows how to pick a particular, canonical representative from each equivalence class such that the collection of all such canonical representatives is a comma-free code. This is what the program below does: given an odd-length string, it outputs the canonical rotation of that string which is part of a maximal comma-free code.

So, without further ado, let’s see the implementation! Again, I really don’t remember much about the details of how (much less why) this works. For that, I recommend watching Knuth’s lecture or reading the explanations in his code (you’ll probably want to compile it into LaTeX first).

First, some imports and such. Look, ma, no LANGUAGE extensions!

> module Commafree where
> import           Control.Arrow      (first)
> import           Control.Monad      (when)
> import           Data.List          (findIndex, intercalate)
> import           Data.List.Split
> import           Data.Maybe         (catMaybes)
> import           Data.Monoid        ((<>))
> import           System.Environment
> import           System.Exit
> import           Text.Printf
> import           Text.Read          (readMaybe)

Here’s the main Eastman algorithm, which actually works for any list of things with a total order (unlike Knuth’s, which only works for lists of nonnegative integers, although that is obviously just a cosmetic difference, since any finite set with a total order is isomorphic to a set of nonnegative integers). We turn each item into a singleton “block”, then iterate the eastmanRound function, which partitions the blocks into subsequences of blocks, which we coalesce into blocks again. So each iteration makes the partition coarser, i.e. the blocks get bigger. We keep iterating until there is only one block left, which contains the rotation that we seek.

> eastman :: Ord a => [a] -> [a]
> eastman
>   = blockContent . head . head
>   . dropWhile ((>1) . length)
>   . iterate (map mconcat . eastmanRound)
>   . map mkBlock

Some code for dealing with blocks. A block is just a list that keeps track of its length for efficiency. The important point about blocks is that they are ordered first by length, then lexicographically (see the Ord instance below). The Monoid instance is straightforward.

> data Block a = Block { blockLen :: !Int, blockContent :: [a] }
>   deriving (Show, Eq)
> instance Ord a => Ord (Block a) where
>   compare (Block m as) (Block n bs)
>     = compare m n <> compare as bs
> instance Monoid (Block a) where
>   mempty = Block 0 []
>   mappend (Block m as) (Block n bs) = Block (m+n) (as ++ bs)
> mkBlock :: a -> Block a
> mkBlock a = Block 1 [a]

One round of the algorithm works as follows: we duplicate the list, partition it after each “dip” (chop splitDip, to be explained below), possibly drop some of the leading parts and coalesce other parts based on size parity (pickOdds), and then keep only a total amount of stuff equal to the length of the original list (takeTotal). This last part with takeTotal ensures that we will end up with something which is a rotation of the original input (though partitioned). In an implementation with random-access arrays, one would just wrap the indices around using mod; in this context it’s easier to first duplicate the input list so we can deal with all rotations at once, determine which rotation we want by dropping some stuff from the beginning, then drop any excess stuff at the end.

> eastmanRound :: Ord a => [a] -> [[a]]
> eastmanRound as
>   = takeTotal (length as)
>   . pickOdds
>   . chop splitDip
>   $ (as ++ as)

It’s interesting to note that in eastmanRound the type a is actually going to be instantiated with Block b for some type b. In the first round, all the blocks are singletons, so this is no different than just taking a list of b. But in subsequent rounds the distinction is nontrivial.

A “dip” is a decreasing substring followed by a single increase, for example, 976325. (Though again, remember that we are actually dealing with sequences of blocks, not integers, so a dip is essentially a sequence of blocks of decreasing length followed by a longer one, with the requisite caveat about blocks of the same length.) splitDip looks for the first place in the list that looks like a > b < c and breaks the list right after it. This is used with the chop function to split the list into a sequence of dips.

> splitDip :: Ord a => [a] -> ([a],[a])
> splitDip (a:b:cs)
>   | a < b     = ([a,b], cs)
>   | otherwise = first (a:) (splitDip (b:cs))
> splitDip as = (as,[])

pickOdds does something like the following: it looks for maximal sequences of dips where the first dip has odd length and the rest have even length, and merges such sequences into one long partition. It also drops everything prior to the first odd dip. Something like that at least; my memory on this is a bit fuzzy.

> pickOdds :: [[a]] -> [[a]]
> pickOdds
>   = map concat
>   . dropWhile (even . length . head)
>   . drop 1
>   . splitAtOdds
> splitAtOdds :: [[a]] -> [[[a]]]
> splitAtOdds = chop $
>   \(x:xs) -> let (ys,zs) = break (odd.length) xs
>              in  (x:ys, zs)

Finally, takeTotal just takes lists until their total length matches the given total.

> takeTotal :: Int -> [[a]] -> [[a]]
> takeTotal _ [] = []
> takeTotal n _ | n <= 0 = []
> takeTotal n (xs:xss) = xs : takeTotal (n - length xs) xss

And that’s it! I also put together a main which more or less emulates what Knuth’s C program does. My program and Knuth’s give the same output on every example I have tried (except that Knuth’s prints out some intermediate information about each iteration step; mine just prints the final answer).

> main :: IO ()
> main = do
>   progName <- getProgName
>   args <- getArgs
>   let n = length args
>   when (n < 3) $ do
>     printf "Usage: %s x1 x2 ... xn\n" progName
>     exitWith (ExitFailure 1)
>   when (even n) $ do
>     printf "The number of items, n, should be odd, not `%d'!\n" n
>     exitWith (ExitFailure 2)
>   let ns :: [Maybe Int]
>       ns = map readMaybe args
>   case findIndex (maybe True (<0) . snd) (zip [1..] ns) of
>     Just i -> do
>       printf "Argument %d should be a nonnegative integer, not `%s'!\n"
>                         i                             (args !! (i-1))
>       exitWith (ExitFailure 3)
>     Nothing ->
>       putStrLn .
>       (' ' :) . intercalate " " . map show .
>       eastman . catMaybes $ ns

by Brent at July 08, 2016 02:32 AM

July 06, 2016

Yesod Web Framework

Implementing HTTP/2 server push

What is HTTP/2 server push?

Server push is a hot topic of HTTP/2. Effective usage of server push can improve user experience. For instance, let's consider a scenario: downloading "index.html" which requires "style.css".

If a browser uses HTTP/1.1, it gets the "index.html" first, parses it, then obtains "style.css". So, two round-trip-times (RTTs) are necessary before the browser starts rendering.

On the other hand, if a browser uses HTTP/2 and the corresponding server supports server push, only one RTT is necessary. That is, when the browser send a GET request for "index.html", the server pushes "style.css" before it transfers "index.html". When the browser parses "index.html", it finds "style.css" in its local cache. Thus, it can start rendering at this timing.

APIs for server push

So, how can we implement HTTP/2 server push in Warp? Clearly, it is necessary for an application to tell Warp what files should be pushed. One way is to extend the Response type to store information on server push. But this breaks compatibility. We need to modify all existing applications.

To keep all existing types as is, I decided to use vault in the Request type. Vault is a heterogeneous infinite map which can store any type. Warp creates a new IORef and store its getter and setter to the vault:

getHTTP2Data :: Request -> IO (Maybe HTTP2Data)
setHTTP2Data :: Request -> Maybe HTTP2Data -> IO ()

HTTP2Data is the data type to store a list of files to be pushed. An application can set files to be pushed by setHTTP2Data. Warp retrieves them by getHTTP2Data and pushes them before sending the corresponding Response.

Note that the vault is a part of Web Application Interface (WAI) but these two functions are not. They are APIs provided only by Warp.

Middleware for server push

The next question is how an application knows which files to be pushed for a given URL. One way is manifest files.

Another way is learning based on Referer:. This idea came from Jetty. Typically, there is the Referer: whose value is, say,", in a GET request to "style.css". So, analyzing requests for a while, we can learn that "style.css" should be pushed when "index.html" is requested.

@davean suggested that I implement this mechanism as a middleware. So, I created a middleware for HTTP/2 server push based on Referer:. Its default behavior for a given Request and Response is as follows:

  • If files to be pushed are found for a given path in a learning dictionary, set them by setHTTP2Data.
  • Otherwise, register the file of Response to the learning dictionary only when the following conditions are met:
  1. The Request stores a valid Referer:
  2. The Response is a file type
  3. The path of Referer: is "/" or ends with ".html"/".html"
  4. The path ends with ".js" and ".css"

The learning dictionary is cleared every 30 seconds.

Warp v3.2.7 with the push APIs and wai-http2-extra v0.0.0 with the middleware are already on Hackage. If you implement a server push middleware based on manifest files, please send a pull request on github.


Here are screen shots of Firefox accessing the new Warp. The first figure is the first access and the middleware has not learned anything. So, no pushes are used.

Figure 1: Download time-line without server push

The second figure is the second access. You can see .js and .css files are pushed since bullets are not green.

Figure 2: Download time-line with server push

Next Step

The next step would be an implementation of Cache Digests for HTTP/2. In this scheme, a browser can tell a list of cached file to a server. So, the server can avoid unnecessary pushes.


Efforts to bring HTTP/2 server push feature to Warp was originally made by Andrew Pritchard. Without his experience and suggestions, this work would be impossible. I thank him deeply.

July 06, 2016 07:10 AM

The team


By the team: Chris Done, Chris Allen, Julie Moronuki, Michael Snoyman, Sibi Prabakaran, Gabriel Gonzalez

We are happy to announce the launch of a new Haskell community nexus site: This website is aimed at providing modern best practices information for the Haskell programming language, and in particular with providing the best possible new user experience. The aim is to lower the barrier to getting started with Haskell, and ultimately increase adoption of Haskell in the greater programming community.

The launch of this website is paired with the launch of a number of additional community resources to aid its growth:

These community resources are open to all to discuss the contents of the website, and more broadly how to make Haskell as welcoming a language, community, and ecosystem as can be managed. We encourage all Haskellers to join, and to take part in lively discussions of how to improve the state of the art within Haskell.

As this community is just forming, now is the perfect time to get involved. Post questions and comments on Reddit, Tweet to us, send pull requests for the website, and open issues. This community will become what you put into it, so help shape it from the beginning!

Why a new site?

Since it is a common question in such statements, let us ask it directly here: why create a new website instead of working to incrementally update In the opinion of the team behind, the tooling story and general ecosystem infrastructure for the Haskell community has accumulated enough baggage that a clean break is the best use of everybody's time. We intend to streamline the on-boarding process for new developers, move away from infrastructure that is showing its age, and embrace newer approaches to facilitate open collaboration. Similar decisions have already been made in creating the Stack build tool and Stackage.

July 06, 2016 12:00 AM

July 05, 2016

Joachim Breitner

HaL deadline extended

There is this long-running workshop series Haskell in Leipzig, which is a meeting of all kinds of Haskell-interested folks (beginners, experts, developers, scientists), and for year’s instance, HaL 2016, I have the honour of being the program committee chair.

The original deadline passed last week, and after looking through the submissions it became clear that although the quality was good, the quantitiy was still lacking. I therefore extended the submission deadline by two weeks, until July 15th.

So if you have something worth talking about, please do submit a proposal1 and come to Leipzig!.

Why should you submit here? Because it gives you a platform to talk about your ideas to an audience that usually does not consist just of your fellow speakers, as it is often with purely academic workshops, but “real” listeners of various kinds. And it is a fun event.

And why should you come to Leipzig? Because of all the interesting talks and tutorials! Of course I cannot say a lot here yet, besides that our invited speaker Alejandro Russo from Chalmers and Gothenburg University will present his work on information-flow control in Haskell (i.e., SecLib, LIO, MAC, HLIO).

  1. And if you want to save me from sleepless nights, submit the first version a few days before the deadline…

by Joachim Breitner ( at July 05, 2016 05:40 PM

Gabriel Gonzalez

Auto-generate service API endpoints from records

Haskell has pretty cool support for code generation from data type definitions using GHC generics. So I thought: "why not generate a service from a data type?".

The basic idea is pretty simple. Given a data type definition like this:

data Command
= Create { filepath :: FilePath, contents :: String }
| Delete { filepath :: FilePath }

... we'll auto-generate two API endpoints:

  • /create?filepath=:string&contents=:string
  • /delete?filepath=:string

Each endpoint accepts query parameters matching the fields for their respective constructors:

$ curl 'localhost:8080/create?filepath=test.txt&contents=ABC'
"File created"
$ cat test.txt
$ curl 'localhost:8080/delete?filepath=test.txt'
"File deleted"
$ cat test.txt
cat: test.txt: No such file or directory

The complete code to build the server looks like this:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}

import Server.Generic
import System.Directory (removeFile)

data Command
= Create { filepath :: FilePath, contents :: String }
| Delete { filepath :: FilePath }
deriving (Generic, ParseRecord)

handler :: Command -> IO String
handler (Create file text) = do
writeFile file text
return "File created"
handler (Delete file) = do
removeFile file
return "File deleted"

main :: IO ()
main = serveJSON 8080 handler

You can test it yourself by running:

$ stack build server-generic
$ stack runghc AboveExample.hs

... and then in a separate terminal you can hit each endpoint with curl as illustrated above.

GHC Generics

The Haskell magic is in this one line of code:

    deriving (Generic, ParseRecord)

This auto-generates code that tells the server how to marshal the route and query parameters into our Command data type. All we have to do is supply a handler that pattern matches on the incoming Command to decide what to do:

handler :: Command -> IO String
handler (Create file text) = do
writeFile file text
return "File created"
handler (Delete file) = do
removeFile file
return "File deleted"

You can read that as saying:

  • "If a client hits the /create endpoint, create the specified file"
  • "If a client hits the /delete endpoint, delete the specified file"

As an exercise, you can try modifying the handler to respond with the name of the file that was created or deleted.

However, you're not limited to query parameters. You can also parse data from path tokens by just omitting field labels from the data type:

{-# LANGUAGE DeriveGeneric #-}

import Server.Generic

data Command
= Add Double Double
| Multiply Double Double
deriving (Generic)

instance ParseRecord Command

handler :: Command -> IO Double
handler (Add x y) = return (x + y)
handler (Multiply x y) = return (x * y)

main :: IO ()
main = serveJSON 8080 handler

If you run the above code, you get a server that has two endpoints:

  • /add/:double/:double
  • /multiply/:double/:double

You can run the server and test that they work:

$ curl 'localhost:8080/add/2/3'
$ curl 'localhost:8080/multiply/2/3'

This library also intelligently handles optional and repeated fields in data type definitions. For example, suppose we serve this data type::

{-# LANGUAGE DeriveGeneric  #-}
{-# LANGUAGE DeriveAnyClass #-}

import Server.Generic

data Example = Example
{ list :: [Int]
, optional :: Maybe Int
, first :: First Int
, last :: Last Int
} deriving (Generic, ParseRecord, ToJSON)

handler :: Example -> IO Example
handler = return -- Serve decoded value back to client as JSON

main :: IO ()
main = serveJSON 8080 handler

... then the server will echo back the decoded type as JSON, correctly handling absent or repeated fields:

$ curl 'localhost:8080/example'
$ curl 'localhost:8080/example?optional=1&list=1&list=2&first=1&first=2&last=1&last=2'

Also, these repeated and optional annotations work for path components, too, in case you were wondering:

{-# LANGUAGE DeriveGeneric  #-}
{-# LANGUAGE DeriveAnyClass #-}

import Server.Generic

data Example = Example [Int] (Maybe Text)
deriving (Generic, ParseRecord, ToJSON)

handler :: Example -> IO Example
handler = return

main :: IO ()
main = serveJSON 8080 handler

The above server does "the right thing" and doesn't need to be told where the Ints end and the Text begins:

$ curl 'localhost:8080/example'
$ curl 'localhost:8080/example/1/2/foo'
$ curl 'localhost:8080/example/1/2/3'
$ curl 'localhost:8080/example/foo'

The server uses backtracking when parsing the route so the server knows when the Ints end and the Text begins.


The whole thing is strongly typed, which means several things in the context of service programming.

For example, if you define a data type that expects an Int field, then by golly your handler will get an Int field or the server will automatically reject the request for you. You don't have to worry about checking that the field is present nor do you need to validate that the parameter decodes to an Int correctly. If you want the parameter to be optional then you need to make that explicit by marking the field as type Maybe Int.

You also don't have to handle fields that belong to other endpoints. Each endpoint only gets exactly the fields it requested; no more, no less. If a given endpoint gets the wrong set of path tokens or query parameters then the server rejects the request for you.

This is also strongly typed in the sense that more logic is pushed into the type and less logic goes in the handler. If you want just the first or last occurrence of a query parameter, you just annotate the type with First or Last, respectively. The more logic you push into declarative type-level programming the more you distill your handler to focus on business logic.


I wrote this library to provide a quick an easy way to spin up Haskell web services but the library could still use some improvement. I'm not really a web developer so I only kind of know what I'm doing and could use help from people more knowledgeable than me.

The most notable deficiency is that the library does not take care to serve proper HTTP status codes for different types of errors. Every failed request returns a 404 status code.

Also, if the route is malformed the error message is a completely unhelpful "404 Not Found" error message that doesn't indicate how to fix the error.

Another blatant deficiency is that the server completely ignores the request method. I wasn't sure how to design this to work within the framework of data type generic programming.

If you have ideas about how to improve things I would greatly welcome any contributions.


People familiar with Haskell will recognize that this library resembles the servant library in some respects. The high-level difference is that this is a subset of servant that is much simpler but also significantly less featureful. For example, servant can also generate client-side bindings and Swagger resource declarations and servant also permits a much greater degree of customization.

This library focuses primarily on simple quick-and-dirty services; for anything more polished and production-ready you will probably want to try other Haskell service libraries. I just wanted to make it as easy as possible for people to get started with back-end development in Haskell and also show off how cool and powerful GHC generics can be.

If you would like to learn more about this library you can read the tutorial or if you would like to use the library you can obtain the code from Hackage or Github.

by Gabriel Gonzalez ( at July 05, 2016 01:45 PM

Neil Mitchell

More space leaks: Alex/Happy edition

Summary: Alex and Happy had three space leaks, now fixed.

Using the techniques described in my previous blog post I checked happy and alex for space leaks. As expected, both had space leaks. Three were clear and unambiguous space leaks, two were more nuanced. In this post I'll describe all five, starting with the obvious ones.

1: Happy - non-strict accumulating fold

Happy contains the code:

indexInto :: Eq a => Int -> a -> [a] -> Maybe Int
indexInto _ _ [] = Nothing
indexInto i x (y:ys) | x == y = Just i
| otherwise = indexInto (i+1) x ys

This code finds the index of an element in a list, always being first called with an initial argument of 0. However, as it stands, the first argument is a classic space leak - it chews through the input list, building up an equally long chain of +1 applications, which are only forced later.

The fix is simple, change the final line to:

let j = i + 1 in j `seq` indexInto j x ys

Or (preferably) switch to using the space-leak free Data.List.elemIndex. Fixed in a pull request.

2: Happy - sum using foldr

Happy also contained the code:

foldr (\(a,b) (c,d) -> (a+b,b+d)) (0,0) conflictList

The first issue is that the code is using foldr to produce a small atomic value, when foldl' would be a much better choice. Even after switching to foldl' we still have a space leak because foldl' only forces the outer-most value - namely just the pair, not the Int values inside. We want to force the elements inside the pair so are forced into the more painful construction:

foldl' (\(a,b) (c,d) ->
let ac = a + c; bd = b + d
in ac `seq` bd `seq` (ac,bd))
(0,0) conflictList

Not as pleasant, but it does work. In some cases people may prefer to define the auxiliary:

let strict2 f !x !y = f x y
in foldr (\(a,b) (c,d) -> strict2 (,) (a+b) (b+d)) (0,0) conflictList

Fixed in a pull request.

3: Alex - lazy state in a State Monad

Alex features the code:

N $ \s n _ -> (s, addEdge n, ())

Here N roughly corresponds to a state monad with 2 fields, s and n. In this code n is a Map, which operates strictly, but the n itself is not forced until the end. We solve the problem by forcing the value before returning the triple:

N $ \s n _ -> let n' = addEdge n in n' `seq` (s, n', ())

Fixed in a pull request.

4: Alex - array freeze

Alex calls the Data.Array.MArray.freeze function, to convert an STUArray (unboxed mutable array in the ST monad) into a UArray (unboxed immutable array). Unfortunately the freeze call in the array library uses an amount of stack proportional to the size of the array. Not necessarily a space leak, but not ideal either. Looking at the code, it's also very inefficient, constructing and deconstructing lots of intermediate data. Fortunately under normal optimisation a rewrite rule fires for this type to replace the call with one to freezeSTUArray, which is much faster and has bounded stack, but is not directly exported.

Usually I diagnose space leaks under -O0, on the basis that any space leak problems at -O0 may eventually cause problems anyway if an optimisation opportunity is lost. In this particular case I had to -O1 that module.

5: Happy - complex fold

The final issue occurs in a function fold_lookahead, which when given lists of triples does an mconcat on all values that match in the first two components. Using the extra library that can be written as:

map (\((a,b),cs) -> (a,b,mconcat cs)) .
groupSort .
map (\(a,b,c) -> ((a,b),c))

We first turn the triple into a pair where the first two elements are the first component of the pair, call groupSort, then mconcat the result. However, in Happy this construction is encoded as a foldr doing an insertion sort on the first component, followed by a linear scan on the second component, then individual mappend calls. The foldr construction uses lots of stack (more than 1Mb), and also uses an O(n^2) algorithm instead of O(n log n).

Alas, the algorithms are not identical - the resulting list is typically in a different order. I don't believe this difference matters, and the tests all pass, but it does make the change more dangerous than the others. Fixed in a pull request.

The result

Thanks to Simon Marlow for reviewing and merging all the changes. After these changes Happy and Alex on the sample files I tested them with use < 1Kb of stack. In practice the space leaks discovered here are unlikely to materially impact any real workflows, but they probably go a bit faster.

by Neil Mitchell ( at July 05, 2016 12:43 PM

Philip Wadler

Roseburn to Leith Walk Cycleway: the website

There is a new website in support of the Roseburn to Leith Walk Cycleway. I especially like their promise to be evidence-based and to cover both sides, something increasingly rare in political discourse.
We are an informal association of local residents working to get the best for our community from the Proposed Cycle Route.  We've spent hundreds of hours gathering the facts.
  1. Even if you don't cycle, the Cycle Route has big benefits for you
  2. Common concerns don't match the facts
  3. The Council's latest revised design has addressed key concerns.

Our promise

Our site is evidence-based, including the disadvantages.  We are ready to engage in discussion with anyone.  Tell us about errors or omissions and we'll fix them as soon as we can.

Our goals

  • Get the best for all residents. This is not a website advocating cycling.  It's true that many of the founders do cycle, and many of us also drive.
  • Make decisions based on the facts.  We are concerned how many people are voicing fears and criticisms yet don't seem to know about some of the most important data and studies.
  • Listen to all views, and bring people together for discussion.  We don't accept the whole notion of classifying people as 'cyclists' and 'drivers'.  We are all ordinary people who use a variety of means of travel appropriate to different situations.

by Philip Wadler ( at July 05, 2016 09:38 AM

Yesod Web Framework

New http-client and mono-traversable releases

I'm happy to announce the release of a number of packages today, but mostly this comes down to upgrades to http-client and mono-traversable. This blog post will cover the main changes you should be aware of it you are using one of these two packages. In addition to these two packages, the following related packages are being released as well: http-client-tls, http-client-openssl, http-conduit, mono-traversable-instances, minlen, chunked-data, conduit-combinators, mutable-containers, classy-prelude, classy-prelude-conduit, classy-prelude-yesod.


http-client is an HTTP client library leveraged by a number of other packages, including http-conduit, pipes-http, and wreq. This release is mostly about addressing issue #193, about an controversial design decision to throw runtime exceptions on non-successful HTTP response statuses. If you want a quick explanation of what's changed and what you should do:

  • If the HTTP server you're talking to gives a non-success HTTP response status (e.g., 404 not found), you will no longer get a runtime exception by default.

    • If you want the old behavior, switch to the parseUrlThrow function
    • The parseUrl function remains with the old behavior, but is deprecated in favor of parseRequest
    • The IsString instance has also switched to the non-throwing behavior
  • In an effort to make the remaining exceptions more useful, and avoid people accidentally relying on the old exception behavior, there's a new structure to the HttpException type. In particular, almost all exceptions are now contained in the HttpExceptionContent type, and will be wrapped up with the HttpExceptionRequest constructor, which provies information on the Request used to generate the exception. Hopefully this will make for much more useful error messages.

Based on the feedback I've received, this should bring the default behavior for http-client into line with what people expect, and will hopefully have a minimal impact of migration for existing users relying on the current behavior.


The mono-traversable package provides a typeclass hierarchy based around the idea of monomorphic containers. This allows, for examples, a unified foldMap function that works on lists, ByteStrings, and unboxed vectors, as well as abstractions over sequences (functions like break and drop) and containers (Maps and Sets).

I laid out a plan for a cleanup of the mono-traversable package. Most of the changes here were minor, and will not affect end users. Of import:

  • The mono-traversable package itself has much reduced dependencies, by putting a number of instances into the new mono-traversable-instances package.
  • A few typeclasses that used to live in chunked-data have moved to mono-traversable
  • The Data.NonNull module is much simpler, and no longer based on Data.MinLen (which lives on in the minlen package)


Mostly, classy-prelude is just inheriting the upstream changes in mono-traversable. The only other point I'd like to make about this classy-prelude release is that it is switching over to the new safe-exceptions package, which I recently announced on the FP Complete blog.

Mega repo

To simplify maintenance, and address a common problem of people not knowing which repo to report issues to, I've combined a few repos together into a mono-traversable mega-repo:

  • classy-prelude (and -conduit and -yesod)
  • chunked-data
  • mutable-containers

I've updated the old repo locations with a final commit pointing to the new location.

July 05, 2016 06:15 AM

July 04, 2016

Ken T Takusagawa

[vuqzjhmd] Heptagon

rainbow heptagon

Rainbow-shaded regular heptagon.  The source code below draws it in two different ways. It is unfortunate that the JuicyPixels Codec.Picture generateImage mapPixels encodePng pipeline (implemented in the function heptagonpic) is not lazy.  A 32000 by 32000 image ran out of memory.  The alternative route, outputting a Netpbm PPM (implemented in the function heptagon) then piping standard output to pnmtopng worked just fine.

There is a curious optical illusion of radial spikes, especially in the red and cyan.

Source code in Haskell.

by Ken ( at July 04, 2016 09:51 PM

Dominic Steinitz

Modelling an Ecosystem via Hamiltonian Monte Carlo


Recall from the previous post that the Hare growth parameter undergoes Brownian motion so that the further into the future we go, the less certain we are about it. In order to ensure that this parameter remains positive, let’s model the log of it to be Brownian motion.

\displaystyle   \begin{aligned}  \frac{\mathrm{d}N_1}{\mathrm{d}t} & = & \rho_1 N_1 \bigg(1 - \frac{N_1}{K_1}\bigg) - c_1 N_1 N_2 \\  \frac{\mathrm{d}N_2}{\mathrm{d}t} & = & -\rho_2 N_2 \bigg(1 + \frac{N_2}{K_2}\bigg) + c_2 N_1 N_2 \\  \mathrm{d} \rho_1 & = & \rho_1 \sigma_{\rho_1} \mathrm{d}W_t  \end{aligned}

where the final equation is a stochastic differential equation with W_t being a Wiener process.

By Itô we have

\displaystyle   \mathrm{d} (\log{\rho_1}) = - \frac{\sigma_{\rho_1}^2}{2} \mathrm{d} t + \sigma_{\rho_1} \mathrm{d}W_t

Again, we see that the populations become noisier the further into the future we go.


Now let us infer the growth rate using Hamiltonian Monte Carlo and the domain specific probabilistic language Stan (Stan Development Team (2015b), Stan Development Team (2015a), Hoffman and Gelman (2014), Carpenter (2015)). Here’s the model expressed in Stan.

functions {
  real f1 (real a, real k1, real b, real p, real z) {
    real q;

    q = a * p * (1 - p / k1) - b * p * z;
    return q;

  real f2 (real d, real k2, real c, real p, real z) {
    real q;

    q = -d * z * (1 + z / k2) + c * p * z;
    return q;

data {
  int<lower=1> T;   // Number of observations
  real y[T];        // Observed hares
  real k1;          // Hare carrying capacity
  real b;           // Hare death rate per lynx
  real d;           // Lynx death rate
  real k2;          // Lynx carrying capacity
  real c;           // Lynx birth rate per hare
  real deltaT;      // Time step

parameters {
  real<lower=0> mu;
  real<lower=0> sigma;
  real<lower=0> p0;
  real<lower=0> z0;
  real<lower=0> rho0;
  real w[T];

transformed parameters {
  real<lower=0> p[T];
  real<lower=0> z[T];
  real<lower=0> rho[T];

  p[1] = p0;
  z[1] = z0;
  rho[1] = rho0;

  for (t in 1:(T-1)){
    p[t+1] = p[t] + deltaT * f1 (exp(rho[t]), k1, b, p[t], z[t]);
    z[t+1] = z[t] + deltaT * f2 (d, k2, c, p[t], z[t]);

    rho[t+1] = rho[t] * exp(sigma * sqrt(deltaT) * w[t] - 0.5 * sigma * sigma * deltaT);

model {
  mu    ~ uniform(0.0,1.0);
  sigma ~ uniform(0.0, 0.5);
  p0    ~ lognormal(log(100.0), 0.2);
  z0    ~ lognormal(log(50.0), 0.1);
  rho0  ~ normal(log(mu), sigma);
  w     ~ normal(0.0,1.0);

  for (t in 1:T) {
    y[t] ~ lognormal(log(p[t]),0.1);

Let’s look at the posteriors of the hyper-parameters for the Hare growth parameter.

Again, the estimate for \mu is pretty decent. For our generated data, \sigma =0 and given our observations are quite noisy maybe the estimate for this is not too bad also.

Appendix: The R Driving Code

All code including the R below can be downloaded from github.


rm(list = ls(all.names=TRUE))

try(detach(package:RBi, unload = TRUE), silent = TRUE)
library(RBi, quietly = TRUE)


library('ggplot2', quietly = TRUE)
library('gridExtra', quietly = TRUE)

endTime <- 50

PP <- bi_model("")
synthetic_dataset_PP <- bi_generate_dataset(endtime=endTime,
                                            add_options = list(

rdata_PP <- bi_read(synthetic_dataset_PP)

df <- data.frame(rdata_PP$P$nr,

ggplot(df, aes(rdata_PP$P$nr, y = Population, color = variable), size = 0.1) +
    geom_line(aes(y = rdata_PP$P$value, col = "Hare"), size = 0.1) +
    geom_line(aes(y = rdata_PP$Z$value, col = "Lynx"), size = 0.1) +
    geom_point(aes(y = rdata_PP$P_obs$value, col = "Observations"), size = 0.1) +
    theme(legend.position="none") +
    ggtitle("Example Data") +
    xlab("Days") +
          axis.title=element_text(size=6,face="bold")) +
    theme(plot.title = element_text(size=10))

rstan_options(auto_write = TRUE)
options(mc.cores = parallel::detectCores())

lvStanModel <- stan_model(file = "SHO.stan",verbose=TRUE)

lvFit <- sampling(lvStanModel,
                  data=list(T = length(rdata_PP$P_obs$value),
                            y = rdata_PP$P_obs$value,
                            k1 = 2.0e2,
                            b  = 2.0e-2,
                            d  = 4.0e-1,
                            k2 = 2.0e1,
                            c  = 4.0e-3,
                            deltaT = rdata_PP$P_obs$time[2] - rdata_PP$P_obs$time[1]

samples <- extract(lvFit)

gs1 <- qplot(x = samples$mu, y = ..density.., geom = "histogram") + xlab(expression(\mu))
gs2 <- qplot(x = samples$sigma, y = ..density.., geom = "histogram") + xlab(expression(samples$sigma))
gs3 <- grid.arrange(gs1, gs2)

synthetic_dataset_PP1 <- bi_generate_dataset(endtime=endTime,
                                             init = list(P = 100, Z=50),
                                             add_options = list(

rdata_PP1 <- bi_read(synthetic_dataset_PP1)

synthetic_dataset_PP2 <- bi_generate_dataset(endtime=endTime,
                                             init = list(P = 150, Z=25),
                                             add_options = list(

rdata_PP2 <- bi_read(synthetic_dataset_PP2)

df1 <- data.frame(hare = rdata_PP$P$value,
                  lynx = rdata_PP$Z$value,
                  hare1 = rdata_PP1$P$value,
                  lynx1 = rdata_PP1$Z$value,
                  hare2 = rdata_PP2$P$value,
                  lynx2 = rdata_PP2$Z$value)

ggplot(df1) +
    geom_path(aes(x=df1$hare,  y=df1$lynx, col = "0"), size = 0.1) +
    geom_path(aes(x=df1$hare1, y=df1$lynx1, col = "1"), size = 0.1) +
    geom_path(aes(x=df1$hare2, y=df1$lynx2, col = "2"), size = 0.1) +
    theme(legend.position="none") +
    ggtitle("Phase Space") +
    xlab("Hare") +
    ylab("Lynx") +
          axis.title=element_text(size=6,face="bold")) +
    theme(plot.title = element_text(size=10))

PPInfer <- bi_model("")

bi_object_PP <- libbi(client="sample", model=PPInfer, obs = synthetic_dataset_PP)

bi_object_PP$run(add_options = list(
                     "end-time" = endTime,
                     noutputs = endTime,
                     nsamples = 2000,
                     nparticles = 128,
                     nthreads = 1),
                 verbose = TRUE,
                 stdoutput_file_name = tempfile(pattern="pmmhoutput", fileext=".txt"))


mu <- bi_read(bi_object_PP, "mu")$value
g1 <- qplot(x = mu[2001:4000], y = ..density.., geom = "histogram") + xlab(expression(mu))
sigma <- bi_read(bi_object_PP, "sigma")$value
g2 <- qplot(x = sigma[2001:4000], y = ..density.., geom = "histogram") + xlab(expression(sigma))
g3 <- grid.arrange(g1, g2)

df2 <- data.frame(hareActs = rdata_PP$P$value,
                  hareObs  = rdata_PP$P_obs$value)

ggplot(df, aes(rdata_PP$P$nr, y = value, color = variable)) +
    geom_line(aes(y = rdata_PP$P$value, col = "Phyto")) +
    geom_line(aes(y = rdata_PP$Z$value, col = "Zoo")) +
    geom_point(aes(y = rdata_PP$P_obs$value, col = "Phyto Obs"))

ln_alpha <- bi_read(bi_object_PP, "ln_alpha")$value

P <- matrix(bi_read(bi_object_PP, "P")$value,nrow=51,byrow=TRUE)
Z <- matrix(bi_read(bi_object_PP, "Z")$value,nrow=51,byrow=TRUE)

data50 <- bi_generate_dataset(endtime=endTime,
                              add_options = list(

rdata50 <- bi_read(data50)

df3 <- data.frame(days = c(1:51), hares = rowMeans(P), lynxes = rowMeans(Z),
                                  actHs = rdata50$P$value, actLs = rdata50$Z$value)

ggplot(df3) +
    geom_line(aes(x = days, y = hares, col = "Est Phyto")) +
    geom_line(aes(x = days, y = lynxes, col = "Est Zoo")) +
    geom_line(aes(x = days, y = actHs, col = "Act Phyto")) +
    geom_line(aes(x = days, y = actLs, col = "Act Zoo"))


Carpenter, Bob. 2015. “Stan: A Probabilistic Programming Language.” Journal of Statistical Software.

Hoffman, Matthew D., and Andrew Gelman. 2014. “The No-U-Turn Sampler: Adaptively Setting Path Lengths in Hamiltonian Monte Carlo.” Journal of Machine Learning Research.

Stan Development Team. 2015a. Stan Modeling Language User’s Guide and Reference Manual, Version 2.10.0.

———. 2015b. “Stan: A C++ Library for Probability and Sampling, Version 2.10.0.”

by Dominic Steinitz at July 04, 2016 12:31 PM

July 03, 2016

Gabriel Gonzalez

list-transformer - A beginner-friendly ListT

Currently, Hackage has four implementations of "ListT-done-right" that I'm aware of:

  • LogicT
  • pipes (which provides a ListT type)
  • list-t
  • List

However, I felt that all of these libraries were more complex than they needed to be so I tried to distill them down to the simplest library possible. I want to encourage more people to use ListT so I'm releasing the beginner-friendly list-transformer library .

There are a few design choices I made to improve the new user experience for this library:

First, the ListT data type is not abstract and users are encouraged to use constructors to both assemble and pattern match on ListT values. This helps them build an intuition for how ListT works under the hood since the type is small and not difficult to use directly:

newtype ListT m a = ListT { next :: m (Step m a) }

data Step m a = Cons a (ListT m a) | Nil

Second, the API is tiny in order to steer users towards leaning on Haskell's "collections API" as much as possible. Specifically, I try to direct people towards these type classes:

  • Functor/Applicative/Monad
  • Alternative/MonadPlus
  • MonadTrans/MonadIO

Right now there are only three functions in the API that are not class methods:

  • runListT
  • fold
  • foldM

Everything else is a method for one of the standard type classes and I avoid introducing new type classes.

Third, the API does not provide convenient helper functions for fully materializing the list. In other words, there is no utility function of this type:

toList :: ListT m a -> m [a]

A determined user can still force the list either indirectly via the fold function or by manually recursing over the ListT type. The goal is not to forbid this behavior, but rather to gently encourage people to preserve streaming. The API promotes the intuition that you're supposed to transform and consume results one-by-one instead of in large batches.

Fourth, the library comes with a long inline tutorial which is longer than the actual code. I think the tutorial could still use some improvement so if you would like to contribute to improve the tutorial please do!


You can find the list-transformer library either on Hackage or on Github.

Hopefully this encourages more people to give ListT a try and provides a stepping stone for understanding more complex streaming abstractoins.

by Gabriel Gonzalez ( at July 03, 2016 04:48 PM

July 02, 2016

Philip Wadler

Where we find ourselves

Jonathan Freedland at the Guardian sums up the state of affairs.
It’s gripping, of course. Game of Thrones meets House of Cards, played out at the tempo of a binge-viewed box-set. ...
This week’s antics of Gove and Johnson are a useful reminder. For the way one has treated the other is the way both have treated the country. ...
[Johnson] didn’t believe a word of his own rhetoric, we know that now. His face last Friday morning, ashen with the terror of victory, proved it. That hot mess of a column he served up on Monday confirmed it again: he was trying to back out of the very decision he’d persuaded the country to make.  ...
When doctrine is kept distilled, pure and fervently uncontaminated by reality, it turns into zealotry
So we have the appalling sight of Gove on Friday, proclaiming himself a proud believer in the UK even though it was obvious to anyone who cared to look that a leave vote would propel Scotland towards saying yes in a second independence referendum. The more honest leavers admit – as Melanie Phillips did when the two of us appeared on Newsnight this week – that they believe the break-up of the union is a price worth paying for the prize of sovereignty. ...
They did it with lies, whether the false promise that we could both halt immigration and enjoy full access to the single market or that deceitful £350m figure, still defended by Gove, which tricked millions into believing a leave vote would bring a cash windfall to the NHS. They did it with no plan, as clueless about post-Brexit Britain as Bush and Blair were about post-invasion Iraq.
Senior civil servants say Brexit will consume their energies for years to come, as they seek to disentangle 40 years of agreements. It will be the central focus of our politics and our government, a massive collective effort demanding ingenuity and creativity. Just think of what could have been achieved if all those resources had been directed elsewhere. Into addressing, for instance, the desperate, decades-long needs – for jobs, for housing, for a future – of those towns that have been left behind by the last 30 years of change, those towns whose people voted leave the way a passenger on a doomed train pulls the emergency cord.
<aside class="element element-pullquote element--supporting" style="background-color: white; box-sizing: border-box; clear: left; color: #333333; float: left; font-family: "Guardian Text Egyptian Web", Georgia, serif; line-height: 24px; margin-bottom: 0.375rem; margin-left: -16.25rem; padding: 0.1875rem 1.25rem 0px; width: 16.25rem;"></aside>

by Philip Wadler ( at July 02, 2016 07:00 AM

Roseburn to Leith Walk Cycleway: A vs B

Edinburgh City Council has released its report on consultation on the Roseburn to Leith Walk cycleway, and Henry Whaley has written a comment for the Edinburgh Evening News.

A few shopkeepers in the area are concerned that the cycleway will have a negative impact on their shops, a well-known cycling fallacy. Whaley describes the current impasse:
The Council have responded to specific concerns from some shopkeepers and residents by reinstating the loading bay on the north side of Roseburn Terrace, increasing the right turn lane and eliminating the floating bus stop whilst maintaining the cyclepath to form a much improved ‘Option A’.
The Council are also assessing an alternative ‘Option B’, which would take the cyclepath away from Roseburn Terrace, on an indirect and complicated route involving three road crossings as well as restricting the space for motor vehicles at the already tight Roseburn Street Junction and not widening the Roseburn Terrace pavements. It’s another option, but one that is worse for most people.
And from the City Council:
Transport Convener Councillor Lesley Hinds said: "We had an overwhelming response to the consultation and the exercise has been extremely helpful to officers working on the proposed Roseburn to Leith Walk cycleway and street improvements.
"Thanks to the feedback received, we've been able to make deliverable adjustments to a number of aspects of the scheme. In terms of the Roseburn section, local concerns have prompted us to present an alternative route (Option B) via Roseburn Place and Roseburn Street for consideration by committee members. However, we remain in favour of Option A because it will enhance the street environment in Roseburn Terrace and is more direct for cyclists - involving one road crossing rather than the three that would be required for Option B.
"After further planned consultation with businesses, community councils and the Council's Active Travel Forum, the project team will consolidate feedback and finalise the preliminary design scheme for presentation to the Transport and Environment Committee on 30 August 2016."

by Philip Wadler ( at July 02, 2016 06:01 AM

July 01, 2016

Joachim Breitner

When to reroll a six

This is a story about counter-intuitive probabilities and how a small bit of doubt turned out to be very justified.

It begins with the game “To Court the King” (German: „Um Krone und Kragen“). It is a nice game with dice and cards, where you start with a few dice, and use your dice rolls to buy additional cards, which give you extra dice or special powers to modify the dice that you rolled. You can actually roll your dice many times, but every time, you have to set aside at least one die, which you can no longer change or reroll, until eventually all dice have been set aside.

A few years ago, I have played this game a lot, both online (on as well as in real life. It soon became apparent that it is almost always better to go for the cards that give you an extra die, instead of those that let you modify the dice. Intuitively, this is because every additional die allows you to re-roll your dice once more.

I concluded that if I have a certain number of dice (say, n), and I want to have a sum as high as possible at the end, then it may make sense to reroll as many dice as possible, setting aside only those showing a 6 (because that is the best you can get) or, if there is no dice showing a 6, then a single die with the best score. Besides for small number of dice (2 or 3), where even a 4 or 5 is worth keeping, this seemed to be a simple, obvious and correct strategy to maximize the expected outcome of this simplified game.

It is definitely simple and obvious. But some doubt that it was correct remained. Having one more die still in the game (i.e. not set aside) definitely improves your expected score, because you can reroll the dice more often. How large is this advantage? What if it ever exceeds 6 – then it would make sense to reroll a 6. The thought was strange, but I could not dismiss it.

So I did what one does these days if one has a question: I posed it on the mathematics site of StackExchange. That was January 2015, and nothing happened.

I tried to answer it myself a month later, or at least work towards at an answer, and did that by brute force. Using a library for probabilistic calculations for Haskell I could write some code that simply calculated the various expected values of n dice for up to n = 9 (beyond that, my unoptimized code would take too long):

1:  3.50000 (+3.50000)
2:  8.23611 (+4.73611)
3: 13.42490 (+5.18879)
4: 18.84364 (+5.41874)
5: 24.43605 (+5.59241)
6: 30.15198 (+5.71592)
7: 35.95216 (+5.80018)
8: 41.80969 (+5.85753)
9: 47.70676 (+5.89707)

Note that this calculation, although printed as floating point numbers, is performed using fractions of unbounded integers, so there are no rounding issues that could skew the result.

The result supported the hypothesis that there is no point in rolling a 6 again: The value of an additional die grows and approaches 6 from beyond, but – judging from these number – is never going to reach it.

Then again nothing happened. Until 14 month later, when some Byron Schmuland came along, found this an interesting puzzle, and set out a 500 point bounty to whoever solved this problem. This attracted a bit attention, and a few not very successful attempts at solving this. Eventually it reached twitter, where Roman Cheplyaka linked to it.

Coincidally a day later some joriki came along, and he had a very good idea: Why not make our life easier and think about dice with less sides, and look at 3 instead of 6. This way, and using a more efficient implementation (but still properly using rationals), he could do a similar calculation for up to 50 dice. And it was very lucky that he went to 50, and not just 25, because up to 27, the results were very much as expected, approaching value of +3 from below. But then it surpassed +3 and became +3.000000008463403.

In other words: If you have roll 28 dice, and you have exactly two dice showing a 3, then it gives you better expected score if you set aside only one 3, and not both of them. The advantage is minuscule, but that does not matter – it is there.

From then on, the results behaved strangely. Between 28 and 34, the additional value was larger than 3. Then, from 35 on again lower than 2. It oscillated. Something similar could be observed when the game is played with coins.

Eventually, joriki improved his code and applied enough tricks so that he could solve it also for the 6-sided die: The difference of the expected value of 198 dice and having 199 dice is larger than 6 (by 10 − 21...)!

The optimizations that allowed him to calculate these numbers in a reasonable amount of time unfortunately was to assume that my original hypothesis (never rerolling a 6 is optimal), which held until n < 199. But this meant that for n > 199, the code did not yield correct results.

What is the rationale of the story? Don’t trust common sense when it comes to statistics; don’t judge a sequence just from a few initial numbers; if you have an interesting question, post it online and wait for 16 months.

by Joachim Breitner ( at July 01, 2016 07:47 PM

Douglas M. Auclair (geophf)

June 2016 1HaskellADay Problems and Solutions

  • June 29th, 2016: Today's #Haskell exercise is REALLY HARD! ... for Big Gov't. Can you solve it? A little bit of (well-typed) Prolog-like code gets us our #haskell solution for today 
  • June 28th, 2016: For today's #haskell problem we do ... NOTHING! But we are introduced to coding software for a huge bureaucracy  ... AAAAANNNDDD three System imports and we've got today's #haskell solution. Groovy! 
  • June 24th, 2016: #haskell problem today charts Stochastic Oscillators of a security  and includes a 'malus' problem: report generation 
  • June 23rd, 2016: Today we look at using #haskell to chart moving averages of a stock's prices 
  • June 21th, 2016: I pushed today's #haskell problem last night on git but did I announce it? sigh Complex roots of quadratic equations The #haskell solution gives us the Complex roots to any (Real) quadratic equation
  • June 20th, 2016: Solving quadratic equations is on the plate for today's #haskell exercise 
    It's not every day I code
    Thank you, #haskell, for today's solution to do so
  • June 17th, 2016: My, my! Where has the day flown? Today's #haskell problem is to reinvent charting API! ... or not.
  • June 16th, 2016: Today's #haskell exercise looks at representing $TWTR data as candlesticks 
  • June 15th, 2016: For today's #haskell problem, we round out the Data.Matrix module with the definition of the identity matrix There are many ways to define the identity matrix. Today's #haskell solution does so with Cellular Automata Rule 16
  • June 14th, 2016: Yesterday we computed the matrix determinant, today we'll invert a matrix and use it to solve systems of equations Today's #haskell solution inverts a matrix BECAUSE WE FEEL LIKE IT! Yeah
  • June 13th, 2016: For today's #haskell problem we *ahem* DETERMINE (eventually) to solve systems of equations The determinant is the sum of the products of the first row with the sub-matrix determinants, right? RIGHT!
  • June 10th, 2016: Today's #haskell problem looks at box-and-whiskers charting of data Boxes for realz, yo: The #haskell solution has @geophf writing 'uncurry uncurry' and sincerely meaning it! 😱 and box: 
  • June 9th, 2016: Triangles are on my mind for today's #haskell problem: … bisecting them, then trisecting them.
  • June 8th, 2016: For today's #haskell problem, just what you've always wanted: MATH HOMEWORK! We find the intersection of two lines
  • ANNOUNCEMENT: is acting up; cloning original @1HaskellADay github repository and putting the exercise there. FYI
  • June 6th, 2016: Today's #haskell problem explores superstring theory No, it doesn't, but saying that has a certain ring to it!
  • June 3rd, 2016: We saw a solution to perfect matching yesterday. For today's #haskell problem, let's efficient-ize it!
  • June 1st, 2016: Today's #haskell problem is pretty much counting complements ... pretty much. These apparently simple problems are actually rather hard. Today we have a #P-complete #haskell solution

by geophf ( at July 01, 2016 04:56 PM

Mark Jason Dominus

Don't tug on that, you never know what it might be attached to

This is a story about a very interesting bug that I tracked down yesterday. It was causing a bad effect very far from where the bug actually was.


The emacs text editor comes with a separate utility, called emacsclient, which can communicate with the main editor process and tell it to open files for editing. You have your main emacs running. Then somewhere else you run the command

     emacsclient some-files...

and it sends the main emacs a message that you want to edit some-files. Emacs gets the message and pops up new windows for editing those files. When you're done editing some-files you tell Emacs, by typing C-# or something, it it communicates back to emacsclient that the editing is done, and emacsclient exits.

This was more important in the olden days when Emacs was big and bloated and took a long time to start up. (They used to joke that “Emacs” was an abbreviation for “Eight Megs And Constantly Swapping”. Eight megs!) But even today it's still useful, say from shell scripts that need to run an editor.

Here's the reason I was running it. I have a very nice shell script, called also, that does something like this:

  • Interpret command-line arguments as patterns
  • Find files matching those patterns
  • Present a menu of the files
  • Wait for me to select files of interest
  • Run emacsclient on the selected files

It is essentially a wrapper around menupick, a menu-picking utility I wrote which has seen use as a component of several other tools. I can type

    also Wizard

in the shell and get a menu of the files related to the wizard, select the ones I actually want to edit, and they show up in Emacs. This is more convenient than using Emacs itself to find and open them. I use it many times a day.

Or rather, I did until this week, when it suddenly stopped working. Everything ran fine until the execution of emacsclient, which would fail, saying:

 emacsclient: can't find socket; have you started the server?

(A socket is a facility that enables interprocess communication, in this case between emacs and emacsclient.)

This message is familiar. It usually means that I have forgotten to tell Emacs to start listening for emacsclient, by running M-x server-start. (I should have Emacs do this when it starts up, but I don't. Why not? I'm not sure.) So the first time it happened I went to Emacs and ran M-x server-start. Emacs announced that it had started the server, so I reran also. And the same thing happened.

 emacsclient: can't find socket; have you started the server?

Finding the socket

So the first question is: why can't emacsclient find the socket? And this resolves naturally into two subquestions: where is the socket, and where is emacsclient looking?

The second one is easily answered; I ran strace emacsclient (hi Julia!) and saw that the last interesting thing emacsclient did before emitting the error message was

    stat("/mnt/tmp/emacs2017/server", 0x7ffd90ec4d40) = -1 ENOENT (No such file or directory)

which means it's looking for the socket at /mnt/tmp/emacs2017/server but didn't find it there.

The question of where Emacs actually put the socket file was a little trickier. I did not run Emacs under strace because I felt sure that the output would be voluminous and it would be tedious to grovel over it.

I don't exactly remember now how I figured this out, but I think now that I probably made an educated guess, something like: emacsclient is looking in /mnt/tmp; this seems unusual. I would expect the socket to be under /tmp. Maybe it is under /tmp? So I looked under /tmp and there it was, in /tmp/emacs2017/server:

    srwx------ 1 mjd mjd 0 Jun 27 11:43 /tmp/emacs2017/server

(The s at the beginning there means that the file is a “Unix-domain socket”. A socket is an endpoint for interprocess communication. The most familiar sort is a TCP socket, which has a TCP address, and which enables communication over the internet. But since ancient times Unix has also supported Unix-domain sockets, which enable communication between two processes on the same machine. Instead of TCP addresses, such sockets are addressed using paths in the filesystem, in this case /tmp/emacs2017/server. When the server creates such a socket, it appears in the filesystem as a special type of file, as here.)

I confirmed that this was the correct file by typing M-x server-force-delete in Emacs; this immediately caused /tmp/emacs2017/server to disappear. Similarly M-x server-start made it reappear.

Why the disagreement?

Now the question is: Why is emacsclient looking for the socket under /mnt/tmp when Emacs is putting it in /tmp? They used to rendezvous properly; what has gone wrong? I recalled that there was some environment variable for controlling where temporary files are put, so I did

       env | grep mnt

to see if anything relevant turned up. And sure enough there was:


When programs want to create tmporary files and directories, they normally do it in /tmp. But if there is a TMPDIR setting, they use that directory instead. This explained why emacsclient was looking for /mnt/tmp/emacs2017/socket. And the explanation for why Emacs itself was creating the socket in /tmp seemed clear: Emacs was failing to honor the TMPDIR setting.

With this clear explanation in hand, I began to report the bug in Emacs, using M-x report-emacs-bug. (The folks in the #emacs IRC channel on Freenode suggested this. I had a bad experience last time I tried #emacs, and then people mocked me for even trying to get useful information out of IRC. But this time it went pretty well.)

Emacs popped up a buffer with full version information and invited me to write down the steps to reproduce the problem. So I wrote down

     % export TMPDIR=/mnt/tmp
     % emacs

and as I did that I ran those commands in the shell.

Then I wrote

     In Emacs:
     M-x getenv TMPDIR
     (emacs claims there is no such variable)

and I did that in Emacs also. But instead of claiming there was no such variable, Emacs cheerfully informed me that the value of TMPDIR was /mnt/tmp.

(There is an important lesson here! To submit a bug report, you find a minimal demonstration. But then you also try the minimal demonstration exactly as you reported it. Because of what just happened! Had I sent off that bug report, I would have wasted everyone else's time, and even worse, I would have looked like a fool.)

My minimal demonstration did not demonstrate. Something else was going on.

Why no TMPDIR?

This was a head-scratcher. All I could think of was that emacsclient and Emacs were somehow getting different environments, one with the TMPDIR setting and one without. Maybe I had run them from different shells, and only one of the shells had the setting?

I got on a sidetrack at this point to find out why TMPDIR was set in the first place; I didn't think I had set it. I looked for it in /etc/profile, which is the default Bash startup instructions, but it wasn't there. But I also noticed an /etc/profile.d which seemed relevant. (I saw later that the /etc/profile contained instructions to load everything under /etc/profile.d.) And when I grepped for TMPDIR in the profile.d files, I found that it was being set by /etc/profile.d/, which the sysadmins had installed. So that mystery at least was cleared up.

That got me on a second sidetrack, looking through our Git history for recent changes involving TMPDIR. There weren't any, so that was a dead end.

I was still puzzled about why Emacs sometimes got the TMPDIR setting and sometimes not. That's when I realized that my original Emacs process, the one that had failed to rendezvous with emacsclient, had not been started in the usual way. Instead of simply running emacs, I had run

    git re-edit

which invokes Git, which then runs


which is a Perl program I wrote that does a bunch of stuff to figure out which files I was editing recently and then execs emacs to edit them some more. So there are several programs here that could be tampering with the environment and removing the TMPDIR setting.

To more accurately point the finger of blame, I put some diagnostics into the git-re-edit program to have it print out the value of TMPDIR. Indeed, git-re-edit reported that TMPDIR was unset. Clearly, the culprit was Git, which must have been removing TMPDIR from the environment before invoking my Perl program.

Who is stripping the environment?

To confirm this conclusion, I created a tiny shell script, /home/mjd/bin/git-env, which simply printed out the environment, and then I ran git env, which tells Git to find git-env and run it. If the environment it printed were to omit TMPDIR, I would know Git was the culprit. But TMPDIR was in the output.

So I created a Perl version of git-env, called git-perlenv, which did the same thing, and I ran it via git perlenv. And this time TMPDIR was not in the output. I ran diff on the outputs of git env and git perlenv and they were identical—except that git perlenv was missing TMPDIR.

So it was Perl's fault! And I verified this by running perl /home/mjd/bin/git-re-edit directly, without involving Git at all. The diagnostics I had put in reported that TMPDIR was unset.

WTF Perl?

At this point I tried getting rid of get-re-edit itself, and ran the one-line program

    perl -le 'print $ENV{TMPDIR}'

which simply runs Perl and tells it to print out the value of the TMPDIR environment variable. It should print /mnt/tmp, but instead it printed the empty string. This is a smoking gun, and Perl no longer has anywhere to hide.

The mystery is not cleared up, however. Why was Perl doing this? Surely not a bug; someone else would have noticed such an obvious bug sometime in the past 25 years. And it only failed for TMPDIR, not for other variables. For example

    FOO=bar perl -le 'print $ENV{FOO}'

printed out bar as one would expect. This was weird: how could Perl's environment handling be broken for just the TMPDIR variable?

At this point I got Rik Signes and Frew Schmidt to look at it with me. They confirmed that the problem was not in Perl generally, but just in this Perl. Perl on other systems did not display this behavior.

I looked in the output of perl -V, which says what version of Perl you are using and which patches have been applied, and wasted a lot of time looking into CVE-2016-2381, which seemed relevant. But it turned out to be a red herring.

Working around the problem, 1.

While all this was going on I was looking for a workaround. Finding one is at least as important as actually tracking down the problem because ultimately I am paid to do something other than figure out why Perl is losing TMPDIR. Having a workaround in hand means that when I get sick and tired of looking into the underlying problem I can abandon it instantly instead of having to push onward.

The first workaround I found was to not use the Unix-domain socket. Emacs has an option to use a TCP socket instead, which is useful on systems that do not support Unix-domain sockets, such as non-Unix systems. (I am told that some do still exist.)

You set the server-use-tcp variable to a true value, and when you start the server, Emacs creates a TCP socket and writes a description of it into a “server file”, usually ~/.emacs.d/server/server. Then when you run emacsclient you tell it to connect to the socket that is described in the file, with

    emacsclient --server-file=~/.emacs.d/server/server

or by setting the EMACS_SERVER_FILE environment variable. I tried this, and it worked, once I figured out the thing about server-use-tcp and what a “server file” was. (I had misunderstood at first, and thought that “server file” meant the Unix-domain socket itself, and I tried to get emacsclient to use the right one by setting EMACS_SERVER_FILE, which didn't work at all. The resulting error message was obscure enough to lead me to IRC to ask about it.)

Working around the problem, 2.

I spent quite a while looking for an environment variable analogous to EMACS_SERVER_FILE to tell emacsclient where the Unix-domain socket was. But while there is a --socket-name command-line argument to control this, there is inexplicably no environment variable. I hacked my also command (responsible for running emacsclient) to look for an environment variable named EMACS_SERVER_SOCKET, and to pass its value to emacsclient --socket-name if there was one. (It probably would have been better to write a wrapper for emacsclient, but I didn't.) Then I put

    EMACS_SERVER_SOCKET=$TMPDIR/emacs$(id -u)/server

in my Bash profile, which effectively solved the problem. This set EMACS_SERVER_SOCKET to /mnt/tmp/emacs2017/server whenever I started a new shell. When I ran also it would notice the setting and pass it along to emacsclient with --socket-name, to tell emacsclient to look in the right place. Having set this up I could forget all about the original problem if I wanted to.

But but but WHY?

But why was Perl removing TMPDIR from the environment? I didn't figure out the answer to this; Frew took it to the #p5p IRC channel on, where the answer was eventually tracked down by Matthew Horsfall and Zefrem.

The answer turned out to be quite subtle. One of the classic attacks that can be mounted against a process with elevated privileges is as follows. Suppose you know that the program is going to write to a temporary file. So you set TMPDIR beforehand and trick it into writing in the wrong place, possibly overwriting or destroying something important.

When a program is loaded into a process, the dynamic loader does the loading. To protect against this attack, the loader checks to see if the program it is going to run has elevated privileges, say because it is setuid, and if so it sanitizes the process’ environment to prevent the attack. Among other things, it removes TMPDIR from the environment.

I hadn't thought of exactly this, but I had thought of something like it: If Perl detects that it is running setuid, it enables a secure mode which, among other things, sanitizes the environment. For example, it ignores the PERL5LIB environment variable that normally tells it where to look for loadable modules, and instead loads modules only from a few compiled-in trustworthy directories. I had checked early on to see if this was causing the TMPDIR problem, but the perl executable was not setuid and Perl was not running in secure mode.

But Linux supports a feature called “capabilities”, which is a sort of partial superuser privilege. You can give a program some of the superuser's capabilities without giving away the keys to the whole kingdom. Our systems were configured to give perl one extra capability, of binding to low-numbered TCP ports, which is normally permitted only to the superuser. And when the dynamic loader ran perl, it saw this additional capability and removed TMPDIR from the environment for safety.

This is why Emacs had the TMPDIR setting when run from the command line, but not when run via git-re-edit.

Until this came up, I had not even been aware that the “capabilities” feature existed.

A red herring

There was one more delightful confusion on the way to this happy ending. When Frew found out that it was just the Perl on my development machine that was misbehaving, he tried logging into his own, nearly identical development machine to see if it misbehaved in the same way. It did, but when he ran a system update to update Perl, the problem went away. He told me this would fix the problem on my machine. But I reported that I had updated my system a few hours before, so there was nothing to update!

The elevated capabilities theory explained this also. When Frew updated his system, the new Perl was installed without the elevated capability feature, so the dynamic loader did not remove TMPDIR from the environment.

When I had updated my system earlier, the same thing happened. But as soon as the update was complete, I reloaded my system configuration, which reinstated the capability setting. Frew hadn't done this.


  • The system configuration gave perl a special capability
  • so the dynamic loader sanitized its environment
  • so that when perl ran emacs,
  • the Emacs process didn't have the TMPDIR environment setting
  • which caused Emacs to create its listening socket in the usual place
  • but because emacsclient did get the setting, it looked in the wrong place


This computer stuff is amazingly complicated. I don't know how anyone gets anything done.

[ Addendum 20160709: Frew Schmidt has written up the same incident, but covers different ground than I do. ]

[ Addendum 20160709: A Hacker News comment asks what changed to cause the problem? Why was Perl losing TMPDIR this week but not the week before? Frew and I don't know! ]

by Mark Dominus ( at July 01, 2016 03:00 PM

Edwin Brady

Elaborator Reflection: Extending Idris in Idris

A new paper by David Christiansen and myself, to appear in ICFP 2016. Abstract:

Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection, a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.

You can get the PDF here.

by edwinb at July 01, 2016 09:48 AM

Christoph Breitkopf

Averaging unsigned numbers in Haskell

In performance sensitive code I needed the average of two unsigned shorts:
  uavg :: Word16 -> Word16 -> Word16
  uavg a b = ...
The naive implementation (a + b) `shiftR` 1 does not work if the addition overflows.

In a language with a less disciplined type systen, such as C, I'd probably have used a higher-precision type to hold the intermediate sum:

  unsigned short uavg(unsigned short a, unsigned short b)
        return (unsigned short) (((unsigned) a + b) >> 1);
But because numeric type conversion in Haskell is rather intrusive, I used the following code:
  uavg a b = (a `shiftR` 1) + (b `shiftR` 1) + (a .&. b .&. 1)
That is correct and has no problems with overflow.

What I overlooked at this point is performance. At first glance, the code looks fast: it does no type conversion and uses only very fast operations. But that first look is deceiving. If you count operations, this version has 6 ops, and the type-cast version only 2. Even if you count the type conversions as operations, you still end up with only 5 ops.

So I ended up with this Haskell version of the C code above:

  uavg a b = let a',b' :: Word
                 a' = fromIntegral a
                 b' = fromIntegral b
             in fromIntegral ((a' + b') `shiftR` 1)
To me, this looks slower, probably because the fromIntegral's take as much space as the rest of the code combined. But it turns out to be at least twice as fast as the bit-twiddling version (on x64 at least).

Now, how to get the same performance with a more generic type signature?

by Christoph Breitkopf ( at July 01, 2016 05:45 AM

June 30, 2016

Chris Smith

CodeWorld for Younger Ages!

Most readers know about CodeWorld, my Haskell-based programming environment that I’ve been using for middle school education for a number of years.  I recently wrote a thorough post about the project and its characteristic choices.  I’ve had a lot of success teaching middle school students, of ages 12 and up.  But why not younger?

There are challenges in teaching younger ages.  Spelling and typing skill is a real limitation.  If it takes kids several minutes to correctly type “solidCircle”, they aren’t going to be having a good time.  Even at the middle school level, students spend a good part of their first few months struggling to match up parentheses.  (So much so that I’ve just implemented “rainbow brackets”, which colors each nested set of parentheses a different color, in the editor in hopes of helping at least a little!)  These have always given me something of a lower bound for the ages at which I can hope to reach students.

This summer, though, as part of the Summer of Haskell project, Stefan Jacholke has been implementing a different programming environment for CodeWorld that solves many of these problems.  He’s just announced his first prototype!

If you need some inspiration, here’s an example of a program to draw a few bears.

This is all great timing, because next week, I’m meeting with my first elementary school to talk about setting up a CodeWorld activity for younger students.  With luck, I’ll have my guinea pigs to try this in the fall.


by cdsmith at June 30, 2016 02:46 PM

June 29, 2016

Stefan Jacholke

Fun Blocks Prototype

After looking up the constituent technologies which will be used for the project, work on the initial prototype began. For the initial version, we want a simple user interface with which simple CodeWorld applications can be built. Thus we want a version where a user can:

  • Drag and drop blocks from the toolbox
  • Provide simple error feedback
  • Generate code for a valid CodeWorld application
  • Run the generated CodeWorld applications
  • Saving and loading

Some more advanced features which are omitted for this release are:

  • Support for functions
  • Support for lists
  • Advanced CodeWorld applications (animations, events)

Simply put, we want a visual block-based interface which can be used to build CodeWorld applications.

This project is educationally based. We want to introduce programming to younger students and make it easy for them to understand the concepts behind it. For more advanced projects students may use the regular CodeWorld text UI.

The initial prototype can be found at


This project relies heavily on Blockly for the user interface. Blockly provides an editor where blocks can be dragged and dropped on a canvas. These blocks can then be interlocked with one another through a snapping behavior.

Blockly provides many features that make it easy to adapt to a new language. It even incorporates simple type checking, luckily, however, there is a project that improves Blockly’s type checking.

For the user-interface, the choice was made to keep the interface clean and simple. The idea is to have a simple toolbar on the left-side with blocks that can be dragged onto the canvas on the right.

Since the project uses Blockly, blocks can be snapped into each other. A block has a single output and may have multiple inputs, each having a type.

Translate Block

In the image above we can see a Translated block, taking a picture and two numbers, and outputs another picture that is translated according to the given x and y values.

Each block may have zero or more inputs and one output type. All blocks are typed, and the functions in CodeWorld work on immutable data structures. A function may take a color as an input to produce another modified color. This works well with a visual block interface and we can expressively see how the program flows.

Blockly provides a lot of features out of the box, though sometimes changes are necessary specifically for this project.

The largest has been to use Anthony’s, which provides some useful typing and polymorphic features though it also diverges from the main Blockly branch and is almost 300 commits behind.

Other changes have been required as well, such as:

  • implementing the let blocks
  • changing default methods of validation for numbers and function names
  • adding error highlighting

and other small changes and additions. Thus we maintain a separate fork of Blockly for this project.


When we build the program below:

Drawing of

we obtain the output code of:

main = drawingOf(rotated(colored(solidRectangle(7,5), white),(60 + 70) * 0.9) & solidCircle(4))

Which looks rather ugly, but code formatting will be addressed at a later stage.

Currently, the regular Blockly code generation paradigm is followed, where a code generation function is given for each block, that converts the block into code. For a single block, we convert all input blocks to code, which are then combined into a single block of code. This process is repeated for all top-level blocks.

For each block, a generation function is assigned, which looks something like this:

blockSector :: GeneratorFunction
blockSector block = do
    startangle <- valueToCode block "STARTANGLE" CNone
    endangle <- valueToCode block "ENDANGLE" CNone
    radius <- valueToCode block "RADIUS" CNone
    return $ none $ "sector(" ++ startangle ++ "," ++ endangle ++ "," ++ radius ++ ")"

This approach has some disadvantages, such being:

  • Difficult to ensure code is consistent and that all types match.
  • Difficult to find errors when they occur
  • Having to define a block for every CodeWorld function

The first problem is alleviated with a different version of Blockly that supports polymorphic types. I’m using an updated version by Anthony that also support automatic coloring of Blocks. Hence the strategy currently taken is to prevent errors through the block based editor.

This version of Blockly fits this project great. Since we don’t have side-effects the type of the if-block should be of the same as the then or else expressions. In order to have a single if block, it must be polymorphic, and this is provided by the alternate Blockly.

If Text Above we can see the if block matching the Text type; below we can see the if block matching the Picture type. If Picture

Regardless, the generated code is then displayed and syntax highlighted using CodeMirror.

The generated code is sent to the CodeWorld server, which compiles the code into JavaScript. The compiled code is then run in the browser and displayed on an HTML canvas.


Error handling

First priority is to prevent a large class of errors from ever occurring. This is done by only allowing certain connections between blocks, validating input, providing default blocks and so on. This makes it easy for the user to construct valid programs.

However, errors do happen. What happens when a block contains a disconnected input ?

In this version, we visually indicate at which block the error occurs and display an error message for the block. This can be seen in the picture below.


Some other errors, such as runtime errors will be addressed at a later stage. Luckily, we currently don’t have missing patterns or partial functions to check for.

Project Management

Project management falls in line with the way things are currently done with the regular CodeWorld site.

Blockly supports exporting the current workspace as XML. This XML is then sent to the server and a hash is returned. This hash identifies a CodeWorld FunBlocks application. For example loads a drawing of a coordinate plane.

Google’s authentication API can be used to log in. Once a user is logged in he can then save and load his projects by name as well.

Issues / Problems

A large majority of the project is in JavaScript, this includes the Blockly library.

Originally I intended to keep the majority of the code in Haskell, however, this is difficult to do. Currently, there is a large part of additional code for Blockly and an additional JavaScript file that handles the user interface initialization and logic.

Most of the code that define the various types of Blocks are in a Haskell file. However, some more standard blocks such as the math number block (which included some validation) are modified from the regular Blockly code base. The let definition is also modified Blockly code.

Thus organisationally, similar features and code are split between the main project and the Blockly fork.

Another issue currently is the renaming of caller blocks for Let definitions. When a Let definition is renamed the callerb blocks should get renamed as well. This currently disabled as Blockly is sometimes calling the text input validator for the wrong block, which tries to rename all of foo’s blocks to bar.

The block type unification for the Let definition is also currently producing strange results and the issues on this are covered in the issue tracker.

Further Work

Currently, we are only able to build very simple programs. For more complicated applications such as animations, we require first class functions. We also need to cover more advanced data types. A starting point would be to cover lists and tuples.

For CodeWorld simulations, the user is required to supply his own world data type, and a user-friendly way is needed for the user to build these in the Blocks UI.

Some more advanced functional features such as pattern matching would make this easier, and it remains to be seen how this will be implemented.

Everything is currently on track, which might mean we will get to spend time on same of the more advanced features later.


Working on the project I’m exposed to GHCJS and JavaScript a lot and I really like what GHCJS is doing. JavaScript has a tendency to let anything almost work and I spend a lot of time debugging and finding JS errors when working on Blockly code.

Straight after starting out I decided to try and keep the bulk of the work in Haskell, which meant using GHCJS. The GHCJS ecosystem lacks good documentation and sometimes in order to accomplish things that are simple in JS, a lot of time has to be spent navigating through many files of GHCJS code and a bit of luck. One such is an example is when you want to assign a higher order function in JS:

Blockly.FunBlocks["block_number"] = function(block){...}

where we want to assign a function to do the code generation for the block indexed as “block_number”

Which involved looking at GHCJS callback source files , even though there are Stackoverflow questions regarding similar issues, the GHCJS project is fast moving and the libraries keep changing.

Haskell Summer of Code

I would like to say thanks for being part of this year’s Haskell Summer of Code as I’m enjoying working the project quite a bit. Thanks goes to all of those who made it possible as well.

I think the way the project is managed is quite good. We (me and my mentor, Chris Smith) are primarily communicating through emails and Github. Working on Github helps a lot and the issue system greatly helps manage the project. It helps when you want to have some idea or goal to work on or if you want to fix something quickly. It’s too easy to forget about a minor bug if it isn’t written down somewhere.

Chris has also been a great help testing new features, providing feedback, opening issues and reporting bugs (which sometimes are a lot, I apologize !) and providing overall direction for the project.

June 29, 2016 10:00 PM

FP Complete

Announce: safe-exceptions, for async exception safety

This blog post is an initial announcement of a new package, safe-exceptions (and Github repo). This is a follow up to a number of comments I made in last week's blog post. To quote the README:

Safe, consistent, and easy exception handling

Runtime exceptions - as exposed in base by the Control.Exception module - have long been an intimidating part of the Haskell ecosystem. This package, and this README for the package, are intended to overcome this. By providing an API that encourages best practices, and explaining the corner cases clearly, the hope is to turn what was previously something scary into an aspect of Haskell everyone feels safe using.

This is an initial release of the package. I fully expect the library to expand in the near future, and in particular there are two open issues for decisions that need to be made in the short term. I'm releasing the package in its current state since:

  1. I think it's useful as-is
  2. I'm hoping to get feedback on how to improve it

On the second point, I've created a survey to get feedback on the interruptible/uninterruptible issue and the throw naming issue. Both are described in this blog post.

I'm hoping this library can bring some sanity and comfort to people dealing with IO and wanting to ensure proper exception handling! Following is the content of the README, which can also be read on Github.


This package provides additional safety and simplicity versus Control.Exception by having its functions recognize the difference between synchronous and asynchronous exceptions. As described below, synchronous exceptions are treated as recoverable, allowing you to catch and handle them as well as clean up after them, whereas asynchronous exceptions can only be cleaned up after. In particular, this library prevents you from making the following mistakes:

  • Catching and swallowing an asynchronous exception
  • Throwing an asynchronous exception synchronously
  • Throwing a synchronous exception asynchronously
  • Swallowing asynchronous exceptions via failing cleanup handlers


This section is intended to give you the bare minimum information to use this library (and Haskell runtime exceptions in general) correctly.

  • Import the Control.Exception.Safe module. Do not import Control.Exception itself, which lacks the safety guarantees that this library adds. Same applies to Control.Monad.Catch.
  • If something can go wrong in your function, you can report this with the throw. (For compatible naming, there are synonyms for this of throwIO and throwM.)
  • If you want to catch a specific type of exception, use catch, handle, or try.
  • If you want to recover from anything that may go wrong in a function, use catchAny, handleAny, or tryAny.
  • If you want to launch separate threads and kill them externally, you should use the async package.
  • Unless you really know what you're doing, avoid the following functions:
    • catchAsync
    • handleAsync
    • tryAsync
    • impureThrow
    • throwTo
  • If you need to perform some allocation or cleanup of resources, use one of the following functions (and don't use the catch/handle/try family of functions):

    • onException
    • withException
    • bracket
    • bracket_
    • finally
    • bracketOnError
    • bracketOnError_

Hopefully this will be able to get you up-and-running quickly.

Request to readers: if there are specific workflows that you're unsure of how to accomplish with this library, please ask so we can develop a more full-fledged cookbook as a companion to this file.


We're going to define three different versions of exceptions. Note that these definitions are based on how the exception is thrown, not based on what the exception itself is:

  • Synchronous exceptions are generated by the current thread. What's important about these is that we generally want to be able to recover from them. For example, if you try to read from a file, and the file doesn't exist, you may wish to use some default value instead of having your program exit, or perhaps prompt the user for a different file location.

  • Asynchronous exceptions are thrown by either a different user thread, or by the runtime system itself. For example, in the async package, race will kill the longer-running thread with an asynchronous exception. Similarly, the timeout function will kill an action which has run for too long. And the runtime system will kill threads which appear to be deadlocked on MVars or STM actions.

    In contrast to synchronous exceptions, we almost never want to recover from asynchronous exceptions. In fact, this is a common mistake in Haskell code, and from what I've seen has been the largest source of confusion and concern amongst users when it comes to Haskell's runtime exception system.

  • Impure exceptions are hidden inside a pure value, and exposed by forcing evaluation of that value. Examples are error, undefined, and impureThrow. Additionally, incomplete pattern matches can generate impure exceptions. Ultimately, when these pure values are forced and the exception is exposed, it is thrown as a synchronous exception.

    Since they are ultimately thrown as synchronous exceptions, when it comes to handling them, we want to treat them in all ways like synchronous exceptions. Based on the comments above, that means we want to be able to recover from impure exceptions.

Why catch asynchronous exceptions?

If we never want to be able to recover from asynchronous exceptions, why do we want to be able to catch them at all? The answer is for resource cleanup. For both sync and async exceptions, we would like to be able to acquire resources - like file descriptors - and register a cleanup function which is guaranteed to be run. This is exemplified by functions like bracket and withFile.

So to summarize:

  • All synchronous exceptions should be recoverable
  • All asynchronous exceptions should not be recoverable
  • In both cases, cleanup code needs to work reliably

Determining sync vs async

Unfortunately, GHC's runtime system provides no way to determine if an exception was thrown synchronously or asynchronously, but this information is vitally important. There are two general approaches to dealing with this:

  • Run an action in a separate thread, don't give that thread's ID to anyone else, and assume that any exception that kills it is a synchronous exception. This approach is covered in the School of Haskell article catching all exceptions, and is provided by the enclosed-exceptions package.

  • Make assumptions based on the type of an exception, assuming that certain exception types are only thrown synchronously and certain only asynchronously.

Both of these approaches have downsides. For the downsides of the type-based approach, see the caveats section at the end. The problems with the first are more interesting to us here:

  • It's much more expensive to fork a thread every time we want to deal with exceptions
  • It's not fully reliable: it's possible for the thread ID of the forked thread to leak somewhere, or the runtime system to send it an async exception
  • While this works for actions living in IO, it gets trickier for pure functions and monad transformer stacks. The latter issue is solved via monad-control and the exceptions packages. The former issue, however, means that it's impossible to provide a universal interface for failure for pure and impure actions. This may seem esoteric, and if so, don't worry about it too much.

Therefore, this package takes the approach of trusting type information to determine if an exception is asynchronous or synchronous. The details are less interesting to a user, but the basics are: we leverage the extensible extension system in GHC and state that any extension type which is a child of SomeAsyncException is an async exception. All other exception types are assumed to be synchronous.

Handling of sync vs async exceptions

Once we're able to distinguish between sync and async exceptions, and we know our goals with sync vs async, how we handle things is pretty straightforward:

  • If the user is trying to install a cleanup function (such as with bracket or finally), we don't care if the exception is sync or async: call the cleanup function and then rethrow the exception.
  • If the user is trying to catch an exception and recover from it, only catch sync exceptions and immediately rethrow async exceptions.

With this explanation, it's useful to consider async exceptions as "stronger" or more severe than sync exceptions, as the next section will demonstrate.

Exceptions in cleanup code

One annoying corner case is: what happens if, when running a cleanup function after an exception was thrown, the cleanup function itself throws an exception. For this, we'll consider action `onException` cleanup. There are four different possibilities:

  • action threw sync, cleanup threw sync
  • action threw sync, cleanup threw async
  • action threw async, cleanup threw sync
  • action threw async, cleanup threw async

Our guiding principle is: we cannot hide a more severe exception with a less severe exception. For example, if action threw a sync exception, and then cleanup threw an async exception, it would be a mistake to rethrow the sync exception thrown by action, since it would allow the user to recover when that is not desired.

Therefore, this library will always throw an async exception if either the action or cleanup thows an async exception. Other than that, the behavior is currently undefined as to which of the two exceptions will be thrown. The library reserves the right to throw away either of the two thrown exceptions, or generate a new exception value completely.


The exceptions package provides an abstraction for throwing, catching, and cleaning up from exceptions for many different monads. This library leverages those type classes to generalize our functions.


There are a few choices of naming that differ from the base libraries:

  • throw in this library is for synchronously throwing within a monad, as opposed to in base where throwIO serves this purpose and throw is for impure throwing. This library provides impureThrow for the latter case, and also provides convenience synonyms throwIO and throwM for throw.
  • The catch function in this package will not catch async exceptions. Please use catchAsync if you really want to catch those, though it's usually better to use a function like bracket or withException which ensure that the thrown exception is rethrown.


Let's talk about the caveats to keep in mind when using this library.

Checked vs unchecked

There is a big debate and difference of opinion regarding checked versus unchecked exceptions. With checked exceptions, a function states explicitly exactly what kinds of exceptions it can throw. With unchecked exceptions, it simply says "I can throw some kind of exception." Java is probably the most famous example of a checked exception system, with many other languages (including C#, Python, and Ruby) having unchecked exceptions.

As usual, Haskell makes this interesting. Runtime exceptions are most assuredly unchecked: all exceptions are converted to SomeException via the Exception typeclass, and function signatures do not state which specific exception types can be thrown (for more on this, see next caveat). Instead, this information is relegated to documentation, and unfortunately is often not even covered there.

By contrast, approaches like ExceptT and EitherT are very explicit in the type of exceptions that can be thrown. The cost of this is that there is extra overhead necessary to work with functions that can return different types of exceptions, usually by wrapping all possible exceptions in a sum type.

This library isn't meant to settle the debate on checked vs unchecked, but rather to bring sanity to Haskell's runtime exception system. As such, this library is decidedly in the unchecked exception camp, purely by virtue of the fact that the underlying mechanism is as well.

Explicit vs implicit

Another advantage of the ExceptT/EitherT approach is that you are explicit in your function signature that a function may fail. However, the reality of Haskell's standard libraries are that many, if not the vast majority, of IO actions can throw some kind of exception. In fact, once async exceptions are considered, every IO action can throw an exception.

Once again, this library deals with the status quo of runtime exceptions being ubiquitous, and gives the rule: you should consider the IO type as meaning both that a function modifies the outside world, and may throw an exception (and, based on the previous caveat, may throw any type of exception it feels like).

There are attempts at alternative approaches here, such as unexceptionalio. Again, this library isn't making a value statement on one approach versus another, but rather trying to make today's runtime exceptions in Haskell better.

Type-based differentiation

As explained above, this library makes heavy usage of type information to differentiate between sync and async exceptions. While the approach used is fairly well respected in the Haskell ecosystem today, it's certainly not universal, and definitely not enforced by the Control.Exception module. In particular, throwIO will allow you to synchronously throw an exception with an asynchronous type, and throwTo will allow you to asynchronously throw an exception with a synchronous type.

The functions in this library prevent that from happening via exception type wrappers, but if an underlying library does something surprising, the functions here may not work correctly. Further, even when using this library, you may be surprised by the fact that throw Foo `catch` (\Foo -> ...) won't actually trigger the exception handler if Foo looks like an asynchronous exception.

The ideal solution is to make a stronger distinction in the core libraries themselves between sync and async exceptions.

Deadlock detection exceptions

Two exceptions types which are handled surprisingly are BlockedIndefinitelyOnMVar and BlockedIndefinitelyOnSTM. Even though these exceptions are thrown asynchronously by the runtime system, for our purposes we treat them as synchronous. The reasons are twofold:

  • There is a specific action taken in the local thread - blocking on a variable which will never change - which causes the exception to be raised. This makes their behavior very similar to synchronous exceptions. In fact, one could argue that a function like takeMVar is synchronously throwing BlockedIndefinitelyOnMVar
  • By our standards of recoverable vs non-recoverable, these exceptions certainly fall into the recoverable category. Unlike an intentional kill signal from another thread or the user (via Ctrl-C), we would like to be able to detect that we entered a deadlock condition and do something intelligent in an application.

Possible future changes

Interruptible vs uninterruptible masking

This discussion is now being tracked at:

In Control.Exception, allocation functions and cleanup handlers in combinators like bracket are masked using the (interruptible) mask function, in contrast to uninterruptibleMask. There have been some debates about the correctness of this in the past, notably a libraries mailing list discussion kicked off by Eyal Lotem. It seems that general consensus is:

  • uninterruptibleMask is a better choice
  • But changing the core library like this would potentially break too many programs

In its current version, this library uses mask (interruptible) for allocation functions and uninterruptibleMask cleanup handlers. This is a debatable decision (and one worth debating!). An example of alternatives would be:

  • Use uninterruptibleMask for both allocation and cleanup pieces
  • Match Control.Exception's behavior
  • Provide two versions of each function, or possibly two modules

Naming of the synchronous monadic throwing function

We may decide to rename throw to something else at some point. Please see

June 29, 2016 12:00 AM

June 28, 2016

Roman Cheplyaka

Install Fedora Linux on an encrypted SSD

I just replaced the SSD in my laptop with a bigger one and installed a fresh Fedora Linux on it, essentially upgrading from F23 to F24.

Here are a few notes which could be useful to others and myself in the future.

Verifying the downloaded image

How do you verify the downloaded image? You verify the checksum.

How do you verify the checksum? You check its gpg signature.

How do you verify the authenticity of the gpg key? You could just check the fingerprint against the one published on the website above, but this is hardly better than trusting the checksum, since they both come from the same source.

Here’s a better idea: if you already have a Fedora system, you have the keys at /etc/pki/rpm-gpg.

In my case, I imported /etc/pki/rpm-gpg/RPM-GPG-KEY-fedora-24-primary (yes, my F23 system already contained the F24 signing keys), and was able to check the checksum signature.

This protects you against a scenario when is compromised and the checksums/signatures/keys are replaced there.

Installing from a USB partition

Turned out the only optical disc in my house was damaged, and I didn’t have a USB stick big enough to burn the Fedora image either.

I did have an external USB drive with some free space on it, but it contained a lot of data, so I couldn’t just make it one big ISO partition.

There are several instructions on how to create bootable USB partitions, but most of them look fragile and complicated.

Luckily, Fedora makes this super easy.

  1. Install the RPM package livecd-tools (which is a packaged version of this repo)
  2. Create a partition big enough for the ISO and format it. Unlike many other instructions that tell you to use FAT, this one works with ext[234] just fine.
  3. livecd-iso-to-disk Fedora-Workstation-Live-x86_64-24-1.2.iso /dev/sdb1

Setting up disk encryption

I was impressed by how easy it was to set up full disk encryption. I just checked the box “Encrypt my data” in the installer, and it used a very sensible partitioning scheme close to what I used to set up manually before:

  • Unencrypted /boot partition
  • Encrypted partition with LVM on top of it
    • Three logical volumes on the encrypted LVM: root, /home, and swap.

The only thing that I had to do was to enable TRIM support:

  1. For LVM: set issue_discards = 1 in /etc/lvm/lvm.conf.
  2. For cryptsetup: change none to discard in /etc/crypttab.
  3. Enable weekly trims systemctl enable fstrim.timer && systemctl start fstrim.timer

June 28, 2016 08:00 PM

Functional Jobs

Senior Software Engineer (Haskell) at Front Row Education (Full-time)


Senior Functional Web Engineer to join fast-growing education startup transforming the way 3+ million K-8 students learn Math and English.

What you will be doing

Architect, design and develop new 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 as part of a very small (there's literally half a dozen of us!), world-class team of engineers with a track record of rapidly delivering valuable software to millions of users.

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.

Why you should join Front Row

Our mission is important to us, and we want it to be important to you as well: millions of students learn math using Front Row every month. Our early results show students improve twice as much while using Front Row than their peers who aren’t using the program.

As an experienced engineer, you will have a massive impact on the company, product, and culture; you’ll have a ton of autonomy and responsibility; you’ll have equity to match the weight of this role. If you're looking for an opportunity to both grow and do meaningful work, surrounded and supported by like-minded professionals, this is THE place for you.

You will be working side by side with well known world-class personalities in the Haskell and Functional Programming community whose work you've likely used. Front Row is an active participant to the Open Source community and contributor to some of the most popular Haskell libraries.

A lot of flexibility: while we all work towards the same goals, you’ll have a lot of autonomy in what you work on. You can work from home up to one day a week, and we have a very flexible untracked vacation days policy

The company and its revenue are growing at a rocketship pace. Front Row is projected to make a massive impact on the world of education in the next few years. It's a once in a lifetime opportunity to join a small organization with great odds of becoming the Next Big Thing.

Must haves

  • You have experience doing full-stack web development. You understand HTTP, networking, databases and the world of distributed systems.
  • You have functional programming experience.
  • Extreme hustle: you’ll be solving a lot of problems you haven’t faced before without the resources and the support of a giant organization. You must thrive on getting things done, whatever the cost.
  • Soft skills: we want you to move into a leadership position, so you must be an expert communicator


  • You have led a software development team before
  • You have familiarity with a functional stack (Haskell / Clojure / Scala / OCaml etc)
  • You understand and have worked all around the stack before, from infrastructure automation all the way to the frontend
  • You're comfortable with the Behavior-Driven Development style
  • You have worked at a very small startup before: you thrive on having a lot of responsibility and little oversight
  • You have worked in small and effective Agile/XP teams before
  • You have delivered working software to large numbers of users before


  • Competitive salary
  • Generous equity option grants
  • Medical, Dental, and Vision
  • Catered lunch and dinner 4 times a week
  • Equipment budget
  • (onsite only) One flexible work day per week
  • (onsite only) Working from downtown SF, very accessible location
  • Professional yet casual work environment

Get information on how to apply for this position.

June 28, 2016 04:35 PM

June 27, 2016

Philip Wadler

Brexit implies Techxit?

In the wake of the EU referendum, there appears to be considerable information about its consequences that many might wish to have seen before the vote. Some of this concerns the negative impact of Brexit on technology firms. Among others, the BBC has a summary.
I was particularly struck by one comment in the story, made by start-up mentor Theo Priestley (pictured above),.
And Mr Priestley thinks that in the event of a Scottish independence referendum that leads to reunification with the EU, it's possible some start-ups could move north of the border, perhaps to rekindle "Silicon Glen" - a 1980s attempt to compete in the semiconductor industry.

by Philip Wadler ( at June 27, 2016 10:48 AM

Bryn Keller

Python Class Properties

Class properties are a feature that people coming to Python from other object-oriented languages expect, and expect to be easy. Unfortunately, it’s not. In many cases, you don’t actually want class properties in Python - after all, you can have first class module-level functions as well, you might very well be happier with one of those.

I sometimes see people claim that you can’t do class properties at all in Python, and that’s not right either. It can be done, and it’s not too bad. Read on!

I’m going to assume here that you already know what class (sometimes called “static”) properties are in languages like Java, and that you’re somewhat familiar with Python metaclasses.

To make this feature work, we have to use a metaclass. In this example, we’ll suppose that we want to be able to access a list of all the instances of our class, as well as reference to the most recently created instance. It’s artificial, but it gives us a reason to have both read-only and read-write properties. We define a metaclass, which is again a class that extends type.

class Extent(type):
    def extent(self):
        ext = getattr(self, '_extent', None)
        if ext is None:
            self._extent = []
            ext = self._extent
        return ext
    def last_instance(self):
        return getattr(self, '_last_instance', None)
    def last_instance(self, value):
        self._last_instance = value

Please note that if you want to do something like this for real, you may well need to protect access to these shared class properties with synchronization tools like RLock and friends to prevent different threads from overwriting each others’ work willy-nilly.

Next we create a class that uses that metaclass. The syntax is different in Python 2.7, so you may need to adjust if you’re working in an older version.

class Thing(object, metaclass=Extent):
    def __init__(self):
        self.__class__.last_instance = self

Another note for real code: these references (the extent and the last_instance) will keep your object from being garbage collected, so if you actually want to keep extents for your classes, you should do so using something like weakref.

Now we can try out our new class:

>>> t1 = Thing()
>>> t2 = Thing()
>>> Thing.extent
[<__main__.Thing object at 0x101c5d080>, <__main__.Thing object at 0x101c5d2b0>]
>>> Thing.last_instance
<__main__.Thing object at 0x101c5d2b0>

Great, we have what we wanted! There are a couple of things to remember, though:

  • Class properties are inherited!
  • Class properties are not accessible via instances, only via classes.

Let’s see an example that demonstrates both. Suppose we add a new subclass of Thing called SuperThing:

>>> class SuperThing(Thing):
...     @property
...     def extent(self):
...             return self.__class__.extent
>>> s = SuperThing()

See how we created a normal extent property that just reads from the class property? So we can now do this:

>>> s.extent
[<__main__.Thing object at 0x101c5d080>, <__main__.Thing object at 0x101c5d2b0>, <__main__.SuperThing object at 0x101c5d2e8>]

Whereas if we were to try that with one of the original Things, it wouldn’t work:

>>> t1.extent
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
AttributeError: 'Thing' object has no attribute 'extent'

We can of course still access either one via classes:

>>> t1.__class__.extent
[<__main__.Thing object at 0x101c5d080>, <__main__.Thing object at 0x101c5d2b0>, <__main__.SuperThing object at 0x101c5d2e8>]
>>> s.__class__.extent
[<__main__.Thing object at 0x101c5d080>, <__main__.Thing object at 0x101c5d2b0>, <__main__.SuperThing object at 0x101c5d2e8>]

Also note that the extent for each of these classes is the same, which shows that class properties are inherited.

Did you spot the bug in Thing? It only manifests when we have subclasses like SuperThing. We inherited the __init__ from Thing, which adds each new instance to the extent, and sets last_instance. In this case, self.__class__.extent was already initialized, on Thing, and so we added our SuperThing to the existing list. For last_instance, however, we assigned directly, rather than first reading and appending, as we did with the list property, and so SuperThing.last_instance will be our s, and Thing.last_instance will be our t2. Tread carefully, it’s easy to make a mistake with this kind of thing!

Hopefully this has been a (relatively) simple example of how to build your own class properties, with or without setters.

by Bryn Keller at June 27, 2016 12:00 AM

June 26, 2016

Dominic Steinitz

Ecology, Dynamical Systems and Inference via PMMH


In the 1920s, Lotka (1909) and Volterra (1926) developed a model of a very simple predator-prey ecosystem.

\displaystyle   \begin{aligned}  \frac{\mathrm{d}N_1}{\mathrm{d}t} & = & \rho_1 N_1  - c_1 N_1 N_2 \label{eq2a} \\  \frac{\mathrm{d}N_2}{\mathrm{d}t} & = & c_2 N_1 N_2 - \rho_2 N2 \label{eq2b}  \end{aligned}

Although simple, it turns out that the Canadian lynx and showshoe hare are well represented by such a model. Furthermore, the Hudson Bay Company kept records of how many pelts of each species were trapped for almost a century, giving a good proxy of the population of each species.

We can capture the fact that we do not have a complete model by describing our state of ignorance about the parameters. In order to keep this as simple as possible let us assume that log parameters undergo Brownian motion. That is, we know the parameters will jiggle around and the further into the future we look the less certain we are about what values they will have taken. By making the log parameters undergo Brownian motion, we can also capture our modelling assumption that birth, death and predation rates are always positive. A similar approach is taken in Dureau, Kalogeropoulos, and Baguelin (2013) where the (log) parameters of an epidemiological model are taken to be Ornstein-Uhlenbeck processes (which is biologically more plausible although adds to the complexity of the model, something we wish to avoid in an example such as this).

Andrieu, Doucet, and Holenstein (2010) propose a method to estimate the parameters of such models (Particle Marginal Metropolis Hastings aka PMMH) and the domain specific probabilistic language LibBi (Murray (n.d.)) can be used to apply this (and other inference methods).

For the sake of simplicity, in this blog post, we only model one parameter as being unknown and undergoing Brownian motion. A future blog post will consider more sophisticated scenarios.

A Dynamical System Aside

The above dynamical system is structurally unstable (more on this in a future post), a possible indication that it should not be considered as a good model of predator–prey interaction. Let us modify this to include carrying capacities for the populations of both species.

\displaystyle   \begin{aligned}  \frac{\mathrm{d}N_1}{\mathrm{d}t} & = & \rho_1 N_1 \bigg(1 - \frac{N_1}{K_1}\bigg) - c_1 N_1 N_2 \\  \frac{\mathrm{d}N_2}{\mathrm{d}t} & = & -\rho_2 N_2 \bigg(1 + \frac{N_2}{K_2}\bigg) + c_2 N_1 N_2  \end{aligned}

Data Generation with LibBi

Let’s generate some data using LibBi.

// Generate data assuming a fixed growth rate for hares rather than
// e.g. a growth rate that undergoes Brownian motion.

model PP {
  const h         = 0.1;    // time step
  const delta_abs = 1.0e-3; // absolute error tolerance
  const delta_rel = 1.0e-6; // relative error tolerance

  const a  = 5.0e-1 // Hare growth rate
  const k1 = 2.0e2  // Hare carrying capacity
  const b  = 2.0e-2 // Hare death rate per lynx
  const d  = 4.0e-1 // Lynx death rate
  const k2 = 2.0e1  // Lynx carrying capacity
  const c  = 4.0e-3 // Lynx birth rate per hare

  state P, Z       // Hares and lynxes
  state ln_alpha   // Hare growth rate - we express it in log form for
                   // consistency with the inference model
  obs P_obs        // Observations of hares

  sub initial {
    P ~ log_normal(log(100.0), 0.2)
    Z ~ log_normal(log(50.0), 0.1)

  sub transition(delta = h) {
    ode(h = h, atoler = delta_abs, rtoler = delta_rel, alg = 'RK4(3)') {
      dP/dt =  a * P * (1 - P / k1) - b * P * Z
      dZ/dt = -d * Z * (1 + Z / k2) + c * P * Z

  sub observation {
    P_obs ~ log_normal(log(P), 0.1)

We can look at phase space starting with different populations and see they all converge to the same fixed point.

Data Generation with Haskell

Since at some point in the future, I plan to produce Haskell versions of the methods given in Andrieu, Doucet, and Holenstein (2010), let’s generate the data using Haskell.

> {-# OPTIONS_GHC -Wall                     #-}
> {-# OPTIONS_GHC -fno-warn-name-shadowing  #-}
> module LotkaVolterra (
>     solLv
>   , solPp
>   , h0
>   , l0
>   , baz
>   , logBM
>   , eulerEx
>   )where
> import Numeric.GSL.ODE
> import Numeric.LinearAlgebra
> import Data.Random.Source.PureMT
> import Data.Random hiding ( gamma )
> import Control.Monad.State

Here’s the unstable model.

> lvOde :: Double ->
>          Double ->
>          Double ->
>          Double ->
>          Double ->
>          [Double] ->
>          [Double]
> lvOde rho1 c1 rho2 c2 _t [h, l] =
>   [
>     rho1 * h - c1 * h * l
>   , c2 * h * l - rho2 * l
>   ]
> lvOde _rho1 _c1 _rho2 _c2 _t vars =
>   error $ "lvOde called with: " ++ show (length vars) ++ " variable"
> rho1, c1, rho2, c2 :: Double
> rho1 = 0.5
> c1 = 0.02
> rho2 = 0.4
> c2 = 0.004
> deltaT :: Double
> deltaT = 0.1
> solLv :: Matrix Double
> solLv = odeSolve (lvOde rho1 c1 rho2 c2)
>                  [50.0, 50.0]
>                  (fromList [0.0, deltaT .. 50])

And here’s the stable model.

> ppOde :: Double ->
>          Double ->
>          Double ->
>          Double ->
>          Double ->
>          Double ->
>          Double ->
>          [Double] ->
>          [Double]
> ppOde a k1 b d k2 c _t [p, z] =
>   [
>     a * p * (1 - p / k1) - b * p * z
>   , -d * z * (1 + z / k2) + c * p * z
>   ]
> ppOde _a _k1 _b _d _k2 _c _t vars =
>   error $ "ppOde called with: " ++ show (length vars) ++ " variable"
> a, k1, b, d, k2, c :: Double
> a = 0.5
> k1 = 200.0
> b = 0.02
> d = 0.4
> k2 = 50.0
> c = 0.004
> solPp :: Double -> Double -> Matrix Double
> solPp x y = odeSolve (ppOde a k1 b d k2 c)
>                  [x, y]
>                  (fromList [0.0, deltaT .. 50])
> gamma, alpha, beta :: Double
> gamma = d / a
> alpha = a / (c * k1)
> beta  = d / (a * k2)
> fp :: (Double, Double)
> fp = ((gamma + beta) / (1 + alpha * beta), (1 - gamma * alpha) / (1 + alpha * beta))
> h0, l0 :: Double
> h0 = a * fst fp / c
> l0 = a * snd fp / b
> foo, bar :: Matrix R
> foo = matrix 2 [a / k1, b, c, negate d / k2]
> bar = matrix 1 [a, d]
> baz :: Maybe (Matrix R)
> baz = linearSolve foo bar

This gives a stable fixed point of

ghci> baz
  Just (2><1)
   [ 120.00000000000001
   ,               10.0 ]

Here’s an example of convergence to that fixed point in phase space.

The Stochastic Model

Let us now assume that the Hare growth parameter undergoes Brownian motion so that the further into the future we go, the less certain we are about it. In order to ensure that this parameter remains positive, let’s model the log of it to be Brownian motion.

\displaystyle   \begin{aligned}  \frac{\mathrm{d}N_1}{\mathrm{d}t} & = & \rho_1 N_1 \bigg(1 - \frac{N_1}{K_1}\bigg) - c_1 N_1 N_2 \\  \frac{\mathrm{d}N_2}{\mathrm{d}t} & = & -\rho_2 N_2 \bigg(1 + \frac{N_2}{K_2}\bigg) + c_2 N_1 N_2 \\  \mathrm{d} \rho_1 & = & \rho_1 \sigma_{\rho_1} \mathrm{d}W_t  \end{aligned}

where the final equation is a stochastic differential equation with W_t being a Wiener process.

By Itô we have

\displaystyle   \mathrm{d} (\log{\rho_1}) = - \frac{\sigma_{\rho_1}^2}{2} \mathrm{d} t + \sigma_{\rho_1} \mathrm{d}W_t

We can use this to generate paths for \rho_1.

\displaystyle   \rho_1(t + \Delta t) = \rho_1(t)\exp{\bigg(- \frac{\sigma_{\rho_1}^2}{2} \Delta t + \sigma_{\rho_1} \sqrt{\Delta t} Z\bigg)}

where Z \sim {\mathcal{N}}(0,1).

> oneStepLogBM :: MonadRandom m => Double -> Double -> Double -> m Double
> oneStepLogBM deltaT sigma rhoPrev = do
>   x <- sample $ rvar StdNormal
>   return $ rhoPrev * exp(sigma * (sqrt deltaT) * x - 0.5 * sigma * sigma * deltaT)
> iterateM :: Monad m => (a -> m a) -> m a -> Int -> m [a]
> iterateM f mx n = sequence . take n . iterate (>>= f) $ mx
> logBMM :: MonadRandom m => Double -> Double -> Int -> Int -> m [Double]
> logBMM initRho sigma n m =
>   iterateM (oneStepLogBM (recip $ fromIntegral n) sigma) (return initRho) (n * m)
> logBM :: Double -> Double -> Int -> Int -> Int -> [Double]
> logBM initRho sigma n m seed =
>   evalState (logBMM initRho sigma n m) (pureMT $ fromIntegral seed)

We can see the further we go into the future the less certain we are about the value of the parameter.

Using this we can simulate the whole dynamical system which is now a stochastic process.

> f1, f2 :: Double -> Double -> Double ->
>           Double -> Double ->
>           Double
> f1 a k1 b p z = a * p * (1 - p / k1) - b * p * z
> f2 d k2 c p z = -d * z * (1 + z / k2) + c * p * z
> oneStepEuler :: MonadRandom m =>
>                 Double ->
>                 Double ->
>                 Double -> Double ->
>                 Double -> Double -> Double ->
>                 (Double, Double, Double) ->
>                 m (Double, Double, Double)
> oneStepEuler deltaT sigma k1 b d k2 c (rho1Prev, pPrev, zPrev) = do
>     let pNew = pPrev + deltaT * f1 (exp rho1Prev) k1 b pPrev zPrev
>     let zNew = zPrev + deltaT * f2 d k2 c pPrev zPrev
>     rho1New <- oneStepLogBM deltaT sigma rho1Prev
>     return (rho1New, pNew, zNew)
> euler :: MonadRandom m =>
>          (Double, Double, Double) ->
>          Double ->
>          Double -> Double ->
>          Double -> Double -> Double ->
>          Int -> Int ->
>          m [(Double, Double, Double)]
> euler stateInit sigma k1 b d k2 c n m =
>   iterateM (oneStepEuler (recip $ fromIntegral n) sigma k1 b d k2 c)
>            (return stateInit)
>            (n * m)
> eulerEx :: (Double, Double, Double) ->
>            Double -> Int -> Int -> Int ->
>            [(Double, Double, Double)]
> eulerEx stateInit sigma n m seed =
>   evalState (euler stateInit sigma k1 b d k2 c n m) (pureMT $ fromIntegral seed)

We see that the populations become noisier the further into the future we go.

Notice that the second order effects of the system are now to some extent captured by the fact that the growth rate of Hares can drift. In our simulation, this is demonstrated by our decreasing lack of knowledge the further we look into the future.


Now let us infer the growth rate using PMMH. Here’s the model expressed in LibBi.

// Infer growth rate for hares

model PP {
  const h         = 0.1;    // time step
  const delta_abs = 1.0e-3; // absolute error tolerance
  const delta_rel = 1.0e-6; // relative error tolerance

  const a  = 5.0e-1 // Hare growth rate - superfluous for inference
                    // but a reminder of what we should expect
  const k1 = 2.0e2  // Hare carrying capacity
  const b  = 2.0e-2 // Hare death rate per lynx
  const d  = 4.0e-1 // Lynx death rate
  const k2 = 2.0e1  // Lynx carrying capacity
  const c  = 4.0e-3 // Lynx birth rate per hare

  state P, Z       // Hares and lynxes
  state ln_alpha   // Hare growth rate - we express it in log form for
                   // consistency with the inference model
  obs P_obs        // Observations of hares
  param mu, sigma  // Mean and standard deviation of hare growth rate
  noise w          // Noise

  sub parameter {
    mu ~ uniform(0.0, 1.0)
    sigma ~ uniform(0.0, 0.5)

  sub proposal_parameter {
     mu ~ truncated_gaussian(mu, 0.02, 0.0, 1.0);
     sigma ~ truncated_gaussian(sigma, 0.01, 0.0, 0.5);

  sub initial {
    P ~ log_normal(log(100.0), 0.2)
    Z ~ log_normal(log(50.0), 0.1)
    ln_alpha ~ gaussian(log(mu), sigma)

  sub transition(delta = h) {
    w ~ normal(0.0, sqrt(h));
    ode(h = h, atoler = delta_abs, rtoler = delta_rel, alg = 'RK4(3)') {
      dP/dt =  exp(ln_alpha) * P * (1 - P / k1) - b * P * Z
      dZ/dt = -d * Z * (1 + Z / k2) + c * P * Z
      dln_alpha/dt = -sigma * sigma / 2 - sigma * w / h

  sub observation {
    P_obs ~ log_normal(log(P), 0.1)

Let’s look at the posteriors of the hyper-parameters for the Hare growth parameter.

The estimate for \mu is pretty decent. For our generated data, \sigma =0 and given our observations are quite noisy maybe the estimate for this is not too bad also.

Appendix: The R Driving Code

All code including the R below can be downloaded from github but make sure you use the straight-libbi branch and not master.


rm(list = ls(all.names=TRUE))

try(detach(package:RBi, unload = TRUE), silent = TRUE)
library(RBi, quietly = TRUE)


library('ggplot2', quietly = TRUE)
library('gridExtra', quietly = TRUE)

endTime <- 50

PP <- bi_model("")
synthetic_dataset_PP <- bi_generate_dataset(endtime=endTime,
                                            add_options = list(

rdata_PP <- bi_read(synthetic_dataset_PP)

df <- data.frame(rdata_PP$P$nr,

ggplot(df, aes(rdata_PP$P$nr, y = Population, color = variable), size = 0.1) +
    geom_line(aes(y = rdata_PP$P$value, col = "Hare"), size = 0.1) +
    geom_line(aes(y = rdata_PP$Z$value, col = "Lynx"), size = 0.1) +
    geom_point(aes(y = rdata_PP$P_obs$value, col = "Observations"), size = 0.1) +
    theme(legend.position="none") +
    ggtitle("Example Data") +
    xlab("Days") +
          axis.title=element_text(size=6,face="bold")) +
    theme(plot.title = element_text(size=10))

synthetic_dataset_PP1 <- bi_generate_dataset(endtime=endTime,
                                             init = list(P = 100, Z=50),
                                             add_options = list(

rdata_PP1 <- bi_read(synthetic_dataset_PP1)

synthetic_dataset_PP2 <- bi_generate_dataset(endtime=endTime,
                                             init = list(P = 150, Z=25),
                                             add_options = list(

rdata_PP2 <- bi_read(synthetic_dataset_PP2)

df1 <- data.frame(hare = rdata_PP$P$value,
                  lynx = rdata_PP$Z$value,
                  hare1 = rdata_PP1$P$value,
                  lynx1 = rdata_PP1$Z$value,
                  hare2 = rdata_PP2$P$value,
                  lynx2 = rdata_PP2$Z$value)

ggplot(df1) +
    geom_path(aes(x=df1$hare,  y=df1$lynx, col = "0"), size = 0.1) +
    geom_path(aes(x=df1$hare1, y=df1$lynx1, col = "1"), size = 0.1) +
    geom_path(aes(x=df1$hare2, y=df1$lynx2, col = "2"), size = 0.1) +
    theme(legend.position="none") +
    ggtitle("Phase Space") +
    xlab("Hare") +
    ylab("Lynx") +
          axis.title=element_text(size=6,face="bold")) +
    theme(plot.title = element_text(size=10))

PPInfer <- bi_model("")

bi_object_PP <- libbi(client="sample", model=PPInfer, obs = synthetic_dataset_PP)

bi_object_PP$run(add_options = list(
                     "end-time" = endTime,
                     noutputs = endTime,
                     nsamples = 4000,
                     nparticles = 128,
                     nthreads = 1),
                 ## verbose = TRUE,
                 stdoutput_file_name = tempfile(pattern="pmmhoutput", fileext=".txt"))


mu <- bi_read(bi_object_PP, "mu")$value
g1 <- qplot(x = mu[2001:4000], y = ..density.., geom = "histogram") + xlab(expression(mu))
sigma <- bi_read(bi_object_PP, "sigma")$value
g2 <- qplot(x = sigma[2001:4000], y = ..density.., geom = "histogram") + xlab(expression(sigma))
g3 <- grid.arrange(g1, g2)

df2 <- data.frame(hareActs = rdata_PP$P$value,
                  hareObs  = rdata_PP$P_obs$value)

ggplot(df, aes(rdata_PP$P$nr, y = value, color = variable)) +
    geom_line(aes(y = rdata_PP$P$value, col = "Phyto")) +
    geom_line(aes(y = rdata_PP$Z$value, col = "Zoo")) +
    geom_point(aes(y = rdata_PP$P_obs$value, col = "Phyto Obs"))

ln_alpha <- bi_read(bi_object_PP, "ln_alpha")$value

P <- matrix(bi_read(bi_object_PP, "P")$value,nrow=51,byrow=TRUE)
Z <- matrix(bi_read(bi_object_PP, "Z")$value,nrow=51,byrow=TRUE)

data50 <- bi_generate_dataset(endtime=endTime,
                              add_options = list(

rdata50 <- bi_read(data50)

df3 <- data.frame(days = c(1:51), hares = rowMeans(P), lynxes = rowMeans(Z),
                                  actHs = rdata50$P$value, actLs = rdata50$Z$value)

ggplot(df3) +
    geom_line(aes(x = days, y = hares, col = "Est Phyto")) +
    geom_line(aes(x = days, y = lynxes, col = "Est Zoo")) +
    geom_line(aes(x = days, y = actHs, col = "Act Phyto")) +
    geom_line(aes(x = days, y = actLs, col = "Act Zoo"))


Andrieu, Christophe, Arnaud Doucet, and Roman Holenstein. 2010. “Particle Markov chain Monte Carlo methods.” Journal of the Royal Statistical Society. Series B: Statistical Methodology 72 (3): 269–342. doi:10.1111/j.1467-9868.2009.00736.x.

Dureau, Joseph, Konstantinos Kalogeropoulos, and Marc Baguelin. 2013. “Capturing the time-varying drivers of an epidemic using stochastic dynamical systems.” Biostatistics (Oxford, England) 14 (3): 541–55. doi:10.1093/biostatistics/kxs052.

Lotka, Alfred J. 1909. “Contribution to the Theory of Periodic Reactions.” The Journal of Physical Chemistry 14 (3): 271–74. doi:10.1021/j150111a004.

Murray, Lawrence M. n.d. “Bayesian State-Space Modelling on High-Performance Hardware Using LibBi.”

Volterra, Vito. 1926. “Variazioni e fluttuazioni del numero d’individui in specie animali conviventi.” Memorie Della R. Accademia Dei Lincei 6 (2): 31–113.{\_}e{\_}fluttuazioni/pdf/volterra{\_}variazioni{\_}e{\_}fluttuazioni.pdf.

by Dominic Steinitz at June 26, 2016 12:53 PM

June 25, 2016

José Pedro Magalhães

Marie Curie individual fellowship application text

Back in 2014 I applied for a Marie Curie fellowship. This was towards the end of my postdoc at Oxford, and then I got my current position at Standard Chartered before I heard back from the European Commission on the results of the Marie Curie. It was accepted with a score of 96%, which is something I'm very proud of, and also very thankful to everyone who helped me prepare the submission.
However, it is now clear that I will not be taking that position, as I am settled in London and at Standard Chartered. I still quite like the proposal, though, and, when writing it, I remember having wanted to see examples of successful Marie Curie proposals to have an idea of what they would look like. As such, I'm making the text of my own Marie Curie fellowship application available online. I hope this can help others to write successful applications, and maybe some of its ideas can be taken on by other researchers. Feel free to adapt any of the ideas in the proposal (but please give credit when it is due, and remember that the European Commission uses plagiarism detection software). It's available on my website, and linked below. I made the LaTeX template for the application available before.

José Pedro Magalhães. Models of Structure in Music (MoStMusic). Marie Sklodowska-Curie Individual Fellowship application, 2014.

by José Pedro Magalhães ( at June 25, 2016 11:22 AM

June 24, 2016

Philip Wadler

A sad day

I don't know what to say. I feel let down, and I feel the UK has let the world down, as well as itself.

by Philip Wadler ( at June 24, 2016 10:08 AM

June 23, 2016

wren gayle romano

Self-improvement goals, overcoming perfectionism, and dissertating

This year's self-improvement goal was to get back into blogging regularly. Part of that goal was just to get back into writing regularly; the other part was specifically to publish more regularly.

I've done fairly well on the first half, actually. I'd hoped to do better, but then all year I've had to deal with spoon-draining circumstances, so I've probably done about as well as I can without sacrificing my health. One of my other self-improvement goals has been to take my health seriously, to listen to my body rather than pushing it beyond its limits. I'm on-track for improving at both of these, I just need to stop beating myself up over it.

For the second half, the publishing bit, that I've done poorly. I'd like to blame the spoon vortex here too, but really I think the biggest problem is my perfectionism. Perfectionism greatly amplifies the problem of lacking spoons: both the editing itself, as well as the emotional fallout of missing the mark or of having taken the entire day to hit it, both of these cost spoons. The real aim behind my goal to publish regularly wasn't to have more words to my name, but rather to “get out there” more, to be more productive in-and-of-itself rather than to have more products. So I've started thinking: the real target for this self-improvement goal should not be publishing regularly, but rather should be (working to) overcome perfectionism.

If perfectionism is a problem of fear, then the thing I must address is that fear. So how to do it? One of the suggestions in that article is to let yourself fail. Not to lower your unreasonable standards (the party-line for what to do), but rather to allow yourself to not meet those standards. One of my standards is to be thought provoking, and hence to focus overmuch on essays. To try and break free from this, I'm thinking to start posting summaries of my daily dissertation progress. A nanowrimo sort of thing, though without the focus on word-count per se. I've read a few articles suggesting one should start their day by summarizing the previous day's progress, but I've never tried it. So here goes nothing :)

comment count unavailable comments

June 23, 2016 08:43 PM


Type 'Int' does not match type 'Int'

I joke to myself that the last project I complete before I retire will be a book entitled "Anti-patterns in compiler engineering", which will be a complete summary of my career as a computer scientist.

I spent a couple of days last week undoing one particular anti-pattern which was causing bogus error messages like: "Type 'Int' does not match type 'Int'". In DDC the root cause these messages was invariably this data type:

data Bound n
= UIx Int -- An anonymous, deBruijn variable.
| UName n -- A named variable or constructor.
| UPrim n (Type n) -- A primitive value (or type) with its type (or kind).
A value of type Bound n represents the bound occurrence of a variable or constructor, where n is the underlying type used for names. In practice n is often Text or String. The data type has three constructors, UIx for occurrences of anonymous variables, UName for named variables and constructors, and UPrim for names of primitives. We use Bound type for both terms and types.

The intent was that when type checking an expression, to determine the type (or kind) of a Bound thing in UIx or UName form, we would look it up in the type environment. However, as the types (and kinds) of primitives are fixed by the language definition, we would have their types attached directly to the UPrim constructor and save ourselves the cost of environment lookup. For example, we would represent the user defined type constructor 'List' as (UName "List"), but the primitive type constructor 'Int' as (UPrim "Int" kStar), where 'kStar' refers to the kind of data types.

The pain begins the first time you accidentally represent a primitive type constructor in the wrong form. Suppose you're parsing type constructor names from a source file, and happen to represent Int as (UName "Int") instead of (UPrim "Int" kData). Both versions are pretty printed as just "Int", so dumping the parsed AST does not reveal the problem. However, internally in the compiler the types of primitive operators like add and mul are all specified using the (UPrim "Int" kData) form, and you can't pass a value of type (UName "Int") to a function expecting a (UPrim "Int" kData). The the uninformative error message produced by the compiler simply "Type 'Int' does not match type 'Int'", disaster.

The first time this happens it takes an hour to find the problem, but when found you think "oh well, that was a trivial mistake, I can just fix this instance". You move on to other things, but next week it happens again, and you spend another hour -- then a month later it happens again and it takes two hours to find. In isolation each bug is fixable, but after a couple of years this reoccurring problem becomes a noticeable drain on your productivity. When new people join the project they invariably hit the same problem, and get discouraged because the error message on the command line doesn't give any hints about what might be wrong, or how to fix it.

A better way to handle names is to parameterise the data types that represent your abstract syntax tree with separate types for each different sort of name: for the bound and binding occurrences of variables, for bound and binding occurrences of constructors, and for primitives. If the implementation is in Haskell we can use type families to produce the type of each name based on a common index type, like so:

type family BindVar l
type family BoundVar l
type family BindCon l
type family BoundCon l
type family Prim l

data Exp l
= XVar (BoundVar l)
| XCon (BoundCon l)
| XPrim (Prim l)
| XLam (BindVar l) (Exp l)
DDC now uses this approach for the representation of the source AST. To represent all names by a single flat text value we define a tag type to represent this variation, then give instances for each of the type families:

data Flat = Flat

type instance BindVar Flat = Text
type instance BoundVar Flat = Text
type instance BindCon Flat = Text
type instance BoundCon Flat = Text
type instance Prim Flat = Text

type ExpFlat = Exp Flat
On the other hand, if we want a form that allows deBruijn indices for variables, and uses separate types for constructors and primitives we can use:

data Separate = Separate

data Bind = BAnon | BName Text
data Bound = UIx Int | UName Text
data ConName = ConName Text
data PrimName = PrimName Text

type instance BindVar Separate = Bind
type instance BoundVar Separate = Bound
type instance BindCon Separate = ConName
type instance BoundCon Separate = ConName
type instance Prim Separate = PrimName

type ExpSeparate = Exp Separate
It's also useful to convert between the above two representations. We might use ExpSeparate internally during program transformation, but use ExpFlat as an intermediate representation when pretty printing. To interface with legacy code we can also instantiate BoundVar with our old Bound type, so the new generic representation is strictly better than the old non-generic one using a hard-wired Bound.

Compiler engineering is full of traps of representation. Decisions taken about how to represent the core data structures permeate the entire project, and once made are very time consuming to change. Good approaches are also difficult to learn. Suppose we inspect the implementation of another compiler and the developers have set up their core data structures in some particular way. Is it set up like that because it's a good way to do so?, or is it set up like that because it's a bad way of doing so, but now it's too difficult to change? For the particular case of variable binding, using type like Bound above is a bad way of doing it. Using the generic representation is strictly better. Let this be a warning to future generations.

by Ben Lippmeier ( at June 23, 2016 12:48 PM

June 21, 2016

Brent Yorgey

Any clues about this Newton iteration formula with Jacobian matrix?

A while ago I wrote about using Boltzmann sampling to generate random instances of algebraic data types, and mentioned that I have some code I inherited for doing the core computations. There is one part of the code that I still don’t understand, having to do with a variant of Newton’s method for finding a fixed point of a mutually recursive system of equations. It seems to work, but I don’t like using code I don’t understand—for example, I’d like to be sure I understand the conditions under which it does work, to be sure I am not misusing it. I’m posting this in the hopes that someone reading this may have an idea.

Let \Phi : \mathbb{R}^n \to \mathbb{R}^n be a vector function, defined elementwise in terms of functions \Phi_1, \dots, \Phi_n : \mathbb{R}^n \to \mathbb{R}:

\displaystyle \Phi(\mathbf{X}) = (\Phi_1(\mathbf{X}), \dots, \Phi_n(\mathbf{X}))

where \mathbf{X} = (X_1, \dots, X_n) is a vector in \mathbb{R}^n. We want to find the fixed point \mathbf{Y} such that \Phi(\mathbf{Y}) = \mathbf{Y}.

The algorithm (you can see the code here) now works as follows. First, define \mathbf{J} as the n \times n Jacobian matrix of partial derivatives of the \Phi_i, that is,

\displaystyle \displaystyle \mathbf{J} = \begin{bmatrix} \frac{\partial}{\partial X_1} \Phi_1 & \dots & \frac{\partial}{\partial X_n} \Phi_1 \\ \vdots & \ddots & \vdots \\ \frac{\partial}{\partial X_1} \Phi_n & \dots & \frac{\partial}{\partial X_n} \Phi_n\end{bmatrix}

Now let \mathbf{Y}_0 = (0, \dots, 0) and let \mathbf{U}_0 = I_n be the n \times n identity matrix. Then for each i \geq 0 define

\displaystyle \mathbf{U}_{i+1} = \mathbf{U}_i + \mathbf{U}_i(\mathbf{J}(\mathbf{Y}_i)\mathbf{U}_i - (\mathbf{U}_i - I_n))

and also

\displaystyle \mathbf{Y}_{i+1} = \mathbf{Y}_i + \mathbf{U}_{i+1}(\Phi(\mathbf{Y}_i) - \mathbf{Y}_i).

Somehow, magically (under appropriate conditions on \Phi, I presume), the sequence of \mathbf{Y}_i converge to the fixed point \mathbf{Y}. But I don’t understand where this is coming from, especially the equation for \mathbf{U}_{i+1}. Most generalizations of Newton’s method that I can find seem to involve multiplying by the inverse of the Jacobian matrix. So what’s going on here? Any ideas/pointers to the literature/etc?

by Brent at June 21, 2016 04:35 PM

Functional Jobs

Haskell Software Engineer at Wrinkl, Inc. (Full-time)

Based in New York City, Wrinkl, Inc. is a next generation SaaS communication platform. Wrinkl is a well-funded startup company with an innovative approach that has received interest from Fortune 500 companies and industry thought leaders. The company’s co-founders each have 30+ years of experience as successful entrepreneurs and in private equity and M&A. Wrinkl has assembled a group of sophisticated investors, advisors and potential beta partners who are committed to success.

Currently, Wrinkl is working with Obsidian Systems, a leading Haskell software consulting company that uses a combination of cutting-edge and tried-and-true technologies to build custom software solutions, which range from seed-stage startups to multinational corporations. Wrinkl’s technology stack is based on Haskell, Reflex and Reflex-DOM, GHCJS, NixOS, PostgresSQL and AWS. Wrinkl is looking to hire experienced and capable Haskell developers to initially work with Obsidian Systems and to be the core on which our in-house technology development team is built.

Wrinkl is building a world-class team that enjoys an intellectually challenging and high-energy environment. We want developers who are fully invested, enthusiastic and take great pride in their work. Wrinkl also fully appreciates the need to live a balanced life and values productive output over face time.

While we are located in New York City, and we will be hiring people locally, remote work is also available. If you are highly proficient with front-end and/or back-end architecture and have a passion for innovation, we would love to tell you more about our exciting opportunity.

Wrinkl provides its developers a competitive compensation package, including cash, equity and health care coverage.


Haskell Developers with experience working on Haskell web and mobile applications. You’ll be working with a team of developers on all levels of our full-stack functional application. Our developers work in quick iterations to build complete features (from database to frontend) with a focus on quality, maintainability, and performance.

Chief Technology Officer with a successful history in managing a development team, specifically for mobile and web apps. The CTO will collaborate closely with the founders to co-create the product and technology strategy, staffing model and delivery plans to realize the full potential of the business. This responsibility includes the planning, development, and implementation of Wrinkl’s application architecture, technology stack and product experience on various platforms including desktop, mobile and native applications (iOS and Android).

Get information on how to apply for this position.

June 21, 2016 02:54 PM

June 20, 2016

The GHC Team

Contributing to GHC

This post is a response to Anthony's blog post about contributing to GHC, and the subsequent Reddit discussion. You'll find it easier to follow my comments below if you read Anthony's post first. Short summary: many of Anthony's criticisms are accurate, but they are not easy to address, especially in a volunteer-only project. However we will do something about the feature-request process.

Barrier to entry

I am ashamed that GHC seems difficult to contribute to. The details don't matter; the fact that it made you feel that way is by definition bad. I'm really sorry. We should find a way to do better.

An underlying issue is one of effort budget. GHC has essentially no full-timers, unlike many open-source projects. In particular, Simon Marlow and I are volunteers like everyone else, and like everyone else we have a day job. Microsoft Research generously pays Well Typed for front-line support, manifested in the heroic form of Ben and Austin, totalling around one FTE. But their effort is fully absorbed by managing releases, reviewing patches, maintaining the infrastructure, and so on.

It's a real challenge to maintain a low barrier to entry for a large complex project, whose motive force is primarily volunteers. It means that any initiative will only fly if someone steps up to drive it.

Technical documentation

The questions of scattered and inconsistent documentation are difficult to address. GHC is twenty-five years old; it has hundreds of authors and documentation that was once accurate falls out of date. I would love it to have consistent, well-explained documentation. But I don't know how to achieve it.

GHC's technical documentation is either in the code itself, or on GHC's wiki. An advantage of a wiki is that anyone can edit it. Yes, instructions and technical descriptions go out of date. Who will fix them? You, gentle reader! There is no one else.

But in practice few do. Perhaps that's because such work is invisible, so no one even knows you've done it? What would make people feel "I'd really like to improve those instructions or that documentation?"

I will argue for two things. First, I find Notes incredibly helpful. They live with the code, so they are less likely to go out of date. They don't mess up the flow of the code. They can be referred to from multiple places. They are the single most successful code documentation mechanism we have. (To be fair to Anthony, I don't think was complaining about Notes, just expressing surprise.)

Second, I really do think that each new proposed feature needs a description, somewhere, of what it is, why it's a good thing, and as precisely as possible what its specification is. Plus perhaps some implementation notes. It's very important when reading an implementation to know what it is that the code is seeking to implement. So yes, I do frequently ask for a specification.

Arc, github, phabricator, etc

Personally I carry no torch for arc. I do whatever I'm told, workflow-wise. If GitHub has got a lot better since we took the Arc decision, and there's a consensus that we should shift, I'm all for it provided someone explains to me what my new workflows should be. I am absolutely in favour of reducing barriers to contribution. (Other members of the GHC team have much stronger and better informed views than me, though.)

But there are costs to moving, especially if the move implies friction in the future. In particular, those that worry me most are those surrounding issue tracking. Github's issue tracker simply doesn't seem sufficient for a project as large and multi-faceted as GHC; in particular, tags as the only form of metadata is extremely limiting.

One alternative would be to use Github and Trac side-by-side, but then we face the issue of conflicting ticket number spaces as both systems insist on ticket numbers of the form #NNNN.

Coding style

Coding style is rather a personal thing, and we have been reluctant to enforce a single uniform style. (Quite apart from the task of reformatting 150k lines of Haskell.) Personally I don't find it an obstacle to reading other people's code.

Feature requests

That leaves the most substantial issue that Anthony poses: the process of making a contribution.

For fixing a bug, I think that (aside from the arc/Github debate) things are not too bad. On the arc/Github question, Austin has been working with the Phabricator maintainers to try to have them introduce a workflow which might be more familiar and more convenient for Github experts.

But for offering a new feature, Anthony argues that the process is unacceptably arduous. There are lots of things to think about

  • GHC has tons of features implemented by talented and motivated folk... who have since moved on. So when a new feature is proposed, my baseline guess is that I will personally be responsible for maintaining it in five years time. So I want to understand what the feature is. I want to understand how the implementation works. I want to be reasonably sure that it doesn't add a bunch of complexity to an already very complicated code base. And since any new feature adds some complexity, I want to have some confidence that the feature commands broad support -- even when it's behind a language extension flag.

So actually I think it's reasonable that the process should be somewhat arduous. A new feature imposes costs on every single person who works on that code in the future. We don't really make this point explicitly, but the contributor guidelines for Phabricator do. It might be helpful if we articulated similar guidelines.

  • "Any proposal needs a lightweight way to gauge broad support, then a period of constructive refinement". Indeed! What would be such a lightweight way? The trouble is that there is an enormous silent majority, and discussions are typically driven by a handful of articulate and well-informed contributors. All credit to them, but they may very well be an unrepresentative sample. I simply don't know how to gauge true broad support.
  • There is a problem with my own personal lack of bandwidth. I am one of the main gatekeepers for some big chunks of GHC, the renamer, typechecker and optimisation passes. That is good in a way, because if GHC lacked gatekeepers, it would soon lose conceptual integrity and become a huge ball of mud. But it is bad in other ways. I review a lot of code; but not fast enough! In prioritising I am guided by my (doubtless flawed) perceptions of things that lots of people are eagerly awaiting. The same thing goes for Simon Marlow, especially in the runtime system. We both have other day jobs. Even writing this post means that I'm not reviewing someone's code.

But I am acutely aware that "Simon and Simon are busy" is pretty cold comfort to someone awaiting a review. Maybe there should be a bunch of other people playing this role. That would be great. For example, Richard Eisenberg has taken responsibility for Template Haskell, which is totally fantastic. I would love to hear from people who are willing to take overall responsibility for a piece of GHC.

None of this is an argument for the status quo. Simon, Ben, Austin, Herbert, and I have been talking about a rather more systematic process for new features. We'd like to learn from experience elsewhere, rather than reinvent the wheel, such as the Rust process. Please suggest processes that you have seen working well elsewhere.

by simonpj at June 20, 2016 12:35 PM

FP Complete

async exceptions, STM, and deadlocks

For a change of pace, I wanted to cover a simple topic: asynchronous exceptions, and how they interact with Software Transactional Memory and MVars, as well as the GHC runtime system's deadlock detection. As fate would have it, the topics in question occurred twice in the past month, once in a bug report against the yaml package, and once in a major refactoring of FP Complete's distributed computation platform. I'll focus on the first since it's an easier case to explain, but I'll try to explain the second (and jucier) one too.

To get this started off nicely, I'll share an interesting piece of code and its output. If you're playing along at home, try guessing what the output of this program will be, and if your guess is different from the actual output, try to predict why. Hopefully, by the end of this post, it will be clear (although still perhaps surprising).

#!/usr/bin/env stack
-- stack --resolver ghc-7.10.3 runghc
import Control.Concurrent
import Control.Exception

mayThrow1, mayThrow2, mayThrow3 :: IO Int

mayThrow1 = return 5 -- nope, don't throw

mayThrow2 = error "throw a normal exception"

mayThrow3 = do
    var <- newEmptyMVar
    takeMVar var -- BlockedIndefinitelyOnMVar, always!

-- implements the idea from:
-- Don't use the async package, which already works around the bug
-- I'm demonstrating!
tryAny :: IO a -> IO (Either SomeException a)
tryAny action = do
    var <- newEmptyMVar
    uninterruptibleMask_ $ forkIOWithUnmask $ \restore -> do
        res <- try $ restore action
        putMVar var res
    takeMVar var

main :: IO ()
main = do
    tryAny mayThrow1 >>= print
    tryAny mayThrow2 >>= print
    tryAny mayThrow3 >>= print

    putStrLn "done!"

And actual output:

Right 5
Left throw a normal exception
example1.hs: thread blocked indefinitely in an MVar operation

To clarify, that last line of output means that the program itself exited because a BlockedIndefinitelyOnMVar exception was thrown to the main thread and was not caught. Also, this is possibly the first time I've written an interesting code example for a blog post that uses only the base package :)

Synchronous vs asynchronous exceptions

There are two* ways an exception can be thrown in Haskell:

  • Synchronous exceptions are generated by the current thread. What's important about these is that we generally want to be able to recover from them. For example, if you try to read from a file, and the file doesn't exist, you may wish to use some default value instead of having your program exit, or perhaps prompt the user for a different file location.

  • Asynchronous exceptions are thrown by either a different user thread, or by the runtime system itself. For example, in the async package, race will kill the longer-running thread with an asynchronous exception. Similarly, the timeout function will kill an action which has run for too long. And epic foreshadowment the runtime system will kill threads which appear to be deadlocked on MVars or STM actions.

    In contrast to synchronous exceptions, we almost never want to recover from asynchronous exceptions. In fact, this is a common mistake in Haskell code, and from what I've seen has been the largest source of confusion and concern amongst users when it comes to Haskell's runtime exception system.

Alright, got that? Catch the synchronous ones and recover, never recover from asynchronous exceptions**.

* You could argue that creating an exception in a pure value, via functions like error and undefined, is a third category. We're going to ignore that for now.

** You may be wondering "why make it possible to catch async exceptions if we can't recover from them?" The answer is that we still want to be able to perform cleanup actions, like closing file handles. This is the topic of the aforementioned upcoming blog post.

Catching all exceptions

Quite a few years ago, I wrote a School of Haskell article on how to catch all exceptions. I'm not going to rehash that article here, since (1) the content is still current, and (2) I'll likely be sharing a new blog post in a few days with a newer approach. But the gist of it is that if we want to catch all synchronous exceptions in an action without catching asynchronous ones, we run that action in a separate thread, and then grab the result from that thread using a mutable variable. The SoH article uses the async package, which hides away some of the details. However, the core idea is easy enough to express as I did above:

tryAny :: IO a -> IO (Either SomeException a)
tryAny action = do
    var <- newEmptyMVar
    uninterruptibleMask_ $ forkIOWithUnmask $ \restore -> do
        res <- try $ restore action
        putMVar var res
    takeMVar var

Let's address some important points in the design of this function, since it has to step quite carefully around asynchronous exceptions:

  • We use forkIOWithUnmask to ensure that the newly created thread has asynchronous exceptions masked. This means that we will receive no async exceptions in the new thread, until we wrap an exception with the restore function.
  • We restore the user's action, meaning async exceptions can be received there. But we wrap that restore action with a try, catching all synchronous and asynchronous exceptions.
  • Since outside of the try we still have all async exceptions masked, there's nothing preventing the putMVar call in the child thread from being called. This means that, in all cases of the action terminating, the putMVar will ensure that the var is filled up.
  • The takeMVar in the parent thread will block until the child thread completes. And since we're guaranteed that the var will always be filled once the action terminates, we seem (once again, epic foreshadowment) to be guaranteed that the takeMVar call will always wait for action to somehow terminate, and once it's terminated will return either the exception is died with or the success result.

Deadlock protection

Alright, I've foreshadowed enough already, I'm guessing everyone's figured out where the problem is going to come. Sure enough, if we look at the program I started this post with, we see that tryAny mayThrow3 >>= print does not catch the exception generated by mayThrow3, but instead itself dies from GHC's deadlock protection (BlockedIndefinitelyInMVar). Simon Marlow explained the reason for this to me twice, once in his (really really good) book, and once when I raised issue #14 on async because I hadn't been smart enough to connect the dots from the book to my actual issue. As long as I'm linking so much to Github, you may also like seeing my pull request to work around issue #14.

Don't worry, I'm not going to make you read all of that. The summary is pretty simple: GHC's run time system has very straightforward deadlock detection. When it finds a group of threads that are all blocked on blocking mutable variables (MVars or STM variables), and finds that no other threads have references to the variables it question, it determines that all of the threads are deadlocked, and sends all of them asynchronous exceptions (either BlockedIndefinitelyOnMVar or BlockedIndefinitelyOnSTM).

So let's analyze tryAny mayThrow3 in excruciating detail. The series of events here is:

  1. Create a new empty MVar to allow the child thread to pass back the result of mayThrow3 to the parent thread.
  2. Fork a new child thread (yes, exceptions are masked, but that's not terribly important for us).
  3. Back in the parent thread: block waiting for that empty MVar to get filled.
  4. In the child thread, set up try to catch all exceptions, and then run the user's action (with async exceptions unmasked).
  5. As it happens, I carefully crafted mayThrow3 to deadlock on an MVar. So now the child thread can't make progress, and is fully deadlocked.

OK, the stage is set: the main thread is blocked on an MVar for the result. As I proved above, we know for a fact that this MVar will ultimately be filled with the result of the user action, once the user action completes or dies with an exception. However, GHC doesn't know this, it just sees the main thread blocked on an MVar action, and that only the main thread and child thread have references to that variable.

In the child thread, we've created a new MVar deadlock. This is a true and legitimate deadlock (if you don't believe me, go back and look at the implementation of mayThrow3). So GHC decides that both the main thread and the child thread are currently blocked on MVar actions, and there is no other thread that can unblock either of them. And GHC is correct. However, the next part is the unfortunate part:

GHC kills both threads with an asynchronous exceptions

Why is this unfortunate? Because we know that if the child thread receives the async exception, it will exit, the result MVar will get filled, and the main thread can complete successfully. That's exactly the behavior we want, but not the behavior GHC is able to deliver to us.

The workaround

The workaround I'm about to demonstrate is not elegant, and it leaves a bad taste in my mouth. If anyone has a better idea, let me know. The idea is this: we know that there's no legitimate reason for the takeMVar inside tryAny to be killed with a BlockedIndefinitelyOnMVar, even if GHC doesn't know that. So we outsmart GHC by catching and ignoring that specific exception. And just in case our logic is wrong and there's a flawed implementation here, we only catch-and-ignore a fixed number of times (arbitrary choice: 10) to avoid creating a real deadlock.

I've added a commit for enclosed-exceptions that implements this behavior, but for the lazy, here's a simplified version of it:

tryAny :: IO a -> IO (Either SomeException a)
tryAny action = do
    var <- newEmptyMVar
    uninterruptibleMask_ $ forkIOWithUnmask $ \restore -> do
        res <- try $ restore action
        putMVar var res
    retryCount 10 (takeMVar var)
    retryCount cnt0 action =
        loop cnt0
        loop 0 = action
        loop cnt = action `catch`
            \BlockedIndefinitelyOnMVar -> loop (cnt - 1)

Swallow the bit of vomit rising in the back of your throat, try this out in the original program, and see if it solves the issue. You should see the following output:

Right 5
Left throw a normal exception
Left thread blocked indefinitely in an MVar operation

Note that the "thread blocked" has actually been caught, and the final done! line is actually printed.

Problem with STM-based tryAny

tryAny was already implemented safely in terms of the async package, which uses STM in place of MVars as we did here. Mitchell Rosen came up with a really convincing demonstration for why we shouldn't use STM for this purpose. To quote, with the program:

#!/usr/bin/env stack
-- stack --resolver lts-6.3 runghc --package yaml
{-# LANGUAGE OverloadedStrings #-}

import Control.Concurrent.STM
import Data.Yaml

main = do
    mval <- atomically (return $! decode "")
    print (mval :: Maybe Value)

We get the rather surprising output:

Control.Concurrent.STM.atomically was nested

The reason is that decode is calling a bunch of IO functions as FFI calls to the libyaml library, and is wrapped in unsafePerformIO to make the morally-pure YAML-decoding action not live in IO. Under the surface, it uses tryAny to avoid unexpected exceptions from breaking out of the unsafePerformIO dungeon it lives in. That's all well and good, but now if you use decode inside an atomically block, you have two layers of STM occurring, which is strictly forbidden.

Extra credit Figure out why I needed to use $! to make this fail.

Our distributed computing problem

This problem arose about two months ago, and is far more complicated than the examples I've discussed until now. In fact, I've so far been unsuccessful at reproducing this with a minimal test case, which is definitely annoying. Nonetheless, I can explain what basically happened:

  1. Have a queue of work items to be performed, represented by a TChan
  2. Have one thread (filler) grabbing work items from somewhere (like a socket) and putting them on the TChan
  3. Have another thread (worker) grabbing work items and performing them
  4. The filler has logic to detect when no more items are incoming, and exits
  5. Run these two threads together using the race function, which guarantees that once the filler exits, the worker will be killed too

Unfortunately, this runs into the same problem I described above, at least in some circumstances. The thread calling race is blocked on an MVar under the surface, which filler and worker both have access to. filler completes, puts something in the MVar, and then disappears, losing its reference to the MVar and the TChan. Meanwhile, worker is still blocked waiting on the TChan, to which only it has access now, resulting in a deadlock condition.

In our application, we ended up with a situation where the worker thread was deadlocked on the TChan, and the thread calling race was blocked on the MVar. It's a slightly more complicated case than this though, since in the simple race case, the thread calling race doesn't actually get blocked on the MVar. Nonetheless, it's another interesting case where the deadlock prevention kills too many threads.

Fortunately for our application, there's a very simple - and more robust - solution, which I recommend to anyone doing this kind of concurrent programming. The problem was that our worker thread had no logic to terminate itself, and instead just waited to be killed by race. Instead, we switched over to a closeable TChan implementation, where the filler thread could explicitly closed out the TChan and then the worker would kill itself instead of waiting around for an async exception.

So to leave this blog post with some recommendations, and a small amount of extra foreshadowment (fourth time getting to use that word in one blog post!):

  • Explicit exit conditions are better than implicit ones
  • Avoid relying on async exceptions for control flow if you can
  • Relying on the deadlock detection to clean up your messes is a bad idea
  • And even if you don't want the deadlock detection to clean up your messes, it may try to do so for you badly anyway

June 20, 2016 12:00 AM

June 18, 2016

Magnus Therning

Free, take 2

The other day I read a blog post on monads and stuff after which I felt rather silly about my earlier posts on Free.

I think this is probably the post I should have written instead :)

I’ll use three pieces of code, each one builds on the one before:

  • Free1.hs - Uses a free monad for a single algebra/API (full code here).
  • Free2.hs - Uses a free monad for a two algebras/APIs, where one decorates the other (full code here).
  • Free3.hs - Uses a free monad for a three algebras/APIs, where two are used in the program and the remaing one decorates the other two (full code here).

The first - one algebra

I’m re-using the algebras from my previous posts, but I believe it makes it easier to follow along if the amount of jumping between posts is minimized so here is the first one once again:

data SimpleFileF a
  = LoadFile FilePath (String -> a)
  | SaveFile FilePath String a

type SimpleFileAPI = Free SimpleFileF

loadFile :: FilePath -> SimpleFileAPI String
loadFile fp = liftF $ LoadFile fp id

saveFile :: FilePath -> String -> SimpleFileAPI ()
saveFile fp d = liftF $ SaveFile fp d ()

It’s a ridiculously small one, but I believe it’s good enough to work with. In the previous posts I implemented the Functor instances manually. I couldn’t be bothered this time around; I think I pretty much know how to do that for this kind of types now.

Having a type for the algebra, SimpleFileAPI, is convenient already now, even more so in the other examples.

The two convenience functions on the end makes it straight forward to write functions using the algebra:

withSimpleFile :: (String -> String) -> FilePath -> SimpleFileAPI ()
withSimpleFile f fp = do
  d <- loadFile fp
  let result = f d
  saveFile (fp ++ "_new") result

This is simple, straight forward monadic code. Easy to read and work with. Of course it doesn’t actually do anything at all yet. For that I need need an interpreter, something that translates (reduces) the algebra, the API, the commands, call them what you will, into the (side-)effects I want. For Free that is foldFree together with a suitable function f :: SimpleFileF a -> IO a.

I want LoadFile to translate to a file being read and SaveFile to some data being saved to a file. That makes it pretty obvious how that f needs to be written:

runSimpleFile :: SimpleFileAPI a -> IO a
runSimpleFile = foldFree f
    f (LoadFile fp f') = f' <$> readFile fp
    f (SaveFile fp d r) = writeFile fp d >> return r

At this point it might be good to explain the constructors of SimpleFileF a bit more. At first I thought they looked a bit funny. I mean, why does SaveFile have an a at all since it obviously always should result in ()? And what’s up with that function in Loadfile?

It did become a little clearer to me after some thought and having a look at Free:

data Free f a = Pure a | Free (f (Free f a))

I personally find the latter constructor a bit mind-bending. I can handle recursive functions fairly well, but recursive types have a tendency to confuse me. From what I understand one can think of Free as similar to a list. Pure ends the list (Nil) and Free one instance of f to the rest of the list (Cons). Since Free f a is a monad one can think of a as the result of the command.

If I were to write saveFile explicitly it’d look like this

saveFile fp d = Free (SaveFile fp d (Pure ()))

and for loadFile:

loadFile fp = Free (LoadFile fp (\ s -> Pure s))

But let’s get back to the type and why ‘a’ occurs like it does in the two constructors. As Gabriel G shows in his post Why free monads matter a constructor without a would result in termination. In other words, if SaveFile didn’t hold an a I’d not be able to write, in a natural way, a function that saves two files.

Another limiting factor is that foldFree of the Free implementation I’m using has the type Monad m => (forall x. f x -> m x) -> Free f a -> m a. This sets a requirement on what the function translating from my API into effects may look like, i.e. what f in runSimpleFile may look like. If SaveFile had no a to return what would f (SaveFile {}) return, how could it ever satisfy the required type?

The reason for LoadFile having a function String -> a is simply that there is no data yet, but I still want to be able to manipulate it. Using a function and function composition is the ticket then.

I think that’s all there is to say about to the first piece of code. To run it take a look at the comment at the end of the file and then play with it. If you want to turn all characters of a file foo into upper case you can use

runSimpleFile $ withSimpleFile (map toUpper) "foo"

The second - two algebras, one decorating the other

The second piece of code almost only adds to the first one. There is one exception though, the function runSimpleFile is removed. Instead I’ve taken the transformation function, which used to be called f and was internal to runSimpleFile and moved it out. It’s called stepSimpleFile:

stepSimpleFile :: SimpleFileF a -> IO a
stepSimpleFile (LoadFile fp f') = f' <$> readFile fp
stepSimpleFile (SaveFile fp d r) = writeFile fp d >> return r

The logging API, LogAPI, follows the same pattern as SimpleFileAPI and I’m counting on the description above being clear enough to not have to repeat myself. For completeness I include the code:

data LogF a = Log String a

type LogAPI = Free LogF

stepLog :: LogF a -> IO a
stepLog (Log s r) = putStrLn s >> return r

I intend the LogAPI to be used as embellishments on the SimpleFileAPI, in other words I somehow have to turn an operation of SimpleFileAPI into an operation of LogAPI, i.e. I need a transformation. I called it logSimpleFileT and let it turn operations in SimpleFileF (i.e. not exactly SimpleFileAPI) into LogAPI (if you are wondering about my choice of type I hope it’ll become clear below, just trust me for now that this is a good choice):

logSimpleFileT :: SimpleFileF a -> LogAPI ()
logSimpleFileT (LoadFile fp _) = liftF $ Log ("** load file " ++ fp) ()
logSimpleFileT (SaveFile fp _ _) = liftF $ Log ("** save file " ++ fp) ()

So far everything is hopefully very straight forward and unsurprising. Now I need to combine the two APIs, I need to add them, in other words, I need a sum type:

data S a1 a2 t = A1 (a1 t) | A2 (a2 t)

type SumAPI = Free (S LogF SimpleFileF)

The next question is how to turn my two original APIs, SimpleFileAPI and LogAPI, into SumAPI. Luckily that’s already solved by the function hoistFree:

hoistFree :: Functor g => (forall a. f a -> g a) -> Free f b -> Free g b 

With this and logSimpleFileT from above I can use foldFree to decorate each operation with a logging operation like this:

logSimpleFile :: SimpleFileAPI a -> SumAPI a
logSimpleFile = foldFree f
  f op = hoistFree A1 (logSimpleFileT op) *> hoistFree A2 (liftF op)

This is where the type of logSimpleFileT hopefully makes sense!

Just as in the first section of this post, I need an interpreter for my API (SumAPI this time). Once again it’s written using foldFree, but this time I provide the interpreters for the sub-algegras (what I’ve chosen to call step functions):

runSum :: Monad m => (forall a. LogF a -> m a) -> (forall a. SimpleFileF a -> m a) -> SumAPI b -> m b
runSum f1 f2 = foldFree f
  f (A1 op) = f1 op
  f (A2 op) = f2 op

The file has a comment at the end for how to run it. The same example as in the previous section, but now with logging, looks like this

runSum stepLog stepSimpleFile $ logSimpleFile $ withSimpleFile (map toUpper) "foo"

The third - three algebras, one decorating the other two

To combine three algebras I simply take what’s in the previous section and extend it, i.e. a sum type with three constructors:

data S a1 a2 a3 t = A1 (a1 t) | A2 (a2 t) | A3 (a3 t)

type SumAPI = Free (S LogF SimpleFileF StdIoF)

runSum :: Monad m => (forall a. LogF a -> m a)
      -> (forall a. SimpleFileF a -> m a)
      -> (forall a. StdIoF a -> m a)
      -> SumAPI b -> m b
runSum f1 f2 f3 = foldFree f
  f (A1 op) = f1 op
  f (A2 op) = f2 op
  f (A3 op) = f3 op

With this I’ve already revealed that my three APIs are the two from previous sections, LogAPI (for decorating the other APIs), SimpleFileAPI and a new one, StdIoAPI.

I want to combine them in such a wat that I can write functions using both APIs at the same time. Then I modify withSimpleFile into

withSimpleFile :: (String -> String) -> FilePath ->  SumAPI ()
withSimpleFile f fp = do
  d <- loadFile fp
  let result = f d
  saveFile (fp ++ "_new") result

and I can add another function that uses it with StdIoAPI:

prog :: FilePath -> SumAPI ()
prog fn = do
  stdioPut "About to start"
  withSimpleFile (map toUpper) fn
  stdioPut "Done!"

The way to allow the APIs to be combined this way is to bake in S already in the convenience functions. This means the code for SimpleFileAPI has to change slightly (note the use of A2 in loadFile and saveFile):

data SimpleFileF a
= LoadFile FilePath (String -> a)
| SaveFile FilePath String a

loadFile :: FilePath -> SumAPI String
loadFile fp = liftF $ A2 $ LoadFile fp id

saveFile :: FilePath -> String -> SumAPI ()
saveFile fp d = liftF $ A2 $ SaveFile fp d ()

stepSimpleFile :: SimpleFileF a -> IO a
stepSimpleFile (LoadFile fp f') = f' <$> readFile fp
stepSimpleFile (SaveFile fp d r) = writeFile fp d >> return r

The new API, StdIoAPI, has only one operation:

data StdIoF a = PutStrLn String a

stdioPut :: String -> SumAPI ()
stdioPut s = liftF $ A3 $ PutStrLn s ()

stepStdIo :: StdIoF b -> IO b
stepStdIo (PutStrLn s a) = putStrLn s >> return a

The logging API, LogAPI, looks exactly the same but I now need two transformation functions, one for SimpleFileAPI and one for StdIoAPI.

data LogF a = Log String a

type LogAPI = Free LogF

stepLog :: LogF a -> IO a
stepLog (Log s r) = putStrLn s >> return r

logSimpleFileT :: SimpleFileF a -> LogAPI ()
logSimpleFileT (LoadFile fp _) = liftF $ Log ("** load file " ++ fp) ()
logSimpleFileT (SaveFile fp _ _) = liftF $ Log ("** save file " ++ fp) ()

logStdIoT :: StdIoF a -> LogAPI ()
logStdIoT (PutStrLn s _) = liftF $ Log ("** on stdio " ++ s) ()

The new version of logT needs to operate on S in order to decorate both APIs.

logT :: SumAPI a -> SumAPI a
logT = foldFree f
    f (A2 op) = hoistFree A1 (logSimpleFileT op) *> hoistFree A2 (liftF op)
    f (A3 op) = hoistFree A1 (logStdIoT op) *> hoistFree A3 (liftF op)
    f a@(A1 _) = liftF a

This file also has comments on how to run it at the end. This time there are two examples, one on how to run it without logging

runSum undefined stepSimpleFile stepStdIo $ prog "foo"

and one with logging

runSum stepLog stepSimpleFile stepStdIo (logT $ prog "foo")

June 18, 2016 12:00 AM

June 15, 2016

wren gayle romano

Off to NYC for July 4th and LICS

Over the last few weeks I was interviewed for the Identity Function. The process was quite nice and got me thinking on a number of things. Some of them I may well flesh out into blog posts once I get the time. Of course, that likely won't be until the autumn given everything else going on the next couple months.

I'll be in New York from 28 June through 10 July. The first couple days are for a PI meeting, then I'll get a four-day weekend before LICS, NLCS, and LOLA. Originally the plan was to take a quick trip to Sacramento that weekend for a friend's wedding. (The wedding's still on, but plans changed.) At least this way I'll get a chance to relax, rather than running all over the place. Of course this also means I'll be spending the 4th in NYC. Historically the 4th has been one of my favorite holidays, because it was one I've always spent with friends. I don't know that any of my readers are in NYC, but if you'll be around drop me a line. Or if you used to live there and know fun things to do that weekend, let me know! (Especially any quiet end-of-Pride things.)

Me and L set the date for our final move to the Bay Area: 20 July. And then I start at Google on the 25th. Between now and then: dissertating!!

comment count unavailable comments

June 15, 2016 07:32 AM

Christopher Allen

How to use UUID values with Persistent and Yesod

Some people find it trickier to store UUID values in their database with Persistent or to use UUID values in a Yesod web application than is really necessary. Here I’ll share some code from my work that demonstrates some patterns in applications that use Persistent or Yesod which should make it easier.

The context for this post can be found in these two links:

Replying to: Jezen Thomas writing about using UUIDs in Yesod
Prior art: Michael Xavier on UUID columns in Persistent

Alternate title: Same as the original, but with: “and no Control.Lens needed” tacked on.

This code is adapted from stuff we’ve written at work.

Persistent / UUID integration


Radioactive dumping ground for orphan instances. Adding the instances makes Persistent understand how to serialize and deserialize the UUID type. The orphans can be avoided if you use a newtype.

-- Note we're taking advantage of
-- PostgreSQL understanding UUID values,
-- thus "PersistDbSpecific"
instance PersistField UUID where
  toPersistValue u = PersistDbSpecific . B8.pack . UUID.toString $ u
  fromPersistValue (PersistDbSpecific t) =
    case UUID.fromString $ B8.unpack t of
      Just x -> Right x
      Nothing -> Left "Invalid UUID"
  fromPersistValue _ = Left "Not PersistDBSpecific"

instance PersistFieldSql UUID where
  sqlType _ = SqlOther "uuid"


This is where we actually use the UUID type in our models.

module MyCompany.DB.Models where

  [mkPersist sqlSettings,mkMigrate "migration"]
User json sql=users
  email                  Email       sqltype=text
  UniqUserEmail        email
  uuid                   UUID        sqltype=uuid   default=uuid_generate_v4()
  UniqUserUuid         uuid
  deriving Show Read Eq Typeable

We use the default JSON representation generated so that the format is predictable for the datatypes. I was a little queasy with this initially and it does mean we have to watch what happens to Aeson, but I believe net-net it reduces defects that reach production.

Yesod PathPiece integration

PathPiece is the typeclass Yesod uses to deserialize Text data into a more structured type, so that something like the following:

!/#Subdomain/#NumberedSlug    SomeRouteR  GET

could work. Here Subdomain and NumberedSlug are domain-specific types we made to represent a concept in our application in a type-safe manner. PathPiece often goes unnoticed by people new to Yesod, but it’s good to understand. For a super simple example:

newtype Subdomain = Subdomain Text
  deriving (Eq, Show, Read)

instance PathPiece Subdomain where
  toPathPiece (Subdomain t) = t
  fromPathPiece = Just . Subdomain

The PathPiece class itself isn’t terribly complicated or interesting:


-- S for "Strict"
class PathPiece s where
    fromPathPiece :: S.Text -> Maybe s
    toPathPiece :: s -> S.Text

To address the original post’s code, I wouldn’t have written that myself. I generally keep DB/IO stuff apart from things like forms. Partly this is because our web app repository is separate from our domain types / DB stuff repo, which sort of forces us to refactor things we might need to do more than once, or in a context that isn’t a web app. The use of applicative style and the double-lifting was not idiomatic.

Alternate title rejected for being too snarky: I told the doctor it hurts when I move my arm a certain way. The doctor told me to stop moving my arm like that.

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 book I've been writing with my coauthor Julie. There's a free sample available too!

June 15, 2016 12:00 AM

June 14, 2016

Douglas M. Auclair (geophf)

May 2016 1Liners

  • May 24th, 2016:
    Given f :: a -> [a] -> b, g :: a -> c
    Write h :: c -> [c] -> b, point-free, in terms of f and g
    where h x y = f (g x) (map g y)
  • May 16th, 2016: The next 3 #1Liner are of a piece, using
    data CmpV a =
       Vec { len :: Int, top :: a,  elts :: [a],
             cmp :: CmpV a -> CmpV a -> Ordering }
    • Give the point-free definition of:
      twoVs :: CmpV a -> CmpV b -> ([a], [b])
    • instance Ord (CmpV a) where
         compare v1 = uncurry (cmp v1) .  (v1,)

      Make compare point-free by removing v1 from above definition
    • An Ord-instance needs an Eq-instance:
      instance Eq a => Eq (CmpV a) where
         v1 == v2 = elts v1 == elts v2

      point-free-itize (==)
  • May 16th, 2016: You have the following lambda:
    \x y -> x == y || fn x y
    where fn :: a -> a -> Bool
    • obadz @obadzz without any fancy uses of the (a ->) Applicative :)
      curry $ foldr (||) False . flip map [(==), fn] . flip uncurry
    • obadz @obadzz with fancy use of (a ->) Applicative :)
      curry $ liftA2 (||) (uncurry (==)) (uncurry fn)
    • Noah Luck Easterly @walkstherain
      curry $ uncurry (||) . (uncurry (==) &&& uncurry fn)
  • May 5th, 2016:
    sames :: Eq a => [a] -> [a] -> Int
    Counts equal values at the same indices in two lists.
    What is the point-free definition?
    • joomy @cattheory
      sames = curry (length . filter (uncurry (==)) . uncurry zip)
    • bazzargh @bazzargh and then Fatih Karakurt @karakfa
      ((length . filter id) .) . zipWith (==)
    • me: sum <<- fromenum="" li="" nbsp="" zipwith="">
    • Noah Luck Easterly @walkstherain
      sames = ((sum . map fromEnum) .) . zipWith (==)
      • `getSum . foldMap (Sum . fromEnum)` seems better than `foldr (bool id succ) 0` but both satisfy `[Bool] -> Int`
    • Андреев Кирилл @nonaem00
      let it = (length .) . (filter id .)  . zipWith (==)

by geophf ( at June 14, 2016 08:46 PM

Roman Cheplyaka

Predicting a coin toss

I flip a coin and it comes up heads. What is the probability it will come up heads the next time I flip it?

“Fifty percent,” you say. “The coin tosses are independent events; the coin doesn’t have a memory.”

Now I flip a coin ten times, and ten times in a row it comes up heads. Same question: what is the probability it will come up heads the next time?

You pause for a second, if only because you are not used to getting heads ten times in a row.

But, after some hesitation, you convince yourself that this is no different from the first experiment. The coin still has got no memory, and the chances are still 50-50.

Or you become suspicious that something is not right with the coin. Maybe it is biased, or maybe it has two heads and no tails. In that case, your answer may be something like 95% for heads, where the remaining 5% account for the chance that the coin is only somewhat biased and tails are still possible.

This sounds paradoxical: coin tosses are independent, yet the past outcomes influence the probability of the future ones. We can explain this by switching from frequentist to Bayesian statistics. Bayesian statistics lets us model the coin bias (the probability of getting a single outcome of heads) itself as a random variable, which we shall call \(\theta\). It is random simply because we don’t know its true value, and not because it varies from one experiment to another. Consequently, we will update its probability distribution after every experiment because we gain more information, not because it affects the coin itself.

<figure> </figure>

Let \(X_i\in\{H,T\}\) be the outcome of \(i\)th toss. If we know \(\theta\), we automatically know the distribution of \(X_i\):


As before, the coin has no memory, so for any given \(\theta\), the tosses are independent: \(p(X_i \wedge X_j|\theta)=p(X_i|\theta)p(X_j|\theta)\). But they are independent only when conditioned on \(\theta\), and that resolves the paradox. If we don’t assume that we know \(\theta\), then \(X\)s are dependent, because the earlier observations affect what we know about \(\theta\), and \(\theta\) affects the probability of the future observations.

A model with conditionally independent variables is called a Bayesian network or probabilistic graphical model, and it can be represented by a directed graph as shown on the right. The arrows point from causes to effects, and the absence of an edge indicates conditional independence.

Based on our evidence of 10 heads in a row, the Bayes’ theorem lets us estimate the distribution of \(\theta\). All we need is a prior distribution – what did we think about the coin before we tossed it?

For coin tossing and other binary problems, it is customary to take the Beta distribution as the prior distribution, as it makes the calculations very easy. Often such choice is justified, but in our case it would be a terrible one. Almost all coins we encounter in our lives are fair. To make the beta distribution centered at \(\theta=0.5\) and low variance, we would need to set its parameters, \(\alpha\) and \(\beta\), to large equal numbers. The resulting distribution would assign non-trivial probability only to low deviations from \(\theta=0.5\), and the distribution would be barely affected by our striking evidence.

<figure> </figure>

Instead, let’s engineer our prior distribution from scratch. Double-sided coins may be rare in everyday life, but they are easy to buy on eBay. When someone approaches us out of the blue and starts flipping coins, there’s a fair chance they’ve got one of those. Still, we believe in humanity, so let’s assign a point probability of just \(1\%\) to \(\theta=0\) and \(\theta=1\). What about biased coins, such as coins with \(\theta=0.83\)? Turns out they are unlikely to exist. Nevertheless, the Bayesian statistics teaches to be reluctant to assign zero probabilities to events, since then no amount of evidence can prove us wrong. So let’s take \(0.1\%\) and spread it uniformly across the interval \([0;1]\). The remaining \(97.9\%\) will be the probability of a fair coin.

Formally, our prior distribution over \(\theta\) can be specified by its probability density as

\[ p(\theta)=0.979\delta(\theta-0.5)+0.01\delta(\theta)+0.01\delta(\theta-1)+0.001, \]

where \(\delta\) is the Dirac delta function used to specify point probabilities.

Let \(D\) refer to the event that \(X_i=H\), \(i=1,2,\ldots,10\). Then \(p(D|\theta)=\theta^{10}\). By Bayes’ theorem,

\[ p(\theta|D)=\frac{p(D|\theta)p(\theta)}{\int_0^1 p(D|\theta)p(\theta)d\theta} = \frac{\theta^{10}p(\theta)}{\int_0^1 \theta^{10}p(\theta)d\theta}. \]

Now we need to do a bit of calculation by hand:

\[ \begin{multline} \int_0^1 \theta^{10}p(\theta)d\theta=0.979\cdot0.5^{10}+0.01\cdot 1^{10}+0.01 \cdot 0^{10} + 0.001\int_0^1 \theta^{10}d\theta \\ = 9.56\cdot 10^{-4} + 0.01 + 9.09\cdot 10^{-5}=0.0110; \end{multline} \] \[ p(\theta|D)=0.087\delta(\theta-0.5)+0.905\delta(\theta-1)+0.091\theta^{10}. \]

Thus, we are \(90.5\%\) sure that the coin is double-headed, but we also allow \(8.7\%\) for pure coincidence and \(0.8\%\) for a biased coin.

<figure> </figure> <figure> </figure>

Now back to our question: how likely is it that the next toss will produce heads?

\[ \begin{multline} p(X_{11}=H|D) = \int_0^1 p(X_{11}=H|D,\theta)p(\theta|D)d\theta = \int_0^1 \theta \, p(\theta|D)d\theta \\ = 0.087\cdot 0.5+0.905\cdot 1+0.091\cdot \int_0^1\theta^{11}d\theta = 0.956. \end{multline} \]

Very likely indeed. Notice, by the way, how we used the conditional independence above to replace \(p(X_{11}=H|D,\theta)\) with \(p(X_{11}=H|\theta)=\theta\).

Bayesian statistics is a powerful tool, but the prior matters. Before you reach for the conjugate prior, consider whether it actually represents your beliefs.

A couple of exercises:

  1. How does our prior distribution change after a single coin toss (either heads or tails)?
  2. How does our prior distribution change after ten heads and one tails?

June 14, 2016 08:00 PM

June 11, 2016

Neil Mitchell

js-jquery 3.0.0 now out

The js-jquery Haskell library bundles the minified jQuery Javascript code into a Haskell package, so it can be depended upon by Cabal packages and incorporated into generated HTML pages. It does so in a way that doesn't require each Haskell package to bundle its own extra data files, and in a way that meets the licensing requirements of distributions such as Debian.

I've just released version 3.0.0, following on from jQuery 3.0.0 a few days ago. This release breaks compatibility with IE6-8, so if that's important to you, insert an upper bound on the package.

by Neil Mitchell ( at June 11, 2016 03:08 PM

June 08, 2016

Jan Stolarek

Coq’Art, CPDT and SF: a review of books on Coq proof assistant

I have been pretty quiet on the blog in the past couple of months. One of the reasons for this is that I have spent most of my time learning Coq. I had my first contact with Coq well over a year ago when I started reading CPDT. Back then I only wanted to learn the basics of Coq to see how it works and what it has to offer compared to other languages with dependent types. This time I wanted to apply Coq to some ideas I had at work, so I was determined to be much more thorough in my learning. Coq is far from being a mainstream language but nevertheless it has some really good learning resources. Today I would like to present a brief overview of what I believe are the three most important books on Coq: “Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions” (which I will briefly refer to as Coq’Art) by Yves Bertot and Pierre Castéran, “Certified Programming with Dependent Types” (CPDT) by Adam Chlipala and “Software Foundations” (SF for short) by Benjamin Pierce and over a dozen over contributors. All three books significantly differ in their scope and focus. CPDT and Coq’Art are standard, printed books. CPDT is also available online for free. Software Foundations is only available as an online book. Interestingly, there is also a version of SF that seems to be in the process of being revised.

I believe Coq’Art was the first book published on Coq. There are two editions – 2004 hardcover version and a 2010 paperback version – but as far as I know there are no differences between them. Too bad the 2010 edition was not updated for the newest versions of Coq – some of the code examples don’t work in the newest compiler. Coq’Art takes a theoretical approach, ie. it teaches Coq largely by explaining how the rules of Calculus of Constructions work. There are also practical elements like case studies and exercises but they do not dominate the book. Personally I found Coq’Art to be a very hard read. Not because it dives too much in theory – it doesn’t – but because the presentation seems to be chaotic. For example, description of a single tactic can be spread throughout deveral places in the book. In principle, I don’t object to extending earlier presentation with new details once the reader gets a hold of some new concepts, but I feel that Coq’Art definitely goes too far. Coq’Art also presents material in a very unusual order. Almost every introduction to Coq or any other functional language begins with defining data types. Coq’Art introduces them in chapter 6. On the other hand sorts and universes – something I would consider an advanced concept for anyone who is not familiar with type-level programming – are presented in the second chapter. (Note that first chapter is a very brief overview of the language.) By contrast, CPDT goes into detailed discussion of universes in chapter 12 and SF does not seem to cover them at all. Overall, Coq’Art is of limited usefulness to me. To tell the truth this is not because of its focus on theory rather than practice, but because of language style, which I find rather inaccessible. Many times I had problems understanding passages I was reading, forcing me to re-read them again and again, trying to figure out what is the message that the authors are trying to convey. I did not have such problems with CPDT, SF, nor any other book I have read in the past few years. At the moment I have given up on the idea of reading the book from cover to cover. Nevertheless I find Coq’Art a good supplementary reading for SF. Most importantly because of the sections that explain in detail the inner workings of various tactics.

As mentioned at the beginning, I already wrote a first impressions post about CPDT. Back then I said the book “is a great demonstration of what can be done in Coq but not a good explanation of how it can be done”. Having read all of it I sustain my claim. CPDT does not provide a thorough and systematic coverage of basics, but instead focuses on advanced topics. As such, it is not the best place to start for beginners but it is a priceless resource for Coq practitioners. The main focus of the book is proof automation with Ltac, Coq’s language for writing automated proof procedures. Reader is exposed to Ltac early on in the book, but detailed treatment of Ltac is delayed until chapter 14. Quite surprisingly, given that it is hard to understand earlier chapters without knowing Ltac. Luckily, the chapters are fairly independent of each other and can be read in any order the reader wishes. Definitely it is worth to dive into chapter 14 and fragments of apter 13 as early as possible – it makes understanding the book a whole lot easier. So far I have already read chapter 14 three times. As I learn Coq more and more I discover new bits of knowledge with each read. In fact, I expect to be going back regularly to CPDT.

Coq’Art and CPDT approach teaching Coq in totally different ways. It might then be surprising that Software Foundations uses yet another approach. Unlike Coq’Art it is focused on practice and unlike CPDT it places a very strong emphasis on learning the basics. I feel that SF makes Coq learning curve as flat as possible. The main focus of SF is applying Coq to formalizing programming languages semantics, especially their type systems. This should not come as a big surprise given that Benjamin Pierce, the author of SF, authored also “Types and Programming Languages” (TAPL), the best book on the topic of type systems and programming language semantics I have seen. It should not also be surprising that a huge chunk of material overlaps between TAPL and SF. I find this to be amongst the best things about SF. All the proofs that I read in TAPL make a lot more sense to me when I can convert them to a piece of code. This gives me a much deeper insight into the meaning of lemmas and theorems. Also, when I get stuck on an exercise I can take a look at TAPL to see what is the general idea behind the proof I am implementing.

SF is packed with material and thus it is a very long read. Three months after beginning the book and spending with it about two days a week I am halfway through. The main strength of SF is a plethora of exercises. (Coq’Art has some exercises, but not too many. CPDT has none). They can take a lot of time – and I really mean a lot – but I think this is the only way to learn a programming language. Besides, the exercises are very rewarding. One downside of the exercises is that the book provides no solutions, which is bad for self-studying. Moreover, the authors ask people not to publish the solutions on the internet, since “having solutions easily available makes [SF] much less useful for courses, which typically have graded homework assignments”. That being said, there are plenty of github repositories that contain the solved exercises (I also pledge guilty!). Although it goes against the authors’ will I consider it a really good thing for self-study: many times I have been stuck on exercises and was able to make progress only by peeking at someone else’s solution. This doesn’t mean I copied the solutions. I just used them to overcome difficulties and in some cases ended up with proofs more elegant than the ones I have found. As a side note I’ll add that I do not share the belief that publishing solutions on the web makes SF less useful for courses. Students who want to cheat will get the solutions from other students anyway. At least that has been my experience as an academic teacher.

To sum up, each of the books presents a different approach. Coq’Art focuses on learning Coq by understanding its theoretical foundations. SF focuses on learning Coq through practice. CPDT focuses on advanced techniques for proof automation. Personally, I feel I’ve learned the most from SF, with CPDT closely on the second place. YMMV

by Jan Stolarek at June 08, 2016 05:30 PM