| Home > Publications > Reports > Informatics (CW) |
CW 507
Martin Sulzmann, Tom Schrijvers, Peter J. Stuckey
Type inference for GADTs via Herbrand constraint abduction
Abstract
Type inference for Hindley/Milner and variants is well understood as a constraint solving problem. Recent extensions to Hindley/Milner such as generalized algebraic data types (GADTs) force us to go beyond this approach to inference.
In this paper we show how to perform type inference for GADTs using Herbrand constraint abduction, a solving method to infer missing facts in terms of Herbrand constraints, i.e. conjunctions of type equations. But typeinference for GADTs is very hard, we are the first to give example programs with an infinite number of maximal types. We propose to rule out several kinds of ``non-intuitive'' solutions and show that we can construct in this way a complete and decidable type inference approach for GADTs and sketch how to support type error diagnosis. Our results point out new direction how to perform type inference for expressive type systems.
report.pdf (214K) / mailto: T. Schrijvers