The Blame Theorem for a Linear Lambda Calculus with Type Dynamic
| Autor: | Peter Thiemann, Luminous Fennell |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
Simply typed lambda calculus
Programming language Computer science System F computer.software_genre Dependent type Lambda cube Curry–Howard correspondence Pure type system TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Church encoding Calculus Computer Science::Programming Languages computer Typed lambda calculus |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783642404467 Trends in Functional Programming |
| DOI: | 10.1007/978-3-642-40447-4_3 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|