International Federation for Information Processing Working Group G2.1 - Algorithmic Languages and Calculi edition:62 location:Namur, Belgium date:11-15 December, 2006
One of the disadvantages of statically typed languages is the programming overhead caused by writing all the necessary type information: Both type declarations and type definitions are typically required. Traditional type
inference aims at relieving the programmer from the former.
We present a rule-based constraint rewriting algorithm that reconstructs both type declarations and type definitions, allowing the programmer to effectively program type-less in a strictly typed language. This effectively combines strong points of dynamically typed languages (rapid prototyping)
and statically typed ones (documentation, optimized compilation). Moreover it allows to quickly port code from a statically untyped to a statically typed setting.
Our constraint-based algorithm reconstructs uniform polymorphic definitions of algebraic data types and simultaneously infers the types of all expressions and
functions (supporting polymorphic recursion) in the program. The declarative nature of the algorithm allows us to easily show that it has a number of highly desirable properties such as soundness, completeness and various
optimality properties. Moreover, we show how to easily extend and adapt it to suit a number of different language constructs and type system features.