Heuristics-based Type Error Diagnosis for Haskell: The case of GADTs and local reasoning
Abstract
Helium is a Haskell compiler designed to provide programmer friendly type error messages. It employs specially designed heuristics that work on a type graph representation of the type inference process.
In order to support existentials and Generalized Algebraic Data Types (GADTs) in Helium, we extend the type graphs of Helium with facilities for local reasoning. We have translated the original Helium heuristics to this new setting, and define a number of GADT-specific heuristics that help diagnose Helium programs that employ GADTs.
References
[1]
Joris Burgers. 2019. Type error diagnosis for OutsideIn(X) in Helium. https://dspace.library.uu.nl/handle/1874/382127.
[2]
Sheng Chen and Martin Erwig. 2014. Counter-factual Typing for Debugging Type Errors. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (POPL ’14). ACM, New York, NY, USA, 583–594. https://doi.org/10.1145/2535838.2535863
[3]
Olaf Chitil. 2001. Compositional Explanation of Types and Algorithmic Debugging of Type Errors. In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming(Florence, Italy) (ICFP ’01). ACM, New York, NY, USA, 193–204. https://doi.org/10.1145/507635.507659
[4]
Luis Damas and Robin Milner. 1982. Principal Type-schemes for Functional Programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Albuquerque, New Mexico) (POPL ’82). ACM, New York, NY, USA, 207–212. https://doi.org/10.1145/582153.582176
[5]
Martin Erwig. 2006. Visual Type Inference. J. Vis. Lang. Comput. 17, 2 (April 2006), 161–186. https://doi.org/10.1016/j.jvlc.2005.04.004
[6]
María García de la Banda, Peter J. Stuckey, and Jeremy Wazny. 2003. Finding All Minimal Unsatisfiable Subsets. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming (Uppsala, Sweden) (PPDP ’03). ACM, New York, NY, USA, 32–43.
[7]
Jurriaan Hage and Bastiaan Heeren. 2007. Heuristics for Type Error Discovery and Recovery. In Proceedings of the 18th International Conference on Implementation and Application of Functional Languages (Budapest, Hungary) (IFL’06). Springer-Verlag, Berlin, Heidelberg, 199–216. http://dl.acm.org/citation.cfm?id=1757028.1757040
[8]
Jurriaan Hage and Bastiaan Heeren. 2009. Strategies for Solving Constraints in Type and Effect Systems. Electron. Notes Theor. Comput. Sci. 236 (April 2009), 163–183. https://doi.org/10.1016/j.entcs.2009.03.021
[9]
Bastiaan Heeren, Jurriaan Hage, and S. Doaitse Swierstra. 2003. Constraint based type inferencing in Helium. In Workshop Proceedings of Immediate Applications of Constraint Programming, M.-C. Silaghi and M. Zanker (Eds.). Cork, 59 – 80.
[10]
Oukseh Lee and Kwangkeun Yi. 1998. Proofs About a Folklore Let-polymorphic Type Inference Algorithm. ACM Trans. Program. Lang. Syst. 20, 4 (July 1998), 707–723. https://doi.org/10.1145/291891.291892
[11]
Chuan-kai Lin and Tim Sheard. 2010. Pointwise Generalized Algebraic Data Types. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation (Madrid, Spain) (TLDI ’10). ACM, New York, NY, USA, 51–62. https://doi.org/10.1145/1708016.1708024
[12]
Zvonimir Pavlinovic, Tim King, and Thomas Wies. 2015. Practical SMT-based Type Error Localization. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). ACM, New York, NY, USA, 412–423. https://doi.org/10.1145/2784731.2784765
[13]
Falco Peijnenburg, Jurriaan Hage, and Alejandro Serrano. 2016. Type Directives and Type Graphs in Elm. In Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2016, Leuven, Belgium, August 31 - September 2, 2016. 2:1–2:12. https://doi.org/10.1145/3064899.3064907
[14]
Hubert Plociniczak. 2013. Scalad: An Interactive Type-level Debugger. In Proceedings of the 4th Workshop on Scala(Montpellier, France) (SCALA ’13). ACM, New York, NY, USA, Article 8, 4 pages. https://doi.org/10.1145/2489837.2489845
[15]
François Pottier and Didier Rémy. 2005. The Essence of ML Type Inference. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, Chapter 10, 389–489.
[16]
Vincent Rahli, Joe Wells, John Pirie, and Fairouz Kamareddine. 2017. Skalpel: A constraint-based type error slicer for Standard ML. J. Symb. Comput. 80, P1 (May 2017), 164–208. https://doi.org/10.1016/j.jsc.2016.07.013
[17]
Alejandro Serrano. 2018. Type Error Customization for Embedded Domain Specific Languages. Ph.D. Dissertation. Universiteit Utrecht, The Netherlands.
[18]
Alejandro Serrano and Jurriaan Hage. 2016. Type Error Diagnosis for Embedded DSLs by Two-Stage Specialized Type Rules. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632. Springer-Verlag New York, Inc., New York, NY, USA, 672–698. https://doi.org/10.1007/978-3-662-49498-1_26
[19]
Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded Impredicative Polymorphism. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA, USA) (PLDI 2018). ACM, New York, NY, USA, 783–796. https://doi.org/10.1145/3192366.3192389
[20]
Vincent Simonet and François Pottier. 2007. A Constraint-based Approach to Guarded Algebraic Data Types. ACM Trans. Program. Lang. Syst. 29, 1, Article 1 (Jan. 2007). https://doi.org/10.1145/1180475.1180476
[21]
Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. 2006. Type Processing by Constraint Reasoning. In Programming Languages and Systems, Naoki Kobayashi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–25.
[22]
Martin Sulzmann, Gregory J. Duck, Simon Peyton Jones, and Peter J. Stuckey. 2007. Understanding Functional Dependencies via Constraint Handling Rules. J. Funct. Program. 17, 1 (Jan. 2007), 83–129. https://doi.org/10.1017/S0956796806006137
[23]
Martin Sulzmann, Tom Schrijvers, and Peter J Stuckey. 2008. Type inference for GADTs via Herbrand constraint abduction. https://lirias.kuleuven.be/retrieve/10888
[24]
Kanae Tsushima and Kenichi Asai. 2013. An Embedded Type Debugger. In Implementation and Application of Functional Languages, Ralf Hinze (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 190–206.
[25]
Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(x): Modular Type Inference with Local Assumptions. J. Funct. Program. 21, 4-5 (Sept. 2011), 333–412. https://doi.org/10.1017/S0956796811000098
[26]
Jeroen Weijers, Jurriaan Hage, and Stefan Holdermans. 2014. Security type error diagnosis for higher-order, polymorphic languages. Science of Computer Programming 95 (2014), 200 – 218. https://doi.org/10.1016/j.scico.2014.03.011 Selected and extended papers from Partial Evaluation and Program Manipulation 2013.
[27]
Jun Yang, Greg Michaelson, Phil Trinder, and J. B. Wells. 2000. Improved Type Error Reporting. In In Proceedings of 12th International Workshop on Implementation of Functional Languages. 71–86.
[28]
Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton Jones. 2015. Diagnosing Type Errors with Class. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (Portland, OR, USA) (PLDI ’15). ACM, New York, NY, USA, 12–21. https://doi.org/10.1145/2737924.2738009
Recommendations
Type Directives and Type Graphs in Elm
IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming LanguagesWe introduce type graphs into Elm in order to improve type error messages for infinite types, and integrate type qualifiers (for type classes a la Haskell) and Elm's row polymorphism into type graphs. We also discuss how specialized type rules and ...
Type Class Instances for Type-Level Lambdas in Haskell
TFP 2015: Revised Selected Papers of the 16th International Symposium on Trends in Functional Programming - Volume 9547Haskell 2010 lacks flexibility in creating instances of type classes for type constructors with multiple type arguments. We would like to make the order of type arguments to a type constructor irrelevant to how type class instances can be specified. ...
Type invariants for Haskell
PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verificationMulti-parameter type classes, functional dependencies, and recently GADTs and open type families open up opportunities to use complex type-level programming to let GHC's type checker verify various properties of your programs. But type-level code is ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2020
161 pages
ISBN:9781450389631
DOI:10.1145/3462172
Copyright © 2020 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 23 July 2021
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
IFL 2020
IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages
September 2 - 4, 2020
Canterbury, United Kingdom
Acceptance Rates
Overall Acceptance Rate 19 of 36 submissions, 53%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 42Total Downloads
- Downloads (Last 12 months)12
- Downloads (Last 6 weeks)0
Reflects downloads up to 14 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in