{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:06:00Z","timestamp":1779836760509,"version":"3.53.1"},"reference-count":54,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2018,5,21]],"date-time":"2018-05-21T00:00:00Z","timestamp":1526860800000},"content-version":"unspecified","delay-in-days":140,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2018]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1017\/s0956796818000126","type":"journal-article","created":{"date-parts":[[2018,5,21]],"date-time":"2018-05-21T05:46:38Z","timestamp":1526881598000},"source":"Crossref","is-referenced-by-count":1,"title":["Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong)"],"prefix":"10.1017","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2529-7790","authenticated-orcid":false,"given":"ERIC L.","family":"SEIDEL","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"RANJIT","family":"JHALA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"WESTLEY","family":"WEIMER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2018,5,21]]},"reference":[{"key":"S0956796818000126_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36575-3_20"},{"key":"S0956796818000126_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159887"},{"key":"S0956796818000126_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_26"},{"key":"S0956796818000126_ref32","first-page":"137","volume-title":"Implementation of Functional Languages","author":"McAdam","year":"1998"},{"key":"S0956796818000126_ref53","doi-asserted-by":"crossref","unstructured":"Zhang D. & Myers A. C. (2014) Toward general diagnosis of static errors. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '14. New York, NY, USA: ACM, pp. 569\u2013581.","DOI":"10.1145\/2535838.2535870"},{"key":"S0956796818000126_ref40","doi-asserted-by":"crossref","unstructured":"Perera R. , Acar U. A. , Cheney J. & Levy P. B. (2012) Functional programs that explain their work. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, pp. 365\u2013376.","DOI":"10.1145\/2364527.2364579"},{"key":"S0956796818000126_ref44","first-page":"1","volume-title":"Trends in Functional Programming","author":"Schilling","year":"2011"},{"key":"S0956796818000126_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291892"},{"key":"S0956796818000126_ref31","doi-asserted-by":"crossref","unstructured":"Marceau G. , Fisler K. & Krishnamurthi S. (2011b) 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. New York, NY, USA: ACM, pp. 3\u201318.","DOI":"10.1145\/2048237.2048241"},{"key":"S0956796818000126_ref16","doi-asserted-by":"crossref","unstructured":"Guo P. J. (2013) Online Python Tutor: Embeddable web-based program visualization for CS education. In Proceedings of the 44th ACM Technical Symposium on Computer Science Education. SIGCSE '13. New York, NY, USA: ACM, pp. 579\u2013584.","DOI":"10.1145\/2445196.2445368"},{"key":"S0956796818000126_ref20","doi-asserted-by":"crossref","unstructured":"Heeren B. , Hage J. & Swierstra S. D. (2003) Scripting the type inference process. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming, vol. 38. ACM, pp. 3\u201313.","DOI":"10.1145\/944705.944707"},{"key":"S0956796818000126_ref6","unstructured":"Christiansen D. R. (2014) Reflect on your mistakes! lightweight domain-specific error messages. In Proceedings of the 15th Symposium on Trends in Functional Programming."},{"key":"S0956796818000126_ref33","unstructured":"Naylor M. & Runciman C. (2007) Finding inputs that reach a target expression. In Proceedings of the 7th IEEE International Working Conference on Source Code Analysis and Manipulation. pp. 133\u2013142."},{"key":"S0956796818000126_ref9","doi-asserted-by":"publisher","DOI":"10.1002\/spe.602"},{"key":"S0956796818000126_ref4","unstructured":"Chargu\u00e9raud A. (2014) Improving type error messages in ocaml. In Proceedings of the ML Family\/OCaml Users and Developers Workshops. Electronic Proceedings in Theoretical Computer Science, vol. 198. Open Publishing Association, pp. 80\u201397."},{"key":"S0956796818000126_ref39","doi-asserted-by":"crossref","unstructured":"Pavlinovic Z. , King T. & Wies T. (2015) Practical SMT-based type error localization. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, pp. 412\u2013423.","DOI":"10.1145\/2784731.2784765"},{"key":"S0956796818000126_ref11","volume-title":"Semantics Engineering with PLT Redex","author":"Felleisen","year":"2009"},{"key":"S0956796818000126_ref24","doi-asserted-by":"crossref","unstructured":"Lempsink E. (2009) Generic Type-Safe Diff and Patch for Families of Datatypes. M.Phil. thesis, Universiteit Utrecht.","DOI":"10.1145\/1596614.1596624"},{"key":"S0956796818000126_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_21"},{"key":"S0956796818000126_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.03.021"},{"key":"S0956796818000126_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426897"},{"key":"S0956796818000126_ref38","doi-asserted-by":"crossref","unstructured":"Pavlinovic Z. , King T. & Wies T. (2014) Finding minimum type error sources. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications. New York, NY, USA: ACM, pp. 525\u2013542.","DOI":"10.1145\/2660193.2660230"},{"key":"S0956796818000126_ref14","first-page":"72","volume-title":"Implementation and Application of Functional Languages","author":"Gast","year":"2004"},{"key":"S0956796818000126_ref18","first-page":"199","volume-title":"Implementation and Application of Functional Languages","author":"Hage","year":"2006"},{"key":"S0956796818000126_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231387"},{"key":"S0956796818000126_ref1","doi-asserted-by":"crossref","unstructured":"Bayne M. , Cook R. & Ernst M. D. (2011) Always-available static and dynamic feedback. In Proceedings of the 33rd International Conference on Software Engineering. ICSE '11. New York, NY, USA: ACM, pp. 521\u2013530.","DOI":"10.1145\/1985793.1985864"},{"key":"S0956796818000126_ref2","unstructured":"Cadar C. , Dunbar D. & Engler D. (2008) 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. Berkeley, CA, USA: USENIX Association, pp. 209\u2013224."},{"key":"S0956796818000126_ref3","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.70.1"},{"key":"S0956796818000126_ref5","doi-asserted-by":"crossref","unstructured":"Chen S. & Erwig M. (2014) Counter-factual typing for debugging type errors. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL. New York, NY, USA: ACM, pp. 583\u2013594.","DOI":"10.1145\/2535838.2535863"},{"key":"S0956796818000126_ref7","unstructured":"Claessen K. & Hughes J. (2000) QuickCheck: A lightweight tool for random testing of haskell programs. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, pp. 268\u2013279."},{"key":"S0956796818000126_ref10","unstructured":"Damas L & Milner R. (1982) Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 207\u2013212."},{"key":"S0956796818000126_ref13","doi-asserted-by":"publisher","DOI":"10.1037\/h0031619"},{"key":"S0956796818000126_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"S0956796818000126_ref21","volume-title":"Content Analysis: An Introduction to Its Methodology","author":"Krippendorff","year":"2012"},{"key":"S0956796818000126_ref22","doi-asserted-by":"publisher","DOI":"10.2307\/2529310"},{"key":"S0956796818000126_ref26","doi-asserted-by":"crossref","unstructured":"Lerner B. S. , Flower M. , Grossman D. & Chambers C. (2007) Searching for type-error messages. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, NY, USA: ACM, pp. 425\u2013434.","DOI":"10.1145\/1250734.1250783"},{"key":"S0956796818000126_ref27","unstructured":"Lindblad F. (2007) Property directed generation of first-order test data. In Proceedings of the Eighth Symposium on Trends in Functional Programming. Moraz\u00e1n M. T. (ed), vol. 8, pp. 105\u2013123."},{"key":"S0956796818000126_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983994"},{"key":"S0956796818000126_ref29","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177730491"},{"key":"S0956796818000126_ref30","doi-asserted-by":"crossref","unstructured":"Marceau G. , Fisler K. & Krishnamurthi S. (2011a) Measuring the effectiveness of error messages designed for novice programmers. In Proceedings of the 42Nd ACM Technical Symposium on Computer Science Education. New York, NY, USA: ACM, pp. 499\u2013504.","DOI":"10.1145\/1953163.1953308"},{"key":"S0956796818000126_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"S0956796818000126_ref35","unstructured":"Neubauer M. & Thiemann P. (2003) Discriminative sum types locate the source of type errors. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming. New York, NY, USA: ACM, pp. 15\u201326."},{"key":"S0956796818000126_ref36","unstructured":"Nguyen P. C , & Van Horn D. (2015) Relatively complete counterexamples for higher-order programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, NY, USA: ACM, pp. 446\u2013456."},{"key":"S0956796818000126_ref37","doi-asserted-by":"crossref","unstructured":"Pacheco C. , Lahiri S. K , Ernst M. D. & Ball T. (2007) Feedback-Directed random test generation. In Proceedings of the 29th International Conference on Software Engineering. ICSE '07, pp. 75\u201384.","DOI":"10.1109\/ICSE.2007.37"},{"key":"S0956796818000126_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.04.012"},{"key":"S0956796818000126_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"S0956796818000126_ref46","doi-asserted-by":"crossref","unstructured":"Seidel E. L. , Jhala R. & Weimer W. (2016a) Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong) In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 228\u2013242.","DOI":"10.1145\/3022670.2951915"},{"key":"S0956796818000126_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"S0956796818000126_ref49","unstructured":"Seven D. (2014 17 Apr.) Knightmare: A DevOps Cautionary Tale. https:\/\/dougseven.com\/2014\/04\/17\/knightmare-a-devops-cautionary-tale\/. Accessed: 2017-4-24."},{"key":"S0956796818000126_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"S0956796818000126_ref52","unstructured":"Wheeler D. A. (2014 23 Nov.) The apple goto fail vulnerability: lessons learned. https:\/\/www.dwheeler.com\/essays\/apple-goto-fail.html. Accessed: 2017-4-24."},{"key":"S0956796818000126_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738009"},{"key":"S0956796818000126_ref45","unstructured":"Seidel E. L. , Jhala R. & Weimer W. (2016b June) Dynamic Witnesses for Static Type Errors."},{"key":"S0956796818000126_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364554"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796818000126","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:46Z","timestamp":1779835006000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796818000126\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"references-count":54,"alternative-id":["S0956796818000126"],"URL":"https:\/\/doi.org\/10.1017\/s0956796818000126","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"article-number":"e13"}}