Computing connected components in an undirected graph is one of the most basic graph problems. Given a graph with n vertices and m edges, you can find its components in linear time O(n + m) using depth-first or breadth-first search. But what if you need to go faster? In this blog post, I will describe a cool new concurrent algorithm for this problem, which I learned this week at the Heidelberg Laureate Forum from Robert Tarjan himself. The algorithm distributes the work among n + m tiny processors that work concurrently most of the time and requires O(log n) global synchronisation rounds. The algorithm is remarkably simple but it’s far from obvious that it works correctly and efficiently. Happily, Tarjan and his co-author S. Cliff Liu have done all the hard proofs in their recent paper, so we can simply take the algorithm and use it.
Category Archives: coding
Stroll: an experimental build system
I’d like to share an experiment in developing a language-agnostic build system that does not require the user to specify dependencies between individual build tasks. By “language-agnostic” I mean the user does not need to learn a new language or a special file format for describing build tasks — existing scripts or executable files can be used as build tasks directly without modification.
I call this build system Stroll because its build algorithm reminds me of strolling through a park where you’ve never been before, trying to figure out an optimal path to your target destination, and likely going in circles occasionally until you’ve built up a complete mental map of the park.
You should try Hadrian
This is an announcement for GHC developers:
You should try to use Hadrian as the GHC build system, because it will (hopefully!) become the default around GHC 8.8.
United Monoids
In this blog post we will explore the consequences of postulating 0 = 1 in an algebraic structure with two binary operations (S, +, 0) and (S, ⋅, 1). Such united monoids have a few interesting properties, which are not immediately obvious. For example, we will see that the axiom 0 = 1 is equivalent to a seemingly less extravagant axiom ab = ab + a, which will send us tumbling down the rabbit hole of algebraic graphs and topology.
Selective applicative functors
Update: I have written a paper about selective applicative functors, and it completely supersedes this blog post (it also uses a slightly different notation). You should read the paper instead.
I often need a Haskell abstraction that supports conditions (like Monad) yet can still be statically analysed (like Applicative). In such cases people typically point to the Arrow class, more specifically ArrowChoice, but when I look it up, I find several type classes and a dozen of methods. Impressive, categorical but also quite heavy. Is there a more lightweight approach? In this blog post I’ll explore what I call selective applicative functors, which extend the Applicative type class with a single method that makes it possible to be selective about effects.
Please meet Selective:
class Applicative f => Selective f where handle :: f (Either a b) -> f (a -> b) -> f b
Think of handle as a selective function application: you apply a handler function of type a → b when given a value of type Left a, but can skip the handler (along with its effects) in the case of Right b. Intuitively, handle allows you to efficiently handle errors, i.e. perform the error-handling effects only when needed.
The Task abstraction
Neil Mitchell, Simon Peyton Jones and I have just finished a paper describing a systematic and executable framework for developing and comparing build systems. The paper and associated code are available here: https://github.com/snowleopard/build. The code is not yet well documented and polished, but I’ll bring it in a good shape in April. You can learn more about the motivation behind the project here.
(Update: the paper got accepted to ICFP! Read the PDF, watch the talk.)
In this blog post I would like to share one interesting abstraction that we came up with to describe build tasks:
type Task c k v = forall f. c f => (k -> f v) -> k -> Maybe (f v)
A Task is completely isolated from the world of compilers, file systems, dependency graphs, caches, and all other complexities of real build systems. It just computes the value of a key k, in a side-effect-free way, using a callback of type k → f v to find the values of its dependencies. One simple example of a callback is Haskell’s readFile function: as one can see from its type FilePath → IO String, given a key (a file path k = FilePath) it can find its value (the file contents of type v = String) by performing arbitrary IO effects (hence, f = IO). We require task descriptions to be polymorhic in f, so that we can reuse them in different computational contexts f without rewriting from scratch.
Formal verification of spacecraft control programs
Last February I spent two weeks in Vienna, visiting Jakob Lechner and RUAG Space Austria, a company developing components for space missions. Jakob and his colleagues designed a specialised processing core called REDFIN (REDuced instruction set for Fixed-point & INteger arithmetic) for executing simple spacecraft control tasks, such as satellite antenna pointing. During the visit I implemented a prototype of a formal verification framework to support the development of REDFIN programs. Afterwards I was quite busy with my other projects, but my PhD student Georgy Lukyanov helped to further improve the prototype.
Jakob, Georgy and I have just submitted a conference paper describing the REDFIN core and the verification framework. Please have a look and let us know what you think. This will be a timely read after yesterday’s exciting SpaceX launch.
Continue reading Formal verification of spacecraft control programs
Hadrian is on the way
Hadrian, a new build system for GHC that we have been working on for the past three years, has finally been merged into the GHC tree (update: we have temporally switched to a submodule). However it’s not yet time to celebrate — there are still many issues that need to be addressed before the Make-based build system may retire.
Want to try? Checkout the GHC repository and run hadrian/build.sh -j or hadrian/build.bat -j on Windows and it should build you a GHC binary. In case of problems, have a look at the README and/or raise an issue.
Here is a quick update on the on-going development:
- Hadrian can build GHC and can already be used as part of the CI infrastructure. However, the resulting binary does not pass the validation. Zhen Zhang is looking into this, but more help is needed.
- A major refactoring by Moritz Angermann is on the way. Moritz is primarily interested in cross compilation, but to make it work he had to get rid of the
ghc-cabalutility, reorganise the build tree, and make numerous other improvements to Hadrian. - There is currently no support for binary distribution. Ben Gamari is looking into this issue.
- Dynamic linking on Windows is not implemented. Tamar Christina has kindly offered help with this.
- Hadrian source code is still not fully documented and tested, and generally requires some polishing. I am currently taking care of this when not distracted by urgent bug fixes and will appreciate your help in making Hadrian easier to understand and use.
I can’t believe that we seem to approach the finish line! It’s been a long, tedious but also interesting project. Thank you all for helping us get this far, and I hope we’ll celebrate the switch from Make to Hadrian soon.
Old graphs from new types
After I got back from the holiday that I planned in the previous blog post, I spent the whole January playing with the algebra of graphs and trying to find interesting and useful ways of constructing graphs, focusing on writing polymorphic code that can manipulate graph expressions without turning them into concrete data structures. I’ve put together a small toolbox containing a few quirky types, which I’d like to share with you in this blog post. If you are not familiar with the algebra of graphs, please read the introductory blog post first.
Update: This series of blog posts was published as a functional pearl at the Haskell Symposium 2017.
Graphs in disguise: from todo lists to build systems
In this blog post we will look at an example of using the algebra of graphs for manipulating sequences of items, which at first sight might not look like graphs, but are actually dependency graphs in disguise. We will develop a tiny DSL for composing todo lists on top of the alga library and will show how it can be used for planning a holiday and, on a more serious note, for writing software build systems. This blog post will partially answer the question about possible applications of the algebra of graphs that was asked in this reddit discussion.
Update: This series of blog posts was published as a functional pearl at the Haskell Symposium 2017.
Continue reading Graphs in disguise: from todo lists to build systems