Type checking with open type functions

Tom Schrijvers; Simon Peyton Jones; Manual Chakravarty; Martin Sulzmann

doi:10.1145/1411204.1411215

Type checking with open type functions

Tom Schrijvers, Simon Peyton Jones, Manual Chakravarty, Martin Sulzmann

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.

Original language	English
Title of host publication	Proceeding of the 13th ACM SIGPLAN international conference on Functional programming
Publisher	Association for Computing Machinery
Publication date	2008
Pages	51-62
ISBN (Print)	978-1-59593-919-7
DOIs	https://doi.org/10.1145/1411204.1411215
Publication status	Published - 2008
Event	ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming - Victoria, British Columbia, Canada Duration: 22 Sept 2008 → 24 Sept 2008 Conference number: 13

Conference

Conference	ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming
Number	13
Country/Territory	Canada
City	Victoria, British Columbia
Period	22/09/2008 → 24/09/2008

Keywords

Haskell extensions
Type-level functions
Equality constraints
Entailment checking
GHC implementation

Access to Document

10.1145/1411204.1411215

Cite this

@inproceedings{1ef3c450f43c11dd9b71000ea68e967b,

title = "Type checking with open type functions",

abstract = "We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.",

keywords = "Haskell extensions, Type-level functions, Equality constraints, Entailment checking, GHC implementation, Haskell extensions, Type-level functions, Equality constraints, Entailment checking, GHC implementation",

author = "Tom Schrijvers and Jones, {Simon Peyton} and Manual Chakravarty and Martin Sulzmann",

year = "2008",

doi = "10.1145/1411204.1411215",

language = "English",

isbn = "978-1-59593-919-7",

pages = "51--62",

booktitle = "Proceeding of the 13th ACM SIGPLAN international conference on Functional programming",

publisher = "Association for Computing Machinery",

address = "United States",

note = "ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming ; Conference date: 22-09-2008 Through 24-09-2008",

}

Schrijvers, T, Jones, SP, Chakravarty, M & Sulzmann, M 2008, Type checking with open type functions. in Proceeding of the 13th ACM SIGPLAN international conference on Functional programming. Association for Computing Machinery, pp. 51-62, ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming, Victoria, British Columbia, Canada, 22/09/2008. https://doi.org/10.1145/1411204.1411215

Type checking with open type functions. / Schrijvers, Tom; Jones, Simon Peyton; Chakravarty, Manual et al.
Proceeding of the 13th ACM SIGPLAN international conference on Functional programming. Association for Computing Machinery, 2008. p. 51-62.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Type checking with open type functions

AU - Schrijvers, Tom

AU - Jones, Simon Peyton

AU - Chakravarty, Manual

AU - Sulzmann, Martin

N1 - Conference code: 13

PY - 2008

Y1 - 2008

N2 - We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.

AB - We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.

KW - Haskell extensions

KW - Type-level functions

KW - Equality constraints

KW - Entailment checking

KW - GHC implementation

KW - Haskell extensions

KW - Type-level functions

KW - Equality constraints

KW - Entailment checking

KW - GHC implementation

U2 - 10.1145/1411204.1411215

DO - 10.1145/1411204.1411215

M3 - Article in proceedings

SN - 978-1-59593-919-7

SP - 51

EP - 62

BT - Proceeding of the 13th ACM SIGPLAN international conference on Functional programming

PB - Association for Computing Machinery

T2 - ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming

Y2 - 22 September 2008 through 24 September 2008

ER -