co-located with ICFP 2010
Baltimore, Maryland, United States
Sunday, September 26, 2010

ML is a family of programming languages that includes dialects known as Standard ML, Objective Caml, and F#. The development of these languages has inspired a large amount of computer science research, both practical and theoretical. This workshop aims to provide a forum to encourage discussion and research on ML and related technology (higher-order, typed, or strict languages).

The 2010 Workshop on ML will be held in conjunction with the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010) in Baltimore, Maryland, United States. Previous instances were ML 2009 in Edinburgh, Scotland, United Kingdom, ML 2008 in Victoria, British Columbia, Canada, ML 2007 in Freiburg, Germany, ML 2006 in Portland, Oregon, United States, and ML 2005 in Tallinn, Estonia.


Invited Talk (chair: Matthew Fluet, Rochester Institute of Technology)
9:00 Visual F#: Bringing F# to Visual Studio 2010
Luke Hoban (Microsoft Research)
10:00 Break
Session 1 (chair: Jacques Garrigue, Nagoya University Graduate School of Mathematics)
10:30 Probabilistic programming using first-class stores and first-class continuations
Oleg Kiselyov (FNMOC); Chung-chieh Shan (Rutgers University)

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

10:55 Effective progamming in ML
Daan Leijen (Microsoft Research); Ross Tate (University of California, San Diego)

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.

11:20 Discussion
Session 2 (chair: Derek Dreyer; Max Planck Institute for Software Systems)
11:30 First-class modules and composable signatures in Objective Caml 3.12
Alain Frisch (LexiFi); Jacques Garrigue (Nagoya University Graduate School of Mathematics)

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.

11:55 First-class modules: hidden power and tantalizing promises
Jeremy Yallop (Applicative Ltd); Oleg Kiselyov (FNMOC)

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

12:20 Discussion
12:30 Lunch break
Session 3 (chair: Daniel Spoonhower, Google)
14:00 Deriving a Typed Implementation for Coroutines in ML
Konrad Anton (Universitat Freiburg); Peter Thiemann (Universitat Freiburg)

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.

14:25 The Design Rationale for Multi-MLton
Suresh Jagannathan (Purdue University); Armand Navabi (Purdue University); KC Sivaramakrishnan (Purdue University); Lukasz Ziarek (Purdue University)

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.

14:50 Discussion
Session 4 (chair: Claudio Russo; Microsoft Research)
15:00 Mirage: high-performance ML kernels in the cloud
Anil Madhavapeddy (University of Cambridge); Thomas Gazagnaire (INRIA Sophia Antipolis)

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.

15:25 Hosting a Standard ML compiler in a Web Browser: Status Report
Martin Elsman

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

15:50 Discussion
16:00 Break
Session 5 (chair: Eijiro Sumii; Tohoku University)
16:30 A simple and effective method for assigning blame for type errors
David MacQueen (University of Chicago)

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.

16:55 The MetaOCaml files: Status report and research proposal
Oleg Kiselyov (FNMOC); Chung-chieh Shan (Rutgers University)

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

17:20 Discussion
17:30 Finish