FabULous Interoperability for ML and a Linear Language
FabULous Interoperability for ML and a Linear Language
复制标题
机器学习和线性语言出色的互操作性
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Amal J. Ahmed
中科院分区：
文献类型：
--
作者：
Gabriel Scherer;Max S. New;Nick Rioux;Amal J. Ahmed
一些编程系统不是试图覆盖所有感兴趣的功能的单一编程语言，而是通过将更简单的语言组合在一起来设计的，这些语言合作覆盖相同的功能空间。这可以通过使每个部分比整体更简单来提高可用性，但是存在从一种语言到另一种语言的抽象泄漏的风险，这将打破只熟悉一种或一些相关语言的用户的期望。
我们提出了一个正式的规范，它意味着一个给定的语言在多语言系统中是可用的，没有泄漏：它应该嵌入到多语言中的一个完全抽象的方式，也就是说，它的上下文等价在更大的系统中应该是不变的。
为了证明我们提出的设计原则和形式规范标准，我们设计了一个多语言编程系统，结合了ML类静态类型的函数式语言和另一种语言的线性类型和线性状态。我们的目标是覆盖混合函数式编程和线性状态（所有权）的语言的表现力的很大一部分，而复杂性只是一小部分。我们证明了ML嵌入到多语言系统中是完全抽象的：函数式程序员不应该害怕抽象泄漏。我们展示了组合程序的例子，展示了就地内存更新和安全的资源处理，以及用我们的线性语言扩展OCaml的实现。
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.