POPL 08 takes place next week, so San Francisco will be flooded with an army of burly and menacing programming language researchers and type theorists. Kids, don’t say you haven’t been warned.
On Wednesday evening, January 9, Phil Wadler will be repeating for the public his talk “Well-typed programs canâ€™t be blamed”, based on joint work with Robby Findler. Here’s the abstract from their eponymous paper.
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.
If you’re a researcher attending POPL, you ought to come to Phil’s talk even if you’ve already seen it. It will be a great, and rare, opportunity to meet Silicon Valley hackers who use functional languages in startups and established companies.