Well-Typed Programs Can't Be Blamed

10 years 2 months ago
Well-Typed Programs Can't Be Blamed
We show how contracts with blame fit naturally with recent work on hybrid types and gradual types. Unlike hybrid types or gradual types, we require casts in the source code, in order to indicate where type errors may occur. Two (perhaps surprising) aspects of our approach are that refined types can provide useful static guarantees even in the absence of a theorem prover, and that type dynamic should not be regarded as a supertype of all other types. We factor the well-known notion of subtyping into new notions of positive and negative subtyping, and use these to characterise where positive and negative blame may arise. Our approach sharpens and clarifies some recent results in the literature.
Philip Wadler, Robert Bruce Findler
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where ESOP
Authors Philip Wadler, Robert Bruce Findler
Comments (0)