ezyang’s blog

the arc of software bends towards understanding

May, 2014

Parsec: “try a <|> b” considered harmful

tl;dr The scope of backtracking try should be minimized, usually by placing it inside the definition of a parser. Have you ever written a Parsec parser and gotten a really uninformative error message? "test.txt" (line 15, column 7): unexpected 'A' expecting end of input The line and the column are randomly somewhere in your document, […]

  • May 17, 2014

GHC and mutable arrays: a DIRTY little secret

Brandon Simmon recently made a post to the glasgow-haskell-users mailing list asking the following question: I've been looking into an issue in a library in which as more mutable arrays are allocated, GC dominates (I think I verified this?) and all code gets slower in proportion to the number of mutable arrays that are hanging […]

  • May 9, 2014

Elimination with a Motive (in Coq)

Elimination rules play an important role in computations over datatypes in proof assistants like Coq. In his paper "Elimination with a Motive", Conor McBride argued that "we should exploit a hypothesis not in terms of its immediate consequences, but in terms of the leverage it exerts on an arbitrary goal: we should give elimination a […]

  • May 7, 2014

The cost of weak pointers and finalizers in GHC

Weak pointers and finalizers are a very convenient feature for many types of programs. Weak pointers are useful for implementing memotables and solving certain classes of memory leaks, while finalizers are useful for fitting "allocate/deallocate" memory models into a garbage-collected language. Of course, these features don’t come for free, and so one might wonder what […]

  • May 4, 2014