Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)

DOI10.1145/2951913.2951915zbMATH Open1361.68050arXiv1606.07557OpenAlexW2996075572WikidataQ130983799 ScholiaQ130983799MaRDI QIDQ2985773FDOQ2985773

Authors: Eric L. Seidel, Ranjit Jhala, Westley Weimer 

Publication date: 10 May 2017

Published in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Abstract: Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend this procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for around 85% of the programs, our reduction graph yields small counterexamples for over 80% of the witnesses, and a simple heuristic allows us to use witnesses to locate the source of type errors with around 70% accuracy. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message.

Full work available at URL: https://arxiv.org/abs/1606.07557

Recommendations

• Compositional explanation of types and algorithmic debugging of type errors
• Guided Type Debugging
• Systematic identification and communication of type errors
• Counter-factual typing for debugging type errors
• Explaining ML Type Errors by Data Flows

zbMATH Keywords

testingdebuggingtype errors

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cited In (5)

• Improving type error reporting for type classes
• Compositional explanation of types and algorithmic debugging of type errors
• Systematic identification and communication of type errors
• Explaining ML Type Errors by Data Flows
• Counter-factual typing for debugging type errors

This page was built for publication: Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2985773)