The Root Cause of Blame: Contracts for Intersection and Union Types
View/ Open
Issue Date
2018-11Author
Williams, Jack
Morris, J. Garrett
Wadler, Philip
Publisher
Association for Computing Machinery
Type
Article
Article Version
Scholarly/refereed, publisher version
Rights
© 2018 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.
Metadata
Show full item recordAbstract
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.
Collections
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
Items in KU ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
We want to hear from you! Please share your stories about how Open Access to this item benefits YOU.