Polymorphic algebraic data type reconstruction

One of the disadvantages of statically typed languages is the pro-gramming overhead caused by writing all the necessary type infor-mation: Both type declarations and type definitions are typically required. Traditional type inference aims at relieving the program-mer from the former. We present a rule-based constraint rewriting algorithm that re-constructs 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 (doc-umentation, optimized compilation). Moreover it allows to quickly port code from a statically untyped to a statically typed setting. Our constraint-based algorithm reconstructs uniform polymor-phic 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