Heuristics-based Type Error Diagnosis for Haskell: The case of GADTs and local reasoning
Publication date
2020-09-02
Authors
Burgers, Joris
Hage, Jurriaan
Serrano Mena, A.
Editors
Chitil, Olaf
Advisors
Supervisors
Document Type
Part of book
Metadata
Show full item recordCollections
License
taverne
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.
Keywords
generalized algebraic data types, Haskell, type error diagnosis, type graphs, Taverne, Human-Computer Interaction, Computer Networks and Communications, Computer Vision and Pattern Recognition, Software
Citation
Burgers, J, Hage, J & Serrano, A 2020, Heuristics-based Type Error Diagnosis for Haskell : The case of GADTs and local reasoning. in O Chitil (ed.), IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages. ACM International Conference Proceeding Series, Association for Computing Machinery, New York, pp. 33-43, 32nd Symposium on Implementation and Application of Functional Languages, IFL 2020, Virtual, Online, United Kingdom, 2/09/20. https://doi.org/10.1145/3462172.3462189, conference