Exploiting Type Annotations

Exploiting Type Annotations

• Atze Dijkstra, S. Doaitse Swierstra, 2007
• rejected by ESOP 2007
• Abstract: The Haskell type system has been designed in such a way that all allowed types can be inferred automatically; any explicit type specification only serves as a means of documentation and safeguarding. Consequently, a programmer is free to omit any type signature, and the program will still type check. The price to be paid for this convenience is limited expressiveness of the type system: even if a programmer is willing to explicitly provide higher-ranked types with polymorphic arguments, this is not allowed. In an effort to obtain the same expressiveness as System F, the use of universally quantified types on higher ranked positions in types in particular has received much attention in recent years. Because type inference for such types in general is not possible, much work has been done to investigate which limitations on higher ranked types still allow type inference. In this paper we explore an alternative, algorithmic, approach to this problem, which does not limit expressiveness: we propagate explicitly specified type information to all program locations where this information provides starting information for a standard Hindley-Milner type inference algorithm.

-- AtzeDijkstra - 21 Sep 2007