Home » forums » LtU Forum

On type safety for core Scala: "From F to DOT: Type Soundness Proofs with Definitional Interpreters"

From F to DOT: Type Soundness Proofs with Definitional Interpreters by Tiark Rompf and Nada Amin:

Scala's type system unifies aspects of ML-style module systems, object-oriented, and functional programming paradigms. The DOT (Dependent Object Types) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, type soundness has only been established for a very restricted subset of DOT (muDOT), and it has been shown that adding important Scala features such as type refinement or extending subtyping to a lattice breaks at least one key metatheoretic property such as narrowing or subtyping transitivity, which are usually required for a type soundness proof.
The first main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a richer DOT calculus that includes both type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that narrowing and subtyping transitivity only need to hold for runtime objects, but not for code that is never executed. Alas, the dominant method of proving type soundness, Wright and Felleisen's syntactic approach, is based on term rewriting, which does not make an adequate distinction between runtime and type assignment time.
The second main contribution of this paper is to demonstrate how type soundness proofs for advanced, polymorphic, type systems can be carried out with an operational semantics based on high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proof for System F<: based on a definitional interpreter. We discuss the challenges that arise in this setting, in particular due to abstract types, and we illustrate in detail how DOT-like calculi emerge from straightforward generalizations of the operational aspects of F<:.

Not only they solve a problem that has been open for 12 years, but they also deploy interesting techniques to make the proof possible and simple. As they write themselves, that includes the first type-soundness proof for F<: using definitional interpreters — that is, at least according to some, denotational semantics.

Understated Twitter announcement here.

By Blaisorblade at 2015-10-24 13:45 | LtU Forum | previous forum topic | next forum topic | other blogs | 21931 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I'd like to highlight a

I'd like to highlight a couple of unusual tricks — not necessarily novel, but still very unusual

  • Among other things, their proof uses a definitional interpreter (or a denotational semantics) for a partial language without needing domain theory; they simply keep track of the number of remaining evaluation steps. This trick probably comes from step-indexed logical relations, but I've never seen it used by itself this way. In other words, their partiality monad amounts to:

    type Partial T = Int -> MaybeResult T
data MaybeResult T = Timeout | Done T
  • when writing that interpreter, they extend closures to close over types. This is not strictly novel (and they don’t claim so), and the same thing shows up naturally if you write an intepreter for PTS, and probably for dependent types. Yet, you see that seldom, because you almost never have reasons to consider environments in a semantics for System F, rather than use substitution. I ran into the idea independently some time ago, and it appears surprising to others as well.
  • Most of their effort, however, is spent taming abstract types with potentially inconsistent constraints. Luckily, such constraints only arise for code that cannot be run, hence they cannot harm type soundness. Actually proving the required lemmas seems trickier, but they still manage.
By Blaisorblade at Sat, 2015-10-24 14:35 | login or register to post comments