Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop Thursday September 4, 2014, Gothenburg, Sweden Call For Participation and Program http://okmij.org/ftp/ML/ML14.html Early registration deadline is August 3. Please register at https://regmaster4.com/2014conf/ICFP14/register.php The workshop is conducted in close cooperation with the OCaml Users and Developers Workshop http://ocaml.org/meetings/ocaml/2014/ taking place on September 5. *** Program with short summaries *** (The online version links to the full 2-page abstracts) * Welcome 09:00 * Session 1: Module Systems 09:10 - 10:00 1ML -- core and modules as one (Or: F-ing first-class modules) 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. Type-level module aliases: independent and equal Jacques Garrigue; Leo White 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. * Session 2: Beyond Hindley-Milner 10:30 - 11:20 The Rust Language and Type System (Demo) Felix Klock; Nicholas Matsakis 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. Doing web-based data analytics with F# (Informed Position) Tomas Petricek; Don Syme 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. * Session 3: Verification 11:40 - 12:30 Well-typed generic smart-fuzzing for APIs (Experience report) Thomas Braibant; Jonathan Protzenko; Gabriel Scherer 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. Improving the CakeML Verified ML Compiler Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens 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. * Session 4: Implicits 14:00 - 14:50 Implicits in Practice (Demo) Nada Amin; Tiark Rompf 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. Modular implicits Leo White; Frédéric Bour We propose a system for ad-hoc polymorphism in OCaml based on using modules as type-directed implicit parameters. * Session 5: To the bare metal 15:10 - 16:00 Metaprogramming with ML modules in the MirageOS (Experience report) Anil Madhavapeddy; Thomas Gazagnaire; David Scott; Richard Mortier 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. Compiling SML# with LLVM: a Challenge of Implementing ML on a Common Compiler Infrastructure Katsuhiro Ueno; Atsushi Ohori 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. * Session 6: No longer foreign 16:30 - 18:00 A Simple and Practical Linear Algebra Library Interface with Static Size Checking (Experience report) Akinori Abe; Eijiro Sumii 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. SML3d: 3D Graphics for Standard ML (Demo) John Reppy 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. * Poster presentation, at the joint poster session with the OCaml workshop Nullable Type Inference Michel Mauny; Benoit Vaugon 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. 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 Tallinn University of Technology, Estonia Didier Remy INRIA Paris-Rocquencourt, France Zhong Shao Yale University, USA Hongwei Xi Boston University, USA