ezyang's blog

the arc of software bends towards understanding

2014/05

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, and you’re pretty sure you should be in the middle of some stack of parser combinators. But wait! Parsec has somehow concluded that the document should be ending immediately. You noodle around and furthermore discover that the true error is some ways after the actually reported line and column.

Read more...

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

…to which I replied:

In the current GC design, mutable arrays of pointers are always placed on the mutable list. The mutable list of generations which are not being collected are always traversed; thus, the number of pointer arrays corresponds to a linear overhead for minor GCs.

Read more...

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 motive.” In other words, proofs in a refinement setting (backwards reasoning) should use their goals to guide elimination.

Read more...

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 the cost of utilizing these two (closely related) features are in GHC. In this blog post, I want to explain how weak pointers and finalizers are implemented in the GHC runtime system and characterize what extra overheads you incur by using them. These post assumes some basic knowledge about how the runtime system and copying garbage collection work.

Read more...