Eric L. Seidel
Ranjit Jhala
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 the above 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 88% of the programs, and our reduction graph yields small counterexamples for 81% of the witnesses. 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.
- M. Bayne, R. Cook, and M. D. Ernst. Always-available static and dynamic feedback. In Proceedings of the 33rd International Conference on Software Engineering, ICSE ’11, pages 521–530, New York, NY, USA, 21 May 2011. ACM. ISBN 9781450304450. doi: 10.1145/ 1985793.1985864. Google Scholar
Digital Library
- C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, pages 209–224, Berkeley, CA, USA, 2008. USENIX Association. Google ScholarDigital Library
- H. R. Chamarthi, P. C. Dillinger, M. Kaufmann, and P. Manolios. Integrating testing and interactive theorem proving. In Proceedings of the 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 ’11, pages 4–19, 2011. doi: 10.4204/EPTCS. 70.1.Google ScholarCross Ref
- S. Chen and M. Erwig. Counter-factual typing for debugging type errors. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pages 583– 594, New York, NY, USA, 2014. ACM. ISBN 9781450325448. Google ScholarDigital Library
- doi: 10.1145/2535838.2535863.Google Scholar
- D. R. Christiansen. Reflect on your mistakes! lightweight domainspecific error messages. In Preproceedings of the 15th Symposium on Trends in Functional Programming, 2014.Google Scholar
- K. Claessen and J. Hughes. QuickCheck: A lightweight tool for random testing of haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP ’00, pages 268–279, New York, NY, USA, 2000. ACM. ISBN 9781581132021. Google ScholarDigital Library
- doi: 10.1145/351240.351266.Google Scholar
- C. Csallner and Y. Smaragdakis. JCrasher: an automatic robustness tester for java. Softw. Pract. Exp., 34(11):1025–1050, 1 Sept. 2004. ISSN 0038-0644. doi: 10.1002/spe.602. Google ScholarDigital Library
- L. Damas and R. Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’82, pages 207–212, New York, NY, USA, 1982. ACM. ISBN 9780897910651. Google ScholarDigital Library
- doi: 10.1145/582153.582176.Google Scholar
- M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. The MIT Press, 1st edition, 2009. ISBN 9780262062756. Google ScholarDigital Library
- C. Flanagan, M. Flatt, S. Krishnamurthi, S. Weirich, and M. Felleisen. Catching bugs in the web of program invariants. In Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation, PLDI ’96, pages 23–32, New York, NY, USA, 1996. ACM. ISBN 0-89791-795-2. doi: 10.1145/231379. Google ScholarDigital Library
- 231387.Google Scholar
- J. L. Fleiss. Measuring nominal scale agreement among many raters. Psychol. Bull., 76(5):378, Nov. 1971. ISSN 0033-2909, 1939-1455.Google ScholarCross Ref
- doi: 10.1037/h0031619.Google Scholar
- H. Gast. Explaining ML type errors by data flows. In Implementation and Application of Functional Languages, Lecture Notes in Computer Science, pages 72–89. Springer Berlin Heidelberg, 8 Sept. 2004. ISBN 9783540260943, 9783540320388. doi: 10.1007/11431664_5. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’05, pages 213–223, New York, NY, USA, 2005. ACM. ISBN 9781595930569. Google ScholarDigital Library
- doi: 10.1145/1065010.1065036.Google Scholar
- C. Haack and J. B. Wells. Type error slicing in implicitly typed Higher-Order languages. In Programming Languages and Systems, Lecture Notes in Computer Science, pages 284–301. Springer Berlin Heidelberg, 7 Apr. 2003. ISBN 9783540008866, 9783540365754. Google ScholarDigital Library
- doi: 10.1007/3-540-36575-3_20.Google Scholar
- J. Hage and B. Heeren. Heuristics for type error discovery and recovery. In Implementation and Application of Functional Languages, Lecture Notes in Computer Science, pages 199–216. Springer Berlin Heidelberg, 4 Sept. 2006. ISBN 9783540741299, 9783540741305. Google ScholarDigital Library
- doi: 10.1007/978-3-540-74130-5_12.Google Scholar
- B. Heeren, J. Hage, and S. D. Swierstra. Scripting the type inference process. In Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, volume 38, pages 3–13. ACM, 25 Aug. 2003. ISBN 9781581137569. doi: 10.1145/944705. Google ScholarDigital Library
- 944707.Google Scholar
- K. Krippendorff. Content Analysis: An Introduction to Its Methodology. SAGE Publications, 2012. ISBN 9781412983150.Google Scholar
- J. R. Landis and G. G. Koch. The measurement of observer agreement for categorical data. Biometrics, 33(1):159–174, Mar. 1977. ISSN 0006-341X.Google ScholarCross Ref
- O. Lee and K. Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Trans. Program. Lang. Syst., 20(4):707–723, July 1998. ISSN 0164-0925. doi: 10.1145/291891.291892. Google ScholarDigital Library
- B. Lerner, D. Grossman, and C. Chambers. Seminal: Searching for ML type-error messages. In Proceedings of the 2006 Workshop on ML, ML ’06, pages 63–73, New York, NY, USA, 2006. ACM. ISBN 9781595934833. doi: 10.1145/1159876.1159887. Google ScholarDigital Library
- B. S. Lerner, M. Flower, D. Grossman, and C. Chambers. Searching for type-error messages. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07, pages 425–434, New York, NY, USA, 2007. ACM. ISBN 9781595936332. doi: 10.1145/1250734.1250783. Google ScholarDigital Library
- F. Lindblad. Property directed generation of First-Order test data. In M. T. Morazán, editor, Proceedings of the Eighth Symposium on Trends in Functional Programming, volume 8 of TFP ’07, pages 105–123, 2007. ISBN 9781841501963.Google Scholar
- G. Marceau, K. Fisler, and S. Krishnamurthi. Measuring the effectiveness of error messages designed for novice programmers. In Proceedings of the 42Nd ACM Technical Symposium on Computer Science Education, SIGCSE ’11, pages 499–504, New York, NY, USA, 2011. Google ScholarDigital Library
- ACM. ISBN 9781450305006. doi: 10.1145/1953163.1953308.Google Scholar
- G. Marceau, K. Fisler, and S. Krishnamurthi. Mind your language: On novices’ interactions with error messages. In Proceedings of the 10th SIGPLAN Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2011, pages 3–18, New York, NY, USA, 2011. ACM. ISBN 9781450309417. Google ScholarDigital Library
- doi: 10.1145/2048237.2048241.Google Scholar
- B. J. McAdam. On the unification of substitutions in type inference. In K. Hammond, T. Davie, and C. Clack, editors, Implementation of Functional Languages, Lecture Notes in Computer Science, pages 137– 152. Springer Berlin Heidelberg, 9 Sept. 1998. ISBN 9783540662297, 9783540485155. doi: 10.1007/3-540-48515-5_9. Google ScholarDigital Library
- M. Naylor and C. Runciman. Finding inputs that reach a target expression. In Seventh IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM ’07, pages 133–142, 2007. doi: 10.1109/SCAM.2007.30. Google ScholarDigital Library
- M. Neubauer and P. Thiemann. Discriminative sum types locate the source of type errors. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP ’03, pages 15–26, New York, NY, USA, 2003. ACM. ISBN 9781581137569. Google ScholarDigital Library
- doi: 10.1145/944705.944708.Google Scholar
- C. Pacheco, S. K. Lahiri, M. D. Ernst, and T. Ball. Feedback-Directed random test generation. In 29th International Conference on Software Engineering, ICSE ’07, pages 75–84, 2007. doi: 10.1109/ICSE. 2007.37. Google ScholarDigital Library
- Z. Pavlinovic, T. King, and T. Wies. Finding minimum type error sources. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’14, pages 525–542, New York, NY, USA, 2014. ACM. ISBN 9781450325851. doi: 10.1145/2660193.2660230. Google ScholarDigital Library
- Z. Pavlinovic, T. King, and T. Wies. Practical SMT-based type error localization. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 412– 423, New York, NY, USA, 2015. ACM. ISBN 9781450336697. Google ScholarDigital Library
- doi: 10.1145/2784731.2784765.Google Scholar
- R. Perera, U. A. Acar, J. Cheney, and P. B. Levy. Functional programs that explain their work. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP ’12, pages 365–376, New York, NY, USA, 2012. ACM. ISBN 9781450310543. Google ScholarDigital Library
- doi: 10.1145/2364527.2364579.Google Scholar
- V. Rahli, J. Wells, J. Pirie, and F. Kamareddine. Skalpel: A type error slicer for standard ML. Electron. Notes Theor. Comput. Sci., 312: 197–213, 24 Apr. 2015. ISSN 1571-0661. doi: 10.1016/j.entcs. 2015.04.012. Google ScholarDigital Library
- C. Runciman, M. Naylor, and F. Lindblad. Smallcheck and lazy smallcheck: Automatic exhaustive testing for small values. In Proceedings of the First ACM SIGPLAN Symposium on Haskell, Haskell ’08, pages 37–48, New York, NY, USA, 2008. ACM. ISBN 9781605580647. Google ScholarDigital Library
- doi: 10.1145/1411286.1411292.Google Scholar
- K. Sagonas, J. Silva, and S. Tamarit. Precise explanation of success typing errors. In Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM ’13, pages 33–42, New York, NY, USA, 2013. ACM. ISBN 9781450318426. Google ScholarDigital Library
- doi: 10.1145/2426890.2426897.Google Scholar
- T. Schilling. Constraint-Free type error slicing. In Trends in Functional Programming, Lecture Notes in Computer Science, pages 1–16. Springer Berlin Heidelberg, 16 May 2011. ISBN 9783642320361, 9783642320378. doi: 10.1007/978-3-642-32037-8_1. Google ScholarDigital Library
- E. L. Seidel, N. Vazou, and R. Jhala. Type targeted testing. In Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems, ESOP ’15, pages 812–836, New York, NY, USA, 2015. Springer-Verlag New York, Inc. ISBN 978-3-662-46668-1. doi: 10.1007/978-3-662-46669-8_33. Google ScholarDigital Library
- E. L. Seidel, R. Jhala, and W. Weimer. Dynamic witnesses for static type errors, June 2016.Google Scholar
- 07557.Google Scholar
- A. Serrano and J. Hage. Type error diagnosis for embedded DSLs by Two-Stage specialized type rules. In Programming Languages and Systems, Lecture Notes in Computer Science, pages 672–698. Springer Berlin Heidelberg, 3 Apr. 2016. ISBN 9783662494974, 9783662494981. doi: 10.1007/978-3-662-49498-1_26.Google Scholar
- N. Tillmann and J. de Halleux. Pex–White box test generation for .NET. In B. Beckert and R. Hähnle, editors, Tests and Proofs, Lecture Notes in Computer Science, pages 134–153. Springer Berlin Heidelberg, 2008. ISBN 9783540791232. doi: 10.1007/978-3-540-79124-9_ 10. Google ScholarDigital Library
- D. Vytiniotis, S. Peyton Jones, and J. P. Magalhães. Equality proofs and deferred type errors: A compiler pearl. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP ’12, pages 341–352, New York, NY, USA, 2012. ACM. ISBN 9781450310543. doi: 10.1145/2364527.2364554. Google ScholarDigital Library
- D. Zhang and A. C. Myers. Toward general diagnosis of static errors. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pages 569– 581, New York, NY, USA, 2014. ACM. ISBN 9781450325448. Google ScholarDigital Library
- doi: 10.1145/2535838.2535870.Google Scholar
- D. Zhang, A. C. Myers, D. Vytiniotis, and S. Peyton-Jones. Diagnosing type errors with class. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pages 12–21, New York, NY, USA, 2015. ACM. ISBN 9781450334686. doi: 10.1145/2737924.2738009. Google ScholarDigital Library
Index Terms
- Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)
Recommendations
Finding minimum type error sources
OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & ApplicationsAutomatic type inference is a popular feature of functional programming languages. If a program cannot be typed, the compiler typically reports a single program location in its error message. This location is the point where the type inference failed, ...
Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)
ICFP '16Static 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, ...
Discriminative sum types locate the source of type errors
We propose a type system for locating the source of type errors in an applied lambda calculus with ML-style polymorphism. The system is based on discriminative sum types---known from work on soft typing---with annotation subtyping and recursive types. ...
Comments