FabULous Interoperability for ML and a Linear Language

TL;DR

This paper introduces a formal framework for multi-language programming systems to ensure usability without abstraction leaks, demonstrated through a system combining ML-like and linear type languages, with proofs of full abstraction and practical implementation.

Contribution

It defines a formal specification for leak-free multi-language embedding and demonstrates it by designing and implementing a system combining ML and linear types with full abstraction guarantees.

Findings

Embedding of ML is fully abstract in the multi-language system

The system enables safe resource management and in-place updates

Implementation extends OCaml with linear types

Abstract

Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages. We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system. To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language.