Computer science, maths, and occasionally something completely different

Camel bikecycle at Burning Man. Unrelated to the contents of this post... sort of...

The OCaml programming language embodies a variety of languages: a core functional language, an object-oriented language, a module language, and a formatting language. As with any self-respecting compiler, the OCaml compiler is capable of bootstrapping itself, i.e. the compiler is capable of compiling its own source. A typical user of OCaml need not worry about bootstrapping, unless, you happen to be developing the OCaml compiler. Recently, the formatting language and the bootstrap process made me scratch my head — multiple times.

Though, first a bit of background: I am currently at OCaml Labs in Cambridge working with Leo White, KC Sivaramakrishnan, Stephen Dolan, and Anil Madhavapeddy on effect typing for Multicore OCaml. This work is based on previous work by White et al. [1]. The main goal of this work is to switch from nominal effects to structural effects. The motivation for this is worth its own post (in other words I will write about this in a future post). However, to kick things off I began by rebasing Leo's previous work on top of the Multicore OCaml master branch. Read more.

Group photo from NII Shonan Seminar 103: Semantics of Effects, Resources, and Applications.

It has been a busy couple of months in the effect handlers biz. The state of effects has been incremented quite a bit. Amongst the recent increments are some of my own work.

Expressivity study Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar got their paper accepted for publication at ICFP'17:

• On the Expressive Power of User-defined Effects: Effect Handlers, Monadic Reflection, Delimited Control (Draft, February). To appear at ICFP'17.

The title pretty much sums it up: using Felleisen's notion of macro expressivity they establish formal connections between the three different control mechanisms effect handlers, monadic reflection, and shift0/reset. They begin by developing a language called multi-adjunctive metalanguage (MAM) which is a lambda calculus with call-by-push-value semantics and a polymorphic type system with a simple effect system. They take MAM as their basis, in turn augmenting it with the three different control mechanisms.

Systems programming with handlers Towards the end of April I spent some time hacking on the Multicore OCaml compiler at OCaml Labs in Cambridge. Stephen Dolan, Spiros Eliopoulos, Anil Madhavapeddy, KC Sivaramakrishnan, Leo White, and I put together various bits of work we had done over the past year or so. We wrote it up as a draft paper:

• Concurrent System Programming with Effect Handlers (Draft, May)

In this draft we argue that effect handlers provide a compelling abstraction for systems programming, providing a direct-style alternative to the predominant callback style programming without sacrificing performance. We evaluate the claim by implementing a web server using effect handlers. We also present an approach to scoped signal handling using asynchronous effects. Stephen presented the draft paper at Trends in Functional Programming this week in Canterbury. Last week I gave brief 10-minute talk about paper during the CDT Pervasive Parallelism Student Showcase event. Read more.

Rod Burstall is one of the founding members of Laboratory for Foundations of Computer Science. The photograph is from Rodney Topor's flickr.

Rod Burstall dropped by the LFCS lab lunch yesterday. Lab lunch is an informal gathering of LFCS members which takes place every Tuesday. On rota a LFCS member gives a (supposedly lightweight) talk which is usually followed by a round of questions. Yesterday, after the questions, Rod stood up to remind us that we, as researchers, carry an ethical responsibility for how our research impact the surrounding society. Read more.

By the end of his talk, Leslie Lamport congratulated Gordon Plotkin.

Today is Gordon Plotkin's 70th birthday! The Laboratory for Foundations of Computer Science at the University of Edinburgh held an event in his honour today to celebrate his birthday. It was a full day of talks by friends, colleagues, and former students of Gordon's.

There is absolutely no doubt that Gordon is my favourite computer scientist. Gordon has made numerous contributions to computer science, and I have been exposed to many of them throughout my undergraduate and postgraduate studies. In fact, my current research topic comes from his line of work. Therefore I am also deeply grateful to be able to take part in the celebration of him on his 70th birthday. Read more.

The pond at Pembroke College, Cambridge. I have seen deeper rain puddles in Edinburgh.

I recently spent two weeks at OCaml Labs, the University of Cambridge implementing a compiler for the experimental, research language Links with effect handlers. During those two weeks I managed to compile a substantial subset of the Links language to native code, in particular, I managed to compile some programs that use handlers. My Links compiler reuses most of the infrastructure from the OCaml effects/multicore compiler.

At OCaml Labs I was working with KC Sivaramakrishnan, whom is working on the Multicore OCaml project.

In this post I shall discuss numerous three things: I will briefly describe the compiler infrastructure, discuss an example program that compiles, and how I encode multi-shot handlers. Read more.