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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	Proceeding of the 13th ACM SIGPLAN international conference on Functional programming
Forlag	Association for Computing Machinery
Publikationsdato	2008
Sider	51-62
ISBN (Trykt)	978-1-59593-919-7
DOI	https://doi.org/10.1145/1411204.1411215
Status	Udgivet - 2008
Begivenhed	ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming - Victoria, British Columbia, Canada Varighed: 22 sep. 2008 → 24 sep. 2008 Konferencens nummer: 13

Konference

Konference	ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming
Nummer	13
Land/Område	Canada
By	Victoria, British Columbia
Periode	22/09/2008 → 24/09/2008

Emneord

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

Adgang til dokumentet

10.1145/1411204.1411215

Citationsformater

@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. i Proceeding of the 13th ACM SIGPLAN international conference on Functional programming. Association for Computing Machinery, s. 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. s. 51-62.

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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 -