Document Open Access Logo

Blame Tracking and Type Error Debugging

Authors Sheng Chen, John Peter Campora III

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2019.2.pdf
  • Filesize: 0.51 MB
  • 14 pages

Document Identifiers

Author Details

Sheng Chen
  • University of Louisiana at Lafayette, USA
John Peter Campora III
  • University of Louisiana at Lafayette, USA

Funding

This work is partially supported by the NSF grant CCF-1750886.

Cite As Get BibTex

Sheng Chen and John Peter Campora III. Blame Tracking and Type Error Debugging. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.SNAPL.2019.2

Abstract

In this work, we present an unexpected connection between gradual typing and type error debugging. Namely, we illustrate that gradual typing provides a natural way to defer type errors in statically ill-typed programs, providing more feedback than traditional approaches to deferring type errors. When evaluating expressions that lead to runtime type errors, the usefulness of the feedback depends on blame tracking, the defacto approach to locating the cause of such runtime type errors. Unfortunately, blame tracking suffers from the bias problem for type error localization in languages with type inference. We illustrate and formalize the bias problem for blame tracking, present ideas for adapting existing type error debugging techniques to combat this bias, and outline further challenges.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
Keywords
  • Blame tracking
  • type error debugging
  • gradual typing
  • type inference

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for All. SIGPLAN Not., 46(1):201-214, January 2011. URL: http://dx.doi.org/10.1145/1925844.1926409.
  2. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for Free for Free: Parametricity, with and Without Types. Proc. ACM Program. Lang., 1(ICFP):39:1-39:28, August 2017. URL: http://dx.doi.org/10.1145/3110283.
  3. Gavin Bierman, Erik Meijer, and Mads Torgersen. Adding Dynamic Types to C♯. In Theo D'Hondt, editor, ECOOP 2010 - Object-Oriented Programming, pages 76-100, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  4. John Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. Migrating Gradual Types. In Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '18, New York, NY, USA, 2018. ACM. Google Scholar
  5. John Peter Campora, Sheng Chen, and Eric Walkingshaw. Casts and Costs: Harmonizing Safety and Performance in Gradual Typing. Proc. ACM Program. Lang., 2(ICFP):98:1-98:30, July 2018. URL: http://dx.doi.org/10.1145/3236793.
  6. Giuseppe Castagna and Victor Lanvin. Gradual Typing with Union and Intersection Types. In ACM SIGPLAN International Conference on Functional Programming, ICFP 2017, 2017. To appear. Google Scholar
  7. Christopher Chambers, Sheng Chen, Duc Le, and Christopher Scaffidi. The function, and dysfunction, of information sources in learning functional programming. Journal of Computing Sciences in Colleges, 28(1):220-226, 2012. Google Scholar
  8. Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. Fast and Precise Type Checking for JavaScript. Proc. ACM Program. Lang., 1(OOPSLA):48:1-48:30, October 2017. URL: http://dx.doi.org/10.1145/3133872.
  9. S. Chen and M. Erwig. Guided Type Debugging. In Int. Symp. on Functional and Logic Programming, LNCS 8475, pages 35-51, 2014. Google Scholar
  10. Sheng Chen and Martin 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. URL: http://dx.doi.org/10.1145/2535838.2535863.
  11. Sheng Chen and Martin Erwig. Systematic identification and communication of type errors. Journal of Functional Programming, 28:e2, 2018. URL: http://dx.doi.org/10.1017/S095679681700020X.
  12. Sheng Chen, Martin Erwig, and Karl Smeltzer. Exploiting diversity in type checkers for better error messages. Journal of Visual Languages & Computing, 39:10-21, 2017. Special Issue on Programming and Modelling Tools. URL: http://dx.doi.org/10.1016/j.jvlc.2016.07.001.
  13. Olaf Chitil. Compositional Explanation of Types and Algorithmic Debugging of Type Errors. In ACM Int. Conf. on Functional Programming, pages 193-204, September 2001. Google Scholar
  14. Hyunjun Eo, Oukseh Lee, and Kwangkeun Yi. Proofs of a set of hybrid let-polymorphic type inference algorithms. New Generation Computing, 22(1):1-36, 2004. URL: http://dx.doi.org/10.1007/BF03037279.
  15. Robert Bruce Findler and Matthias Felleisen. Contracts for Higher-order Functions. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP '02, pages 48-59, New York, NY, USA, 2002. ACM. URL: http://dx.doi.org/10.1145/581478.581484.
  16. Ronald Garcia and Matteo Cimini. Principal Type Schemes for Gradual Programs. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 303-315, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2676726.2676992.
  17. Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. In European Symposium on Programming, pages 284-301, 2003. Google Scholar
  18. Jurriaan Hage and Bastiaan Heeren. Heuristics for Type Error Discovery and Recovery. In Implementation and Application of Functional Languages, pages 199-216. Springer, 2007. Google Scholar
  19. Jurriaan Hage and Peter Van Keeken. Mining for Helium. Technical report UU-CS, 2006. Google Scholar
  20. Bastiaan Heeren, Daan Leijen, and Arjan van IJzendoorn. Helium, for learning Haskell. In Proceedings of the 2003 ACM SIGPLAN workshop on Haskell, Haskell '03, pages 62-71, New York, NY, USA, 2003. ACM. URL: http://dx.doi.org/10.1145/871895.871902.
  21. Bastiaan J. Heeren. Top Quality Type Error Messages. PhD thesis, Universiteit Utrecht, The Netherlands, September 2005. URL: http://www.cs.uu.nl/people/bastiaan/phdthesis.
  22. Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. On Polymorphic Gradual Typing. Proc. ACM Program. Lang., 1(ICFP):40:1-40:29, August 2017. URL: http://dx.doi.org/10.1145/3110284.
  23. Lintaro Ina and Atsushi Igarashi. Gradual Typing for Generics. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '11, pages 609-624, New York, NY, USA, 2011. ACM. URL: http://dx.doi.org/10.1145/2048066.2048114.
  24. Gregory F. Johnson and Janet A. Walz. A maximum-flow approach to anomaly isolation in unification-based incremental type inference. In ACM Symp. on Principles of Programming Languages, pages 44-57, 1986. URL: http://dx.doi.org/10.1145/512644.512649.
  25. Oukseh Lee and Kwangkeun Yi. A Generalized Let-Polymorphic Type Inference Algorithm. Technical report, Technical Memorandum ROPAS-2000-5, Research on Program Analysis System, Korea Advanced Institute of Science and Technology, 2000. Google Scholar
  26. B. Lerner, M. Flower, Dan Grossman, and Craig Chambers. Searching for type-error messages. In ACM Int. Conf. on Programming Language Design and Implementation, pages 425-434, 2007. URL: http://dx.doi.org/10.1145/1250734.1250783.
  27. Calvin Loncaric, Satish Chandra, Cole Schlesinger, and Manu Sridharan. A Practical Framework for Type Inference Error Explanation. In OOPSLA, pages 781-799, 2016. Google Scholar
  28. Bruce J. McAdam. How to repair type errors automatically. In Kevin Hammond and Sharon Curtis, editors, Selected papers from the 3rd Scottish Functional Programming Workshop (SFP01), University of Stirling, Bridge of Allan, Scotland, August 22nd to 24th, 2001, volume 3 of Trends in Functional Programming, pages 87-98. Intellect, 2001. Google Scholar
  29. Bruce J McAdam. Reporting Type Errors in Functional Programs. PhD thesis, Larboratory for Foundations of Computer Science, The University of Edinburgh, 2002. Google Scholar
  30. Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi. Dynamic Type Inference for Gradual Hindley-Milner Typing. Proc. ACM Program. Lang., 3(POPL):18:1-18:29, January 2019. URL: http://dx.doi.org/10.1145/3290331.
  31. Fabian Muehlboeck and Ross Tate. Sound Gradual Typing is Nominally Alive and Well. In OOPSLA, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3133880.
  32. Matthias Neubauer and Peter Thiemann. Discriminative sum types locate the source of type errors. In ACM Int. Conf. on Functional Programming, pages 15-26, 2003. URL: http://dx.doi.org/10.1145/944705.944708.
  33. Zvonimir Pavlinovic, Tim King, and Thomas Wies. Finding Minimum Type Error Sources. In OOPSLA, pages 525-542, 2014. Google Scholar
  34. Zvonimir Pavlinovic, Tim King, and Thomas Wies. Practical SMT-based Type Error Localization. In ICFP, pages 412-423, 2015. Google Scholar
  35. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  36. Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. The Ins and Outs of Gradual Type Inference. SIGPLAN Not., 47(1):481-494, January 2012. URL: http://dx.doi.org/10.1145/2103621.2103714.
  37. Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, and Panagiotis Vekris. Safe & Efficient Gradual Typing for TypeScript. In POPL, 2015. Google Scholar
  38. Baishakhi Ray, Daryl Posnett, Vladimir Filkov, and Premkumar Devanbu. A Large Scale Study of Programming Languages and Code Quality in Github. In Proceedings of the 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2014, pages 155-165, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2635868.2635922.
  39. J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1):23-41, January 1965. URL: http://dx.doi.org/10.1145/321250.321253.
  40. Thomas Schilling. Constraint-Free type error slicing. In Trends in Functional Programming, pages 1-16. Springer, 2012. Google Scholar
  41. Eric L. Seidel, Ranjit Jhala, and Westley Weimer. Dynamic Witnesses for Static Type Errors. In ACM SIGPLAN International Conference on Functional Programming, 2016. to appear. Google Scholar
  42. Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, and Ranjit Jhala. Learning to Blame: Localizing Novice Type Errors with Data-driven Diagnosis. Proc. ACM Program. Lang., 1(OOPSLA):60:1-60:27, October 2017. URL: http://dx.doi.org/10.1145/3138818.
  43. Jeremy Siek, Peter Thiemann, and Philip Wadler. Blame and Coercion: Together Again for the First Time. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, pages 425-435, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2737924.2737968.
  44. Jeremy Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. Monotonic References for Efficient Gradual Typing. In In Proceedings of the 24th European Symposium on Programming (ESOP'15), volume 9032 of Lecture Notes in Computer Science, Berlin, Heidelberg, 2015. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_18.
  45. Jeremy G. Siek and Walid Taha. Gradual Typing for Functional Languages. In IN SCHEME AND FUNCTIONAL PROGRAMMING WORKSHOP, pages 81-92, 2006. Google Scholar
  46. Jeremy G. Siek and Manish Vachharajani. Gradual Typing with Unification-based Inference. In Proceedings of the 2008 Symposium on Dynamic Languages, DLS '08, pages 7:1-7:12, New York, NY, USA, 2008. ACM. URL: http://dx.doi.org/10.1145/1408681.1408688.
  47. Jeremy G Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, volume 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  48. Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. Interactive type debugging in Haskell. In ACM SIGPLAN Workshop on Haskell, pages 72-83, 2003. URL: http://dx.doi.org/10.1145/871895.871903.
  49. Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. Improving type error diagnosis. In ACM SIGPLAN Workshop on Haskell, pages 80-91, 2004. URL: http://dx.doi.org/10.1145/1017472.1017486.
  50. F. Tip and T. B. Dinesh. A slicing-based approach for locating type errors. ACM Trans. on Software Engineering and Methodology, 10(1):5-55, January 2001. URL: http://dx.doi.org/10.1145/366378.366379.
  51. Ville Tirronen, SAMUEL UUSI-MÄKELÄ, and VILLE ISOMÖTTÖNEN. Understanding beginners' mistakes with Haskell. Journal of Functional Programming, 25:e11, 2015. Google Scholar
  52. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage Migration: From Scripts to Programs. In Companion to the 21st ACM SIGPLAN Symposium on Object-oriented Programming Systems, Languages, and Applications, OOPSLA '06, pages 964-974, New York, NY, USA, 2006. ACM. URL: http://dx.doi.org/10.1145/1176617.1176755.
  53. Sam Tobin-Hochstadt and Matthias Felleisen. The Design and Implementation of Typed Scheme. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pages 395-406, New York, NY, USA, 2008. ACM. URL: http://dx.doi.org/10.1145/1328438.1328486.
  54. Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory Typing: Ten Years Later. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages (SNAPL 2017), volume 71 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2017.17.
  55. Kanae Tsushima and Olaf Chitil. A Common Framework Using Expected Types for Several Type Debugging Approaches. In John P. Gallagher and Martin Sulzmann, editors, Functional and Logic Programming, pages 230-246, Cham, 2018. Springer International Publishing. Google Scholar
  56. Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi. The Behavior of Gradual Types: A User Study. In Proceedings of the 14th ACM SIGPLAN International Symposium on Dynamic Languages, DLS 2018, pages 1-12, New York, NY, USA, 2018. ACM. URL: http://dx.doi.org/10.1145/3276945.3276947.
  57. Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. Big Types in Little Runtime: Open-world Soundness and Collaborative Blame for Gradual Type Systems. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 762-774, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3009837.3009849.
  58. Dimitrios Vytiniotis, Simon Peyton Jones, and José Pedro 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, 2012. URL: http://dx.doi.org/10.1145/2364527.2364554.
  59. Dimitrios Vytiniotis, Simon Peyton jones, Tom Schrijvers, and Martin Sulzmann. Outsidein(x) modular type inference with local assumptions. J. Funct. Program., 21(4-5):333-412, September 2011. Google Scholar
  60. Philip Wadler. A Complement to Blame. In SNAPL, 2015. Google Scholar
  61. Philip Wadler and Robert Bruce Findler. Well-Typed Programs Can't Be Blamed. In Proceedings of the 18th European Symposium on Programming Languages and Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, ESOP '09, pages 1-16, Berlin, Heidelberg, 2009. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-00590-9_1.
  62. Mitchell Wand. Finding the source of type errors. In ACM Symp. on Principles of Programming Languages, pages 38-43, 1986. URL: http://dx.doi.org/10.1145/512644.512648.
  63. Jeremy Richard Wazny. Type inference and type error diagnosis for Hindley/Milner with extensions. PhD thesis, The University of Melbourne, January 2006. Google Scholar
  64. Baijun Wu, John Peter Campora III, and Sheng Chen. Learning User Friendly Type-error Messages. Proc. ACM Program. Lang., 1(OOPSLA):106:1-106:29, October 2017. URL: http://dx.doi.org/10.1145/3133930.
  65. Baijun Wu and Sheng Chen. How Type Errors Were Fixed and What Students Did? Proc. ACM Program. Lang., 1(OOPSLA):105:1-105:27, October 2017. URL: http://dx.doi.org/10.1145/3133929.
  66. Jun Yang. Improving Polymorphic Type Explanations. PhD thesis, Heriot-Watt University, May 2001. Google Scholar
  67. Danfeng Zhang and Andrew C. Myers. Toward General Diagnosis of Static Errors. In ACM Symp. on Principles of Programming Languages, pages 569-581, 2014. Google Scholar
  68. Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton-Jones. Diagnosing Type Errors with Class. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 12-21, 2015. Google Scholar
  69. Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton-Jones. SHErrLoc: A Static Holistic Error Locator. ACM Trans. Program. Lang. Syst., 39(4):18:1-18:47, August 2017. URL: http://dx.doi.org/10.1145/3121137.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact