TY - JOUR UR - http://lib.ugent.be/catalog/pug01:1202271 ID - pug01:1202271 LA - eng TI - OUTSIDEIN(X): modular type inference with local assumptions PY - 2011 JO - (2011) JOURNAL OF FUNCTIONAL PROGRAMMING SN - 0956-7968 PB - 2011 AU - Vytiniotis, Dimitrios AU - Peyton Jones, Simon AU - Schrijvers, Tom UGent 802000842623 AU - Sulzmann, Martin AB - 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. ER -Download RIS file
00000nam^a2200301^i^4500 | |||
001 | 1202271 | ||
005 | 20180823080020.0 | ||
008 | 110405s2011------------------------eng-- | ||
022 | a 0956-7968 | ||
024 | a 000295538000002 2 wos | ||
024 | a 1854/LU-1202271 2 handle | ||
024 | a 10.1017/S0956796811000098 2 doi | ||
040 | a UGent | ||
245 | a OUTSIDEIN(X): modular type inference with local assumptions | ||
260 | c 2011 | ||
520 | a 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. | ||
598 | a A1 | ||
700 | a Vytiniotis, Dimitrios | ||
700 | a Peyton Jones, Simon | ||
700 | a Schrijvers, Tom u UGent 0 802000842623 0 975595201789 9 2E6C35CC-F0EE-11E1-A9DE-61C894A0A6B4 | ||
700 | a Sulzmann, Martin | ||
650 | a Science General | ||
653 | a type system | ||
653 | a type inference | ||
653 | a local assumtions | ||
653 | a type classes | ||
653 | a GADTs | ||
653 | a type families | ||
653 | a Haskell | ||
653 | a CONSTRAINT HANDLING RULES | ||
653 | a CONGRUENCE CLOSURE | ||
773 | t JOURNAL OF FUNCTIONAL PROGRAMMING g J. Funct. Program. 2011. 21 (4-5) p.333-412 q 21:4-5<333 | ||
856 | 3 Full Text u https://biblio.ugent.be/publication/1202271/file/1933147 z [ugent] y jfp-outsidein.pdf | ||
920 | a article | ||
Z30 | x WE 1 WE02 | ||
922 | a UGENT-WE |
All data below are available with an Open Data Commons Open Database License. You are free to copy, distribute and use the database; to produce works from the database; to modify, transform and build upon the database. As long as you attribute the data sets to the source, publish your adapted database with ODbL license, and keep the dataset open (don't use technical measures such as DRM to restrict access to the database).
The datasets are also available as weekly exports.