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.
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.
Malfunction is an untyped program representation, suitable as a
compilation target for functional languages. It's a thin wrapper
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 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
used. As well as
the jq manual, there
are many tutorials floating around the internet, of which my
favourite is this talk by Bob
jq is maintained by Nicolas Williams, William
Langford and a large ensemble
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]
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).
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]
Talk given at S-REPLS 3, about what was then work-in-progress on subtyping and type inference.
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]
A rant delivered at the Cambridge LLVM Day, about the inadequacy
gcroot interface for high-performance garbage
collectors. (A bit dated now: the new 'statepoints'
interface looks much
better designed, although it's still experimental).
Unpublished. Shows how to simulate a Turing machine using just
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
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]