Journal article
The root cause of blame: contracts for intersection and union types
Proceedings of ACM on programming languages, Vol.2(OOPSLA), pp.1-29
10/24/2018
DOI: 10.1145/3276504
Abstract
Gradual typing has emerged as the tonic for programmers with a thirst for a blend of static and dynamic typing. Contracts provide a lightweight form of gradual typing as they can be implemented as a library, rather than requiring a gradual type system. Intersection and union types are well suited to static and dynamic languages: intersection encodes overloaded functions; union encodes uncertain data arising from branching code. We extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, for the first time giving a uniform treatment to both. Each operator requires a single reduction rule that does not depend on the constituent types or the context of the operator. We present a new method for defining contract satisfaction based on blame behaviour. A value positively satisfies a type if applying a contract of that type can never elicit positive blame. A continuation negatively satisfies a type if applying a contract of that type can never elicit negative blame. We supplement our definition of satisfaction with a series of monitoring properties that satisfying values and continuations should have.
Details
- Title: Subtitle
- The root cause of blame: contracts for intersection and union types
- Creators
- Jack Williams - University of EdinburghJ. Garrett Morris - University of KansasPhilip Wadler - University of Edinburgh
- Resource Type
- Journal article
- Publication Details
- Proceedings of ACM on programming languages, Vol.2(OOPSLA), pp.1-29
- DOI
- 10.1145/3276504
- ISSN
- 2475-1421
- eISSN
- 2475-1421
- Grant note
- DOI: 10.13039/501100000266, name: Engineering and Physical Sciences Research Council, award: EP/K034413/1; DOI: 10.13039/100006112, name: Microsoft Research
- Language
- English
- Date published
- 10/24/2018
- Academic Unit
- Computer Science
- Record Identifier
- 9984259411802771
Metrics
10 Record Views