Polymorphic algebraic data type reconstruction

One of the disadvantages of statically typed languages is the programmingoverhead caused by writing all the necessary type information: Both typedeclarations and type definitions are typically required. Traditional typeinference aims at relieving the programmer from the former.We present a rule-based constraint rewriting algorithm that reconstructs bothtype declarations and type definitions, allowing the programmer to effectivelyprogram type-less in a strictly typed language. This effectivelycombines strong points of dynamically typed languages (rapid prototyping)and statically typed ones (documentation, optimized compilation). Moreoverit allows to quickly port code from a statically untyped to a staticallytyped setting.Our constraint-based algorithm reconstructs uniform polymorphic definitions ofalgebraic data types and simultaneously infers the types of all expressions andfunctions (supporting polymorphic recursion) in the program. The declarativenature of the algorithm allows us to easily show that it has a number ofhighly desirable properties such as soundness, completeness and variousoptimality properties. Moreover, we show how to easily extend and adapt itto suit a number of different language constructs and type system features.status: publishe