Ghent University Academic Bibliography

Advanced

OUTSIDEIN(X): modular type inference with local assumptions

Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers UGent and Martin Sulzmann (2011) JOURNAL OF FUNCTIONAL PROGRAMMING. 21(4-5). p.333-412
abstract
Advanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and - perhaps controversially - argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called OUTSIDEIN(X), is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. OUTSIDEIN(X) extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7.
Please use this url to cite or link to this publication:
author
organization
year
type
journalArticle (original)
publication status
published
subject
keyword
type system, type inference, local assumtions, type classes, GADTs, type families, Haskell, CONSTRAINT HANDLING RULES, CONGRUENCE CLOSURE
journal title
JOURNAL OF FUNCTIONAL PROGRAMMING
J. Funct. Program.
volume
21
issue
4-5
pages
333 - 412
Web of Science type
Article
Web of Science id
000295538000002
JCR category
COMPUTER SCIENCE, SOFTWARE ENGINEERING
JCR impact factor
0.878 (2011)
JCR rank
51/103 (2011)
JCR quartile
2 (2011)
ISSN
0956-7968
DOI
10.1017/S0956796811000098
language
English
UGent publication?
yes
classification
A1
copyright statement
I have transferred the copyright for this publication to the publisher
id
1202271
handle
http://hdl.handle.net/1854/LU-1202271
date created
2011-04-05 12:08:02
date last changed
2012-01-26 13:12:53
@article{1202271,
  abstract     = {Advanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and - perhaps controversially - argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called OUTSIDEIN(X), is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. OUTSIDEIN(X) extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7.},
  author       = {Vytiniotis, Dimitrios and Peyton Jones, Simon and Schrijvers, Tom and Sulzmann, Martin},
  issn         = {0956-7968},
  journal      = {JOURNAL OF FUNCTIONAL PROGRAMMING},
  keyword      = {type system,type inference,local assumtions,type classes,GADTs,type families,Haskell,CONSTRAINT HANDLING RULES,CONGRUENCE CLOSURE},
  language     = {eng},
  number       = {4-5},
  pages        = {333--412},
  title        = {OUTSIDEIN(X): modular type inference with local assumptions},
  url          = {http://dx.doi.org/10.1017/S0956796811000098},
  volume       = {21},
  year         = {2011},
}

Chicago
Vytiniotis, Dimitrios, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. “OUTSIDEIN(X): Modular Type Inference with Local Assumptions.” Journal of Functional Programming 21 (4-5): 333–412.
APA
Vytiniotis, D., Peyton Jones, S., Schrijvers, T., & Sulzmann, M. (2011). OUTSIDEIN(X): modular type inference with local assumptions. JOURNAL OF FUNCTIONAL PROGRAMMING, 21(4-5), 333–412.
Vancouver
1.
Vytiniotis D, Peyton Jones S, Schrijvers T, Sulzmann M. OUTSIDEIN(X): modular type inference with local assumptions. JOURNAL OF FUNCTIONAL PROGRAMMING. 2011;21(4-5):333–412.
MLA
Vytiniotis, Dimitrios, Simon Peyton Jones, Tom Schrijvers, et al. “OUTSIDEIN(X): Modular Type Inference with Local Assumptions.” JOURNAL OF FUNCTIONAL PROGRAMMING 21.4-5 (2011): 333–412. Print.