rapid unplanned disassembly

Projects

Multicore OCaml

Back in 2014, I designed (with Leo White) and began to implement a multicore runtime for the OCaml programming language, which I worked on sporadically as a means of avoiding my PhD work. I've now finished my PhD, and KC Sivaramakrishnan (who worked on the impressive MultiMLton project) has joined the effort, so this project is finally getting the attention it deserves. (The first 90% of the work is done, so we only have the remaining 90% and then the final 90% left to do).

Recently, I've been working on a memory model for parallel OCaml programs, which specifies the behaviour of programs sharing mutable locations between threads, balancing performance and the ability to reason about code.

Multicore OCaml development happens on github.

Type inference with subtyping

My PhD (supervised by the wonderful Alan Mycroft) was on cleanly integrating type inference with subtyping, allowing functional and object-oriented programming techniques to be seamlessly combined.

The result is a type inference algorithm in the Hindley-Milner vein, which manages to infer compact principal types even in the presence of record subtyping and co-/contra-variance. Technically, this involved taking an algebraic approach to the definition of subtyping and introducing biunification, an analogue of unification that works with subtyping constraints.

You can read my thesis, read the POPL paper, see a prototype type checker, or get the code.

Malfunction

Malfunction is an untyped program representation, suitable as a compilation target for functional languages. It's a thin wrapper around the Lambda intermediate language of OCaml, providing a means for other languages to target the mature OCaml back-end.

I presented it at the ML Workshop 2016, along with a prototype backend for the Idris programming language, which significantly outperformed Idris' native C backend. Currently, Frederik Hanghøj Iversen and Jan Mas Rovira are working on a Malfunction back-end for Agda

jq

jq is a command-line tool for filtering, transforming, and generally mangling JSON data. It's designed to be concise and easy to use for simple tasks, but if you dig a little deeper you'll find a featureful functional programming language hiding underneath. It's become widely used. As well as the jq manual, there are many tutorials floating around the internet, of which my favourite is this talk by Bob Tiernay.

These days, jq is maintained by Nicolas Williams, William Langford and a large ensemble cast.

Papers and talks

Polymorphism, subtyping and type inference in MLsub Jan 2017

Paper published at POPL 2017, with Alan Mycroft. Covers type inference with principal types for a simple core ML calculus with subtyping, including some of the results from my thesis. [pdf] [slides] [extended slides]

Algebraic Subtyping Sep 2016

My thesis. Presents a type system (the first!) combining ML-style parametric polymorphism and subtyping, with type inference, principal types and decidable type subsumption. [abstract] [pdf]

Irrelevant classical logic in Agda Nov 2016

Talk given at SPLS Nov '16. By careful abuse of Agda's proof-irrelevance, we can use some classical principles like Markov's principle while remaining constructive. During the talk, we ran into a soundness bug in Agda! (which was quickly fixed when reported).

Malfunctional Programming Sep 2016

Talk given at the ML Workshop 2016. Introduces Malfunction, explains why the OCaml back-end is a good candidate for reuse, and gives some preliminary results from a new Idris back-end. [pdf] [talk]

Towards an effect system for OCaml May 2016

Report from the Dagstuhl seminar on algebraic effects. Matija Pretnar, Leo White, KC Sivaramakrishnan and I worked out some details of how to introduce effect typing to OCaml, and collaborated on a toy implementation. Later, Leo integrated effect typing with the real OCaml typechecker, and gave a talk at HOPE 2016. [pdf] [code]

Principal Type Inference with Subtyping Apr 2016

Talk given at S-REPLS 3, about what was then work-in-progress on subtyping and type inference.

Polymorphism, subtyping and type inference in MLsub Sep 2015

Talk given at the ML Workshop 2015, which later became a POPL paper. With Alan Mycroft. [pdf] [talk]

Multicore OCaml Sep 2014

Talk given at the OCaml Workshop 2014, about the design of the multicore OCaml runtime. With Leo White and Anil Madhavapeddy. [pdf] [talk]

Fun with Semirings Sep 2013

Paper published at ICFP 2013. I show how a single small piece of code implementing the 'closure' operation on a semiring can find shortest paths, analyse data flow, pack knapsacks and simulate Petri nets. Selected as a SIGPLAN Research Highlight. [pdf] [slides]

Challenges using LLVM for OCaml Nov 2013

A rant delivered at the Cambridge LLVM Day, about the inadequacy of LLVM's gcroot interface for high-performance garbage collectors. (A bit dated now: the new 'statepoints' interface looks much better designed, although it's still experimental). [slides]

mov is Turing-complete Jul 2013

Unpublished. Shows how to simulate a Turing machine using just the x86 mov instruction (and one unconditional branch). Chris Domas took the joke a bit too far by actually implementing it in a C compiler, and gave a talk about it. [pdf]

Compiler support for lightweight context switching Jan 2013

Paper published in ACM TACO and presented at HiPEAC 2013, with Servesh Muralidharan and David Gregg. We found that by adding context-switching as a language primitive rather than a library feature, we can do extremely efficient user-level concurrency. [paper]