Type checking with open type functions
- Tom Schrijvers,
- Simon Peyton Jones,
- Manual Chakravarty,
- Martin Sulzmann
- KU Leuven,
- Microsoft Research,
- University of New South Wales
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-review
Open access
Publication Information
Output type
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 51-62Publication milestones
- Published - 2008
Publication status
Published - 2008
Publisher
Association for Computing Machinery, United StatesISBN (Print)
978-1-59593-919-7Publication IDs
- Scopus: 59249097904
Host publication title
Proceeding of the 13th ACM SIGPLAN international conference on Functional programmingAbstract
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.
Publication metrics
PlumX, opens in new tab
Captures
57
Citations
113
Access to documents
Related Event
Title
ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming
Event type
ConferenceDate
22/09/2008 - 24/09/2008Location
Victoria, British ColumbiaCanada