ITEM METADATA RECORD
Title: OUTSIDEIN(X) Modular type inference with local assumptions
Authors: Vytiniotis, Dimitrios ×
Jones, Simon Peyton
Schrijvers, Tom
Sulzmann, Martin #
Issue Date: 2011
Publisher: Cambridge University Press
Series Title: Journal of Functional Programming vol:21 pages: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 article,
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 also 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.
ISSN: 0956-7968
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Non-KU Leuven Association publications
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
jfp-outsidein.pdf Published 750KbAdobe PDFView/Open

 


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science