Probabilistic inference is a popular way to deal with uncertainty in many areas of science and engineering. Following the declarative approach of expressing probabilistic models and inference algorithms as separate, reusable modules, we built a probabilistic programming language as an OCaml library and applied it to several problems. We describe this embedded domain-specific language using aircraft tracking as an example. We focus on our use of first-class stores and first-class continuations to perform faster inference (with local laziness and full-speed determinism) and express more models (with stochastic memoization and nested inference).

Supplementary materials

• HANSEI: Embedded Probabailistic Programming

The ML language let one freely use arbitrary (side) effects. This is despite the fact that unknown and unrestricted side effects are the cause of many software problems. We propose a language based on ML where effects are treated in a disciplined way, and where the potential side-effects of a function are apparent in its type signature. In contrast to most effect systems that are meant for internal compiler optimizations, our system is designed to be used by the programmer. Inspired by Haskell, we use a coarse-grained hierarchy of effects, like pure and io, which makes it convenient to read and write type signatures. The type and effect of expressions can also be inferred automatically, and we describe a polymorphic type inference system based on Hindley-Milner style inference.

Notwithstanding its name, Objective Caml has a full-fledged SML-style module system. Its applicative functors allow for flexible parameterization of components, and many libraries, including the preprocessor Camlp4, use them for their structure. More recent extensions include the addition of recursive modules, and private row types, which allow even more involved structuring.

While this module language is overall successful, as demonstrated by its active use, it has also some well-known weaknesses. Among them, one can mention its mostly static nature — despite the availability of local module definitions inside expressions, modules remained second class citizens — and the absence of compositionality of its signature language. In this presentation we show how these two weaknesses were alleviated in Objective Caml 3.12, and what are the concrete applications of these features.

First-class modules introduced in OCaml 3.12 make type constructors first-class, permitting type constructor abstraction and polymorphism. It becomes possible to manipulate and quantify over types of higher kind. We demonstrate that as a consequence, full-scale, efficient generalized algebraic data types (GADTs) become expressible in OCaml 3.12 as it is, without any further extensions. Value-independent generic programming along the lines of Haskell's popular "Generics for the masses" become possible in OCaml for the first time. We discuss extensions such as a better implementation of polymorphic equality on modules, which can give us intensional type analysis (aka, type-case), permitting generic programming frameworks like SYB.

Supplementary materials

• First-Class modules: submission and code

Starting from a reduction semantics for a calculus that supports several styles of coroutines, we apply Danvy's method to obtain equivalent definitional interpreters. We further transform these interpreters to a denotational implementation, i.e., a set of combinators that interpret the individual syntactic constructors of the original calculus. By applying existing type systems for programs with continuations, we obtain a sound typing for the coroutine combinators from the transla- tion. This set of combinators comprises a type-safe implementation of coroutines in OCaml which is correct by construction.

Multi-MLton is a compiler and runtime environment that targets scalable multicore platforms. It combines new language abstractions and associated compiler analyses for expressing and implementing various kinds of fine-grained parallelism (safe futures, speculation, transactions, etc.), along with a sophisticated runtime system tuned to efficiently handle large numbers of lightweight threads.

Multi-MLton defines a programming model in which threads primarily communicate via message-passing. It differs from other message-passing systems insofar as the abstractions it provides per- mit (a) the expression of isolation of communication effects among groups of communicating threads; (b) composable speculative actions that are message-passing aware; (c) the construction of asynchronous events that seamlessly integrate abstract asynchronous communication protocols with abstract CML-style events, and (d) deterministic concurrency within threads to enable the extraction of additional parallelism when feasible and profitable.

These abstractions are supported by a combination of compile-time analyses and specialized runtime structures to enable efficient execution on scalable multicore and manycore platforms.

The wide availability of cloud computing offers an un- precedented opportunity to rethink how we construct network applications. The cloud is currently mostly used to package up existing software stacks and operating systems. We instead view the cloud as a stable hardware platform, and present a programming framework which permits applications to be constructed to run directly on top of a hypervisor without intervening software layers.

Our framework, dubbed Mirage, extends the Objective Caml language with I/O extensions and a custom runtime to emit binaries that execute as a paravirtual operating system directly under Xen.

The custom run-time is significantly simpler than a general-purpose operating system, with a static single-process 64-bit address space, and "zero-copy" I/O that works directly with the OCaml garbage collector. As a result, Mirage applications exhibit significant performance speedups for I/O and memory handling versus the same code running under Linux/Xen.

We present how we have managed to host an entire Standard ML compiler in a Web browser by constructing and bootstrapping SMLtoJs, a compiler that translates all of Standard ML into JavaScript.

Supplementary materials

• SMLtoJs: A Standard ML to JavaScript Compiler
• SMLtoJs Prompt

The Hindley-Milner type system used in ML sometimes produces type errors whose causes are not obvious. Here we present a simple, pragmatic approach to augmenting type error messages with additional information about the textual origins of conflicting types. This additional information is, in practice, usually enough to quickly identify the root cause of type errors.

Custom code generation is the leading approach to reconciling gen- erality with performance. MetaOCaml, a dialect of OCaml, is the best-developed way today to write custom code generators and assure them type-safe across multiple stages of computation. Nevertheless, the continuing interest from the community has yet to result in a mature implementation of MetaOCaml that integrates cleanly with OCaml's type checker and run-time system. Even in theory, it is unclear how staging interacts with effects, polymorphism, and user-defined data types.

We report on the status of the ongoing MetaOCaml project, focusing on the gap between theory and practice and the difficulties that arise in a full-featured staged language rather than an idealized calculus. We highlight foundational problems in type soundness and cross-stage persistence that demand investigation. We also suggest a lightweight implementation of a two-stage dialect of OCaml, as syntactic sugar.

Supplementary materials

• BER MetaOCaml