dc.contributor.author | Williams, Jack | |
dc.contributor.author | Morris, J. Garrett | |
dc.contributor.author | Wadler, Philip | |
dc.date.accessioned | 2018-10-26T20:03:24Z | |
dc.date.available | 2018-10-26T20:03:24Z | |
dc.date.issued | 2018-11 | |
dc.identifier.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 | en_US |
dc.identifier.uri | http://hdl.handle.net/1808/27076 | |
dc.description.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. | en_US |
dc.publisher | Association for Computing Machinery | en_US |
dc.rights | © 2018 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License. | en_US |
dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | en_US |
dc.subject | Functional languages | en_US |
dc.subject | Semantics | en_US |
dc.subject | Theory of computation | en_US |
dc.subject | Program semantics | en_US |
dc.subject | Software and its engineering | en_US |
dc.subject | Gradual typing | en_US |
dc.subject | Blame | en_US |
dc.subject | Contracts | en_US |
dc.subject | Intersection | en_US |
dc.subject | Union | en_US |
dc.title | The Root Cause of Blame: Contracts for Intersection and Union Types | en_US |
dc.type | Article | en_US |
kusw.kuauthor | Morris, J. Garrett | |
kusw.kudepartment | Electrical Engineering & Computer Science | en_US |
dc.identifier.doi | 10.1145/3276504 | en_US |
kusw.oaversion | Scholarly/refereed, publisher version | en_US |
kusw.oapolicy | This item meets KU Open Access policy criteria. | en_US |
dc.rights.accessrights | openAccess | en_US |