Semantic Encapsulation using Linking Types

Interoperability pervades nearly all mainstream language implementations, as most systems leverage subcomponents written in different languages. And yet, such linking can expose a language to foreign behaviors that are internally inexpressible, which poses a serious threat to safety invariants and programmer reasoning. To preserve such invariants, a language may try to add features to limit the reliance on external libraries, but endless extensions can obscure the core abstractions the language was designed to provide. In this paper, we outline an approach that encapsulates foreign code in a sound way-i.e., without disturbing the invariants promised by types of the core language. First, one introduces novel linking types that characterize the behaviors of foreign libraries that are inexpressible in the core language. To reason about the soundness of linking, one constructs a realizability model that captures the meaning of both core types and linking types as sets of target-language terms. Using this model, one can formally prove when foreign behavior is encapsulated; that is, unobservable to core code. We show one way to discharge such proofs automatically by augmenting the compiler to insert verified encapsulation wrappers around components that use foreign libraries. Inspired by existing approaches to FFIs, we develop a pair of case studies that extend a pure, functional language: one extension for state, and another for exceptions. The first allows us to implement mutable references via a library, whereas the second allows us to implement try and catch as library functions. Both extensions and the overall system are proven sound using logical relations that use realizability techniques.