Williams, JackMorris, J. GarrettWadler, Philip2018-10-262018-10-262018-11Jack 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/3276504https://hdl.handle.net/1808/27076Gradual 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.© 2018 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.https://creativecommons.org/licenses/by/4.0/Functional languagesSemanticsTheory of computationProgram semanticsSoftware and its engineeringGradual typingBlameContractsIntersectionUnionArticle10.1145/3276504openAccess