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

Joris Burgers; Jurriaan Hage; Alejandro Serrano

doi:10.1145/3462172.3462189

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 proceeding › Conference 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 language	English
Title of host publication	IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages
Editors	Olaf Chitil
Publisher	Association for Computing Machinery
Pages	33-43
Number of pages	11
ISBN (Print)	9781450389631
DOIs	https://doi.org/10.1145/3462172.3462189
Publication status	Published - 2 Sept 2020
Event	32nd Symposium on Implementation and Application of Functional Languages 2020 - Virtual, Online, United Kingdom Duration: 2 Sept 2020 → 4 Sept 2020

Conference

Conference	32nd Symposium on Implementation and Application of Functional Languages 2020
Abbreviated title	IFL 2020
Country/Territory	United Kingdom
City	Virtual, Online
Period	2/09/20 → 4/09/20

Keywords

generalized algebraic data types
Haskell
type error diagnosis
type graphs

Access to Document

10.1145/3462172.3462189

Cite this

@inproceedings{bb211458b6c74174894aeda6beee2c2e,

title = "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.",

keywords = "generalized algebraic data types, Haskell, type error diagnosis, type graphs",

author = "Joris Burgers and Jurriaan Hage and Alejandro Serrano",

year = "2020",

month = sep,

day = "2",

doi = "10.1145/3462172.3462189",

language = "English",

isbn = "9781450389631",

pages = "33--43",

editor = "Olaf Chitil",

booktitle = "IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages",

publisher = "Association for Computing Machinery",

address = "United States",

note = "32nd Symposium on Implementation and Application of Functional Languages 2020, IFL 2020 ; Conference date: 02-09-2020 Through 04-09-2020",

}

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. Association for Computing Machinery, pp. 33-43, 32nd Symposium on Implementation and Application of Functional Languages 2020, Virtual, Online, United Kingdom, 2/09/20. https://doi.org/10.1145/3462172.3462189

Heuristics-based Type Error Diagnosis for Haskell: The case of GADTs and local reasoning. / Burgers, Joris; Hage, Jurriaan; Serrano, Alejandro.
IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages. ed. / Olaf Chitil. Association for Computing Machinery, 2020. p. 33-43.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Heuristics-based Type Error Diagnosis for Haskell

T2 - 32nd Symposium on Implementation and Application of Functional Languages 2020

AU - Burgers, Joris

AU - Hage, Jurriaan

AU - Serrano, Alejandro

PY - 2020/9/2

Y1 - 2020/9/2

N2 - 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.

AB - 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.

KW - generalized algebraic data types

KW - Haskell

KW - type error diagnosis

KW - type graphs

U2 - 10.1145/3462172.3462189

DO - 10.1145/3462172.3462189

M3 - Conference contribution

SN - 9781450389631

SP - 33

EP - 43

BT - IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages

A2 - Chitil, Olaf

PB - Association for Computing Machinery

Y2 - 2 September 2020 through 4 September 2020

ER -

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

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this