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.

• Type: Conference
• Year: 2009
• Where: ESOP
• Authors: Philip Wadler, Robert Bruce Findler
• Keywords: ESOP 2009, Gradual Types, Hybrid Types, Programming Languages, Useful Static Guarantees