Loading...
The Root Cause of Blame: Contracts for Intersection and Union Types
Williams, Jack Morris, J. Garrett Wadler, Philip
Williams, Jack
Morris, J. Garrett
Wadler, Philip
Citations
Altmetric:
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.
Description
Date
2018-11
Journal Title
Journal ISSN
Volume Title
Publisher
Association for Computing Machinery
Research Projects
Organizational Units
Journal Issue
Keywords
Functional languages, Semantics, Theory of computation, Program semantics, Software and its engineering, Gradual typing, Blame, Contracts, Intersection, Union
Citation
Jack Williams, J. Garrett Morris, and Philip Wadler. 2018. The Root Cause of Blame: Contracts for Intersection and Union Types. Proc. ACM Program. Lang. 2, OOPSLA, Article 134 (November 2018), 29 pages. https://doi.org/10.1145/3276504