Higher-order, Typed, Inferred, Strict

ACM SIGPLAN ML Family Workshop

Thursday September 4, 2014, Gothenburg, Sweden
(immediately following ICFP and preceding OCaml Users and Developers Workshop)

News

Dec 5, 2015
The post-proceedings with the extended versions of the selected ML Family and OCaml 2014 workshop submissions are published as EPTCS 198
Sep 10, 2014
The video record of all presentations is available on YouTube
< https://www.youtube.com/channel/UCP9g4dLR7xt6KzCYntNqYcw/videos >
(please search for the "ML Family 2014"). There is also a liveblog of the event
< http://www.syslog.cl.cam.ac.uk/2014/09/05/ml-family-workshop/ >
Sep 06, 2014
The workshop concluded. Added the code for the Scala implicits demo to the Program
July 30, 2014
Program
June 30, 2014
Review period concluded:
12 papers are to presented at the workshop;
2 more are to be presented at the joint poster session during the OCaml workshop.
May 19, 2014
Submission deadline extended to May 23
April 7, 2014
Post-proceedings will be published in EPTCS

Important dates

Sunday August 3
Early registration deadline
Thursday September 4, 2014
ML Family Workshop

ML is a very large family of programming languages that includes Standard ML, OCaml, F#, SML#, Manticore, MetaOCaml, JoCaml, Alice ML, Dependent ML, Flow Caml, and many others. All ML languages, beside the great deal of syntax, share several fundamental traits. They are all higher-order, strict, mostly pure, and typed, with algebraic and other data types. Their type systems inherit from Hindley-Milner. The development of these languages has inspired a significant amount of computer science research and influenced a number of programming languages, including Haskell, Scala and Clojure, as well as Rust, ATS and many others.

ML workshops have been held in affiliation with ICFP continuously since 2005. This workshop specifically aims to recognize the entire extended ML family and to provide the forum to present and discuss common issues, both practical (compilation techniques, implementations of concurrency and parallelism, programming for the Web) and theoretical (fancy types, module systems, metaprogramming). The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of the members of the ML family. We also encourage presentations from related languages (such as Scala, Rust, Nemerle, ATS, etc.), to exchange experience of further developing ML ideas.

The ML family workshop will be held in close coordination with the OCaml Users and Developers Workshop.

Program

09:00 Welcome
Session 1 Module Systems Chair: Didier Rémy
09:10 1ML -- core and modules as one (Or: F-ing first-class modules) (Research presentation)
Andreas Rossberg
We propose a redesign of ML in which modules are first-class values. Functions, functors, and even type constructors are one and the same construct. Likewise, no distinction is made between structures, records, or tuples, including tuples over types. Yet, 1ML does not depend on dependent types, and its type structure is expressible in terms of plain System F-omega, in a minor variation of our F-ing modules approach. Moreover, it supports (incomplete) Hindley/Milner-style type inference. Both is enabled by a simple universe distinction into small and large types.
09:35 Type-level module aliases: independent and equal (Research presentation)
Jacques Garrigue (Nagoya University); Leo White (University of Cambridge)
We promote the use of type-level module aliases, a trivial extension of the ML module system, which helps avoiding code dependencies, and provides an alternative to strengthening for type equalities.
10:00 - 10:30 coffee break
Session 2 Verification Chair: Anil Madhavapeddy
10:30 Well-typed generic smart-fuzzing for APIs (Experience report)
Thomas Braibant (Cryptosense); Jonathan Protzenko; Gabriel Scherer (INRIA)

In spite of recent advances in program certification, testing remains a widely-used component of the software development cycle. Various flavors of testing exist: popular ones include unit testing, which consists in manually crafting test cases for specific parts of the code base, as well as quickcheck-style testing, where instances of a type are automatically generated to serve as test inputs.
These classical methods of testing can be thought of as internal testing: the test routines access the internal representation of the data structures to be checked. We propose a new method of external testing where the library only deals with a module interface. The data structures are exported as abstract types; the testing framework behaves like regular client code and combines functions exported by the module to build new elements of the various abstract types. Any counter-examples are then presented to the user. Furthermore, we demonstrate that this methodology applies to the smart-fuzzing of security APIs.

10:55 Improving the CakeML Verified ML Compiler (Research presentation)
Ramana Kumar; Magnus O. Myreen (University of Cambridge); Michael Norrish (NICTA); Scott Owens (University of Kent)
The CakeML project comprises a mechanised semantics for a subset of Standard ML and a formally verified compiler. We will discuss our plans for improving and applying CakeML in four directions: optimisations, new primitives, a library, and verified applications.
11:20 - 11:40 break
Session 3 Beyond Hindley-Milner Chair: Jacques Garrigue
11:40 The Rust Language and Type System (Demo)
Felix Klock; Nicholas Matsakis (Mozilla Research)
Rust is a new programming language for developing reliable and efficient systems. It is designed to support concurrency and parallelism in building applications and libraries that take full advantage of modern hardware. Rust's static type system is safe and expressive and provides strong guarantees about isolation, concurrency, and memory safety.
Rust also offers a clear performance model, making it easier to predict and reason about program efficiency. One important way it accomplishes this is by allowing fine-grained control over memory representations, with direct support for stack allocation and contiguous record storage. The language balances such controls with the absolute requirement for safety: Rust's type system and runtime guarantee the absence of data races, buffer overflows, stack overflows, and accesses to uninitialized or deallocated memory. In this demonstration, we will briefly review the language features that Rust leverages to accomplish the above goals, focusing in particular on Rust's advanced type system, and then show a collection of concrete examples of program subroutines that are efficient, easy for programmers to reason about, and maintain the above safety property.
If time permits, we will also show the current state of Servo, Mozilla's research web browser that is implemented in Rust.
12:05 Doing web-based data analytics with F# (Informed Position)
Tomas Petricek (University of Cambridge); Don Syme (Microsoft Research Cambridge)
With type providers that integrate external data directly into the static type system, F# has become a fantastic language for doing data analysis. Rather than looking at F# features in isolation, this paper takes a holistic view and presents the F# approach through a case study of a simple web-based data analytics platform.
12:30 - 14:00 lunch
Session 4 Implicits Chair: Andreas Rossberg
14:00 Implicits in Practice (Demo)
Nada Amin (EPFL); Tiark Rompf (EPFL & Oracle Labs)
Popularized by Scala, implicits are a versatile language feature that are receiving attention from the wider PL community. This demo will present common use cases and programming patterns with implicits in Scala.
The annotated demonstration code used in the presentation
14:25 Modular implicits (Research presentation)
Leo White; Frédéric Bour (University of Cambridge)
We propose a system for ad-hoc polymorphism in OCaml based on using modules as type-directed implicit parameters.
14:50 - 15:10 break
Session 5 To the bare metal Chair: Martin Elsman
15:10 Metaprogramming with ML modules in the MirageOS (Experience report)
Anil Madhavapeddy; Thomas Gazagnaire (University of Cambridge); David Scott (Citrix Systems R&D); Richard Mortier (University of Nottingham)
In this talk, we will go through how MirageOS lets the programmer build modular operating system components using a combination of functors and metaprogramming to ensure portability across both Unix and Xen, while preserving a usable developer workflow.
15:35 Compiling SML# with LLVM: a Challenge of Implementing ML on a Common Compiler Infrastructure (Research presentation)
Katsuhiro Ueno; Atsushi Ohori (Tohoku University)
We report on an LLVM backend of SML#. This development provides detailed accounts of implementing functional language functionalities in a common compiler infrastructure developed mainly for imperative languages. We also describe techniques to compile SML#'s elaborated features including separate compilation with polymorphism, and SML#'s unboxed data representation.
16:00 - 16:30 tea break
Session 6 No longer foreign Chair: Oleg Kiselyov
16:30 A Simple and Practical Linear Algebra Library Interface with Static Size Checking (Experience report)
Akinori Abe; Eijiro Sumii (Tohoku University)
While advanced type systems--specifically, dependent types on natural numbers--can statically ensure consistency among the sizes of collections such as lists and arrays, such type systems generally require non-trivial changes to existing languages and application programs, or tricky type-level programming. We have developed a linear algebra library interface that guarantees consistency (with respect to dimensions) of matrix (and vector) operations by using generative phantom types as fresh identifiers for statically checking the equality of sizes (i.e., dimensions). This interface has three attractive features in particular.
(i) It can be implemented only using fairly standard ML types and its module system. Indeed, we implemented the interface in OCaml (without significant extensions like GADTs) as a wrapper for an existing library.
(ii) For most high-level operations on matrices (e.g., addition and multiplication), the consistency of sizes is verified statically. (Certain low-level operations, like accesses to elements by indices, need dynamic checks.)
(iii) Application programs in a traditional linear algebra library can be easily migrated to our interface. Most of the required changes can be made mechanically.
To evaluate the usability of our interface, we ported to it a practical machine learning library (OCaml-GPR) from an existing linear algebra library (Lacaml), thereby ensuring the consistency of sizes.
16:55 SML3d: 3D Graphics for Standard ML (Demo)
John Reppy (University of Chicago)
The SML3d system is a collection of libraries designed to support real-time 3D graphics programming in Standard ML (SML). This paper gives an overview of the system and briefly highlights some of the more interesting aspects of its design and implementation.
18:00 Closure

Poster presentation
at the joint poster session with the OCaml workshop, Sep 5

  Nullable Type Inference
Michel Mauny; Benoit Vaugon (ENSTA-ParisTech)
We present a type system for nullable types in an ML-like programming language. We start with a simple system, presented as an algorithm, whose interest is to introduce the formalism that we use. We then extend it as system using subtyping constraints, that accepts more programs. We state the usual properties for both systems. This is work in progress.

Format

Since 2010, the ML workshop has adopted an informal model. Presentations are selected from submitted abstracts. There are no published proceedings, so any contributions may be submitted for publication elsewhere. We hope that this format encourages the presentation of exciting (if unpolished) research and deliver a lively workshop atmosphere.

Each presentation should take 20-25 minutes, except demos, which should take 10-15 minutes. The exact time will be decided based on the number of accepted submissions. The presentations will likely be recorded.

Post-conference proceedings

The post-proceedings of selected papers from the ML Family and the OCaml Users and Developers workshops will be published in the Electronic Proceedings in Theoretical Computer Science. The Program Committee shall invite interested authors of selected presentations to expand their abstract for inclusion in the proceedings. The submissions are to be reviewed according to the EPTCS standards.

Coordination with the OCaml Users and Developers Workshop

The OCaml workshop is seen as more practical and is dedicated in significant part to the OCaml community building and the evolution of the OCaml system. In contrast, the ML family workshop is not focused on any language in particular, is more research oriented, and deals with general issues of the ML-style programming and type systems. Yet there is an overlap, which we are keen to explore in various ways. The authors who feel their submission fits both workshops are encouraged to mention it at submission time or contact the Program Chairs.

Program Committee

Kenichi Asai Ochanomizu University, Japan
Matthew Fluet Rochester Institute of Technology, USA
Jacques Garrigue Nagoya University, Japan
Dave Herman Mozilla, USA
Stefan Holdermans Vector Fabrics, Netherlands
Oleg Kiselyov (Chair) University of Tsukuba, Japan
Keiko Nakata Institute of Cybernetics, Estonia
Didier Rémy INRIA Paris-Rocquencourt, France
Zhong Shao Yale University, USA
Hongwei Xi Boston University, USA

Steering Committee

Alain Frisch LexiFi, France
Oleg Kiselyov University of Tsukuba, Japan
Daan Leijn Microsoft Research, Redmond, USA
Anil Madhavapeddy Cambridge University, UK
Greg Morrisett Harvard University, USA
Chung-chieh Shan (Chair) Indiana University, USA

Resources