Published: 5th December 2015|
|Preface Oleg Kiselyov and Jacques Garrigue|
|A Simple and Practical Linear Algebra Library Interface with Static Size Checking Akinori Abe and Eijiro Sumii||1|
|Modular implicits Leo White, Frédéric Bour and Jeremy Yallop||22|
|In the Age of Web: Typed Functional-First Programming Revisited Tomas Petricek, Don Syme and Zach Bray||64|
|Improving Type Error Messages in OCaml Arthur Charguéraud||80|
In total 29 papers were presented at the ML Family and OCaml workshops, either orally or as posters. Not all presentations could be written up as full journal submissions: either the work was still in progress, or the authors lacked time. Eventually PCs selected four submissions, whose authors agreed to do the required hard work of writing a full paper, with in-depth treatment of the material, including either examples, detailed formal treatment or evaluation and benchmarks, as applicable. The PCs gave concrete recommendations to the authors. The papers were reviewed by two reviewers, one of whom was one of the original PC reviewers, according to the standards of post-proceedings. All four submissions have eventually been recommended for publication. We are very grateful to the reviewers for their work in selecting and helping to improve the submissions.
The ML Family workshop aims to recognize the entire extended family of ML and ML-like languages: languages that are Higher-order, Typed, Inferred, and Strict. It provides the forum to 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.
The OCaml workshop is more specifically targeted at the OCaml community, with an emphasis on new proposals and tools aiming to improve OCaml, its environment, and the functioning of the community. As such, it is interested in works on the type system, language extensions, compiler and optimizations, applications, tools, and experience reports of exciting uses.
The papers in this volume are representative of the workshops and their scope.
The first article, by Akinori Abe and Eijiro Sumii, describes a typed wrapper for the LACAML linear algebra library interface, which uses the technique of generative phantom types to check the coherence of matrix sizes. It is even able to check statically the size coherence when the size itself is unknown. The authors could implement in ordinary OCaml what would seem to require dependent types. The practical applicability of the method was verified, and many examples are given explaining how this level of abstraction appears to be a sweet spot between avoided run-time errors, and the burden for the programmer.
The next article by Leo White, Frédéric Bour and Jeremy Yallop presents the design and implementation of Modular Implicits. This is a proposed extension to the OCaml language for ad-hoc polymorphism, inspired by implicits in Scala and type classes in Haskell. The new element is the use of ML modules, as a way to define implicits and as a way to implement (elaborate) them. Modular implicits turn out to encompass even such features as constructor and multi-parameter classes and associated types. The paper has many examples and the detailed discussion of thorny issues such as backtracking, canonicity, order dependence and compositionality.
Tomas Petricek and Don Syme in In the Age of Web: Typed Functional-First Programming Revisited well defend a controversial position, of how 'data in a cloud' change the nature of programs and in particular, the meaning and guarantees of types. The authors use F# to illustrate the challenges of web-age programming, where data and even their types are subject to change and where interaction with remote programs (possibly written in different language) is the norm.
The last article, by Arthur Charguéraud, proposes a number of techniques to improve error messages in languages that use Hindley-Milner type inference. Rather than looking for a new algorithm, it focuses on providing unbiased and clear error messages to the user, based on a trove of common errors from beginners. The improved messages, implemented as a patch to the OCaml type checker, suggest explicit causes for common errors, in a way that avoid confusing the user.
We hope this volume is informative, and illustrative of the workshops.
|October 30, 2015|| Oleg Kiselyov |