How to Evaluate Blame for Gradual Types by Lazarek, Greenman, Felleisen, Dimoulas, ICFP 2021 #19
Description
How to evaluate blame for gradual types
Lukas Lazarek, Ben Greenman, Matthias Felleisen, Christos Dimoulas
ICFP 2021
Abstract
Programming language theoreticians develop blame assignment systems and prove blame theorems for gradually typed programming languages. Practical implementations of gradual typing almost completely ignore the idea of blame assignment. This contrast raises the question whether blame provides any value to the working programmer and poses the challenge of how to evaluate the effectiveness of blame assignment strategies. This paper contributes (1) the first evaluation method for blame assignment strategies and (2) the results from applying it to three different semantics for gradual typing. These results cast doubt on the theoretical effectiveness of blame in gradual typing. In most scenarios, strategies with imprecise blame assignment are as helpful to a rationally acting programmer as strategies with provably correct blame.
Why are you interested in it or why should it be a good idea?
This article is about programming language pragmatics, i.e. the study of a programming language in context, using the rational programmer method. It is applied to gradual typing. See also the Rational Programmer: Investigating Programming Language Pragmatics for an overview of the rational programmer and How to evaluate blame for gradual types, Part 2 for the follow-up article.