Generating random planar graphs

I am a great fan of the QuickCheck testing library for Haskell and have been using it for some time now. If you don't know about it stop reading this immediately and go read the original ICFP paper. Alternatively (for the impatient) browse the article on Wikipedia which also refers to some re-implementations in other languages.

QuickCheck can be seen as two domain-specific languages embedded in Haskell: one for generating test data and another writing properties of Haskell programs (and also collecting coverage statistics). But you can also use QuickCheck to generate complex input data for programs in any language.

The example I am reporting came up when setting up a problem for TIUP, a locally organized ACM-style programming contest for undergraduate students. The competitors must solve a number of coding problems in C/C++, Java or PASCAL. The solutions are tested automatically by running the programs against a number of hidden test inputs to assess output correctness (and perhaps efficiency by imposing time and space limits).

For my particular problem, the inputs are planar graphs representing a city road map. I used Haskell and QuickCheck to generate random planar graphs of increasing size. The idea is simple (and probably not original): start with a regular mesh and randomly delete some edges; some care is needed to avoid disconnecting the graph and avoid leaving nodes with a single outward edge (for esthetical reasons).

Here are some examples of generated graphs with 25 nodes and an increasing number of edges removed.

Full mesh

20% random edges removed

50% edges removed

You can download the source file here: Graph.hs. This Haskell script generates some random graphs and invokes graphviz to render them. It is very short (around 120 lines) and, I my opinion, quite readable; it should also be easy to modify. The functional programming "idioms" like parametric polymorphism, higher-order functions, list comprehensions and point-free style really shine on this kind of problem.

Regular expression matching in Haskell

This is a short Haskell program that implements regular expression matching ( you can download the source file here: RE.hs). Two neat things about this implementation:

1.  matching is defined by recursion over the structure of the regexp (i.e. there is no need to convert the regexp to an automata); and
2. it uses the "overloaded strings" extension to allow treating string literals as regexps.

Matching is implemented using continuations that specify what to do with the suffix left-over after matching the string; this leads to a very elegant and self-documented solution.
There is, however, one drawback: the handling of star-closure is inefficient due to the test cs'/=cs to check that a prefix of the string was consumed. The changes needed to implement a more efficient version are left as an exercise for the reader.

{- ------------------------------------------------------------------ 
   Regular expression matching in Haskell 
 
   This is a classical example of functional programming with 
   continuations. Adapted from the SML version by Olivier Danvy 
   (from "Defunctionalization at Work", BRICS RS-01-23, 2001).
   This version uses the "overloaded strings" GHC extension for
   mixing character literals in regexps.  

   Some examples to try on the GHCi interpreter;
   (Note: use the command ":set -XOverloadedStrings"
   to enable overloaded strings for the GHCi session.)

   > :set -XOverloadedStrings
   > match (star "ab") ""
   = True
   > match (star "ab") "aba"
   = False
   > match (star "ab") "abab"
   = True
   > match (star "a" <+> star "b") "aaaa"
   = True
   > match (star "a" <+> star "b") "aabb"
   = False
   > match (star ("a" <+> "b")) "aabb"
   = True

   Pedro Vasconcelos, 2012
  -------------------------------------------------------------------
-}

-- enable the overloaded strings language extension in GHC
{-# LANGUAGE OverloadedStrings #-}
module RE where
-- import the interface for overloading strings
import GHC.Exts ( IsString(..) )

-- Abstract syntax of regular expressions;
-- literal characters, empty word, empty language
-- concatenation, union and Kleene star closure
data Regexp = Lit Char
            | Epsilon
            | Empty
            | Concat Regexp Regexp
            | Union Regexp Regexp
            | Star Regexp
            deriving (Show, Read, Eq)
                            
-- "Smart" constructors that perform some simplifications
-- Infix binary operators for concation and union
infixl 7 <>
infixl 6 <+>

(<>) :: Regexp -> Regexp -> Regexp
Empty <> _ = Empty
_ <> Empty = Empty
Epsilon <> r = r
r <> Epsilon = r
r <> r'      = Concat r r'

(<+>) :: Regexp -> Regexp -> Regexp
Empty <+> r = r
r <+> Empty = r
r <+> r'    = Union r r'

-- Kleene star closure
star :: Regexp -> Regexp 
star Empty     = Epsilon
star Epsilon   = Epsilon
star (Star r) = Star r
star r        = Star r

-- coercion of strings to regular expressions
-- e.g. fromString "abc" = Lit 'a' <> Lit 'b' <> Lit 'c' <> Epsilon
instance IsString Regexp where
  fromString cs = foldr ((<>) . Lit) Epsilon cs


-- Higher-order, continuation-based matcher for regular expressions
-- worker function to match a regexp with string
-- 3rd argument is the continuation for the non-matched suffix
accept :: Regexp -> String -> (String -> Bool) -> Bool
accept Empty cs k   = False
accept Epsilon cs k = k cs
accept (Lit c) (c':cs) k = c==c' && k cs
accept (Lit c) []  k   = False
accept (Concat r1 r2) cs k = accept r1 cs (\cs' -> accept r2 cs' k)
accept (Union r1 r2) cs k = accept r1 cs k || accept r2 cs k
accept (Star r) cs k = accept_star r cs k
  
accept_star r cs k 
  = k cs || accept r cs (\cs' -> cs'/=cs && accept_star r cs' k)

-- top-level matcher; initial continuation tests for the empty string
match :: Regexp -> String -> Bool
match r cs = accept r cs null

-- end of file --

The rise of functional programming

I have returned from Copenhagen were last week I attended ICFP 2012, the principal scientific conference on functional programming and related topics. This year's conference was very busy with a record number of participants and very high quality presentations (which, by the way, you can watch on YouTube by courtesy of Malcom Wallace).

I was quite surprised by high number of people from industry, both small and large: Google, Jane Street, Standard Chartered, Galois, Well-Typed, Basho, among others. It seems that functional programming is a hot topic for real software developers - not just academics.

The discussion at the end of the Haskell Symposium on Thursday was also a turning point for the language and for FP in general. Aaron Contorer addressed the participants to put forward his view for his new company called FPComplete: get a lot more users in the software industry to adopt Haskell by providing the tools and support that the open-source community can't provide. FPComplete aims to fill this gap in much the same way as RedHat did for Linux in the enterprise. By the way, Aaron is not an FP geek - he headed the developer productivity tools at Microsoft, for example. That someone comming from the software business says that it's now time for FP is a great endorsement for the Haskell language and community.

This is great news for Haskell and wish FPComplete great success!

Predicting the costs of lazy evaluation

For quite some time there have been very compelling arguments for non-strict functional programming in the style made popular by Haskell; here are some more recent ones.  In a nutshell: non-strict semantics is a very powerful "glue" to aid the modular decomposition of programs. And, as software gets more complex, modularity matters most. (Types are arguably even more important, but they are orthogonal to the strict versus non-strict debate).

The most serious critique of non-strict semantics is that the time and space behavior of its implementation (lazy evaluation) are difficult to reason about. In other words: non-strict functional programming allows reasoning about denotational properties but hinders reasoning about operational ones. And how something is computed is often as important as what is computed: for example, all sorting algorithms (when seen as pure functions) have the same denotation, yet their differences are extremely relevant.

However, I don't think the situation is hopeless; two things are required to improve this state of affairs: 1) a language-level operational model of lazy evaluation; and 2) a compositional method for assigning costs derived from the execution model to language fragments.

There has been a good solution for the first part for some time now, namely, Launchbury's natural semantics for lazy evaluation. The key idea is to consider an abstract model of heap as a mapping from variables to expressions (thunks); the evaluation of let x=e1 in e2 extends the heap with a mapping from x to e1 and proceeds to evaluate e2. To model call-by-need (i.e. graph reduction with update in-place) rather than call-by-name we also need to update a thunk with its result when evaluating a variable. (I'm glossing over many technical points for simplicity; go and read the paper for the details).

I have been working with Kevin Hammond, Steffen Jost, Mário Florido and Hugo Simões on a new approach for the second problem based on amortised static analysis. The use of amortisation with lazy evaluation goes back to Okasaki's "Purely functional data-structures"; unlike the later, our approach is type-based and fully automatic. Simplifying slightly many technical details to focus on the intuitions, the key ideas are:

1. for concreteness, we consider the number of allocations in a semantics similar to Launchbury's as our measure of cost;
2. we annotate thunk costs in types, e.g. in a context x:T^q(A) the variable x is a thunk which costs q to evaluate to whnf and whose value has type A;  
3. we also annotate the overall evaluation cost in type judgments, e.g. Gamma |-p- e:B means that evaluation of e to whnf costs p (and admits type B);
4. the type rule for variables requires paying the full cost annotated in the type (i.e. as if evaluation was call-by-name);
5.  we recover the cost of call-by-need by a structural type rule that allows prepaying part or all of the cost of thunks (amortisation allows decoupling the accounting of the cost from the dynamic moment when evaluation actually occurs).

We have written a paper describing the analysis that will be presented at ICFP 2012 conference next week; the full soundness proof is available in a draft extended version of the paper. Moreover, the analysis is fully automatic (it generates a linear program that can be feed to an LP solver to determine the type annotations) and we have built a prototype implementation which we have used to accurately determine the costs of simple examples (but you most likely need to read the paper to understand the output). 

Of course, the general computability limitations apply, so this analysis cannot predict costs of arbitrary programs. In particular, it is limited to costs that are constant or linear functions of the number of data constructors.

A little strictness goes a long way

In a previous post, I argued that Haskell isn't always lazy because you can control strictness of data types and functions. Today I will show a little example that shows how strictness can be used to avoid problems associated with too much laziness. The good part is that you often only need a little strictness.

When implementing an two-player board game, I had to represent the board pieces and moves. For presentation purposes, let us consider Chess moves; a first aproach is to represent a move as a pair of algebraic coordinates, which in turn are pairs of column and row:

type Move = (Coord, Coord)  -- from, to
type Coord = (Char, Int)    -- column, row

For example, the king pawn opening move is represented by (('e',2),('e',4)).

The problem with this is that pairs are non-strict, and therefore the Move type is inhabited by partially defined moves, e.g.:

(bottom, bottom)  :: Move
(('e',2), bottom) :: Move
(bottom, ('e',4)) :: Move
(('e',2), ('e',bottom) :: Move

(where bottom is some expression that either fails to terminate or throws an exception).

We can rule out all these partially defined moves simply by declaring data types with strict components:

data Move = MkMove !Coord !Coord   -- from, to
data Coord = MkCoord !Char !Int    -- column, row

The advantage of the second representation is that if any of the arguments of MkMove or MkCoord is bottom then the result is also bottom, e.g.:

MkMove bottom bottom  = bottom
MkMove (MkCoord bottom 2) (MkCoord 'e' 4) = bottom 

Why is this important in practice? I can think of at least three advantages:

1. if your code is buggy and, say, throws an exception when computing move coordinates you will get the error message when the move is constructed rather than when it is used; if your program is going to fail, then it should fail fast;
2. when writing concurrent or parallel code this ensures that moves are fully evaluated at the right moment, i.e. in the right thread (I stumbled upon this bug when writing a multi-threaded GUI in Haskell);
3. finally, when compiling with optimization on, GHC will unbox strict data fields which reduces the number of allocations and increases locally; for very inner loops this can be a big performance win.

First experiences with the Raspberry Pi

Finally, my Raspberry Pi arrived last week. I had placed my order around April so this was a long wait. But it was worth it!

In case you haven't heard about it, the Raspberry Pi is a $35 bare-board computer intended for school children to learn the basics of computers and programming. It is promoted by a non-profit organization (the Raspberry Pi Foundation) and fills the void left by the demise of the small personal computers of the 80s (such as the ZX Spectrum, the BBC Micro or the C64) on which many of today's scientists and engineers (including myself) first learnt to program.

Of course time has moved on, and the Pi can now be made so cheaply by using high integration components from the mobile phone industry: a system-on-a-chip comprising a GPU, CPU and 256MB of RAM; an SD card slot for persistent storage, an ethernet port, HDMI/composite for display and USB for input devices (or more storage).

The principle difference between the Pi and a smartphone (regardless of price) is that, unlike the later, the Pi is a general purpose programmable computer running a generic GNU/Linux OS. Yes, you can buy or download an SDK for an IPhone/Android but that is a much higher entry barrier. And the higher cost and utility of a smartphone/PC discourages anyone from tinkering with it.

Because it runs an open-source OS, the Pi is remarkably agnostic regarding programming languages and environments. In a couple a days I have successfully tried C, Python, Haskell, O'Caml and Prolog.

I teach programming to first-year CS students and intend to use my Pi to show how abstraction allows running the same high-level program developed in class on both the lab's x86 PCs and the ARM-based Pi: different CPUs, different memory size and storage devices, different flavors of Linux; but by focusing on a proper level of abstraction we can re-use the same source code on vastly different devices. We already tell them such things, but the Pi makes it easy to actually show them. And, as I get older, I realize that the persuasive power hands-on experiment is often underestimated in formal education.

Why Haskell is not a lazy language

There is a recurrent misconception that Haskell is a lazy functional language. As some people have pointed out, this is not an acurate description: Haskell is a non-strict functional language. Lazy evaluation (i.e. call-by-need or graph reduction) is an (operational) implementation technique; non-strictness is a (denotational) semantic property.

The Haskell standard (almost)  never specifies evaluation order; it says what the values (denotations) of expressions should be (in particular, whether they should be terminating or non-terminating - designated "bottom" in denotational semantics). Implementations are free to choose any evaluation strategy that preserves the semantics. With call-by-name being too inefficient for general use, a "safe" approach would to use lazy evaluation everywhere. However, an implementation can use eager evaluation whenever this does not change the termination properties of the program. This is can be automatically detected by strictness analysis and is routinely done by the GHC compiler to optimize numerical code (for example).

Moreveover, Haskell is non-strict by default only:  the programmer can also express strictness information through annotations. Consider the definition of the natural numbers in Peano-style; a first attempt would be as follows.

 data Nat = Zero | Suc Nat deriving Show

Data constructors are non-strict by default, so this type includes an "infinite" natural number; let's try it out in the Haskell interpreter:

> let inf = Suc inf in inf
Suc (Suc (Suc (....^C Interrupted

Such cyclic values can lead to undesirable consequences. For example, they break some familiar algebraic laws: from A+x=B+x we can no longer infer that A=B. For a counterexample, let's first define addition using primitive recursion:

 (+) :: Nat -> Nat -> Nat
 Zero + y = y
 Suc x + y = Suc (x+y)

Now we can show that Suc Zero + inf = Zero + inf:

  Suc Zero + inf 
= {1st equation of +}
  Suc (Zero + inf) 
= {2nd equation of +}
  Suc inf 
= {definition of inf}
  inf
= {1st equation of +}
  Zero + inf

Thus from the above law we could prove Suc Zero = Zero which is not a good thing.
We can prevent such pathological values by adding a strictness annotation to the data type declaration; let's define proper Peano naturals:

> data PNat = PZero | PSuc !Nat deriving Show

The exclamation mark (pronounced "bang") declares that PSuc is strict in its argument, i.e. PSuc bottom = bottom (where bottom is a non-terminating expression). (By the way, such strictness annotations are part of the Haskell standard, not a GHC extension).

What happens if we attempt to definite the infinite number? Well, we simply get a non-terminating computation (bottom). In other words: inf becomes indistinguishable from a completely circular definition:

> let inf = PSuc inf in inf
^C Interrupted

> let bottom = bottom in bottom
^C Interrupted

Now what if we want to specify the strictness of functions? Strictness annotations don't work for this because we are not defining a new data type; we can instead use bang patterns (which is not part of the Haskell standard but is an extension supported by GHC and other implementations). For example, let's define the strict and non-strict constant functions (i.e. that yield the first argument and ignore the second).

{-# LANGUAGE BangPatterns #-}
strict_const :: a -> b -> a
strict_const k !x = k
const :: a -> b -> a
const k x = k

Testing these in the interpreter works as expected:

> let bottom=bottom in const 42 bottom
42
> let bottom=bottom in strict_const 42 bottom
^C Interrupted

The moral of the story is that the Haskell programmer is not forced to be lazy or non-strict. We have at our disposal means for expressing our intent. We them often and use them wisely!

Getting started!

In this blog I'll wrote about things that surprise and amuse me in computer science, programming languages theory and practice, mathematics, science and technology.

About the title

In programming languages theory, the "Y combinator" (also called the "fixed point combinator") is a higher-order function that allows encoding recursion without self-reference (i.e. without defining a name in terms of itself); this is useful in giving meaning to recursive definitions in a way that is mathematically precise. You can read more about it in the Wikipedia article.