The blame theorem for a linear lambda calculus with type dynamic

Abstract

Scripting languages have renewed the interest in languages with dynamic types. For various reasons, realistic programs comprise dynamically typed components as well as statically typed ones. Safe and seamless interaction between these components is achieved by equipping the statically typed language with a type Dynamic and coercions that map between ordinary types and Dynamic. In such a gradual type system, coercions that map from Dynamic are checked at run time, throwing a blame exception on failure. This paper enlightens a new facet of this interaction by considering a gradual type system for a linear lambda calculus with recursion and a simple kind of subtyping. Our main result is that linearity is orthogonal to gradual typing. The blame theorem, stating that the type coercions always blame the dynamically typed components, holds in a version analogous to the one proposed by Wadler and Findler, also the operational semantics of the calculus is given in a quite different way. The significance of our result comes from the observation that similar results for other calculi, e.g., affine lambda calculus, standard call-by-value and call-by-name lambda calculus, are straightforward to obtain from our results, either by simple modification of the proof for the affine case, or, for the latter two, by encoding them in the linear calculus. © 2013 Springer-Verlag.