Heuristics-based Type Error Diagnosis for Haskell: The case of GADTs and local reasoning

Joris Burgers, Jurriaan Hage, Alejandro Serrano

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationIFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages
EditorsOlaf Chitil
PublisherAssociation for Computing Machinery
Pages33-43
Number of pages11
ISBN (Print)9781450389631
DOIs
Publication statusPublished - 2 Sep 2020
Event32nd Symposium on Implementation and Application of Functional Languages 2020 - Virtual, Online, United Kingdom
Duration: 2 Sep 20204 Sep 2020

Conference

Conference32nd Symposium on Implementation and Application of Functional Languages 2020
Abbreviated titleIFL 2020
Country/TerritoryUnited Kingdom
CityVirtual, Online
Period2/09/204/09/20

Keywords

  • generalized algebraic data types
  • Haskell
  • type error diagnosis
  • type graphs

Fingerprint

Dive into the research topics of 'Heuristics-based Type Error Diagnosis for Haskell: The case of GADTs and local reasoning'. Together they form a unique fingerprint.

Cite this