Analytical and structural polymorphism expressed using patterns over types
Karl Fritz Ruehr · Deep Blue (University of Michigan) · 1992
Modem functional languages feature polymorphic types whose data structures must be fixed, though their component types may be generic; we present a new notion called analytical polymorphism which allows both data structures and their component types to be generic. Traditional polymorphism is expressed with universally-quantified variables ranging over types and is justified by the independence of a typing with respect to the quantified variable. Analytical polymorphism is expressed with universally-quantified variables ranging over both types and type functions and is justified instead by the recursive analysis of the forms of all admissible instantiations of these variables. We use pattern-matching to express the recursive analysis of types and type functions, following the traditional use of patterns in functional languages to express the recursive analysis of values of algebraic types. We develop analytical polymorphism first as a generalization of the standard higher-order lambda calculus: this explicitly-typed context more clearly exposes certain subtleties and provides a solid theoretical foundation for further study. The explicitly-typed calculus includes higher-order data structures and kind polymorphism, features which may be of independent interest. We next consider applications to realistic programming languages which feature first-order, implicit polymorphism and automated type inference. Fundamental limitations of unification, on which traditional type inference algorithms are based, force us to consider a restricted notion of structural polymorphism, in which quantified type function variables may only be instantiated to outermost occurrences of algebraic type constructors. We investigate two different approaches to structural polymorphism, one which adheres to a strict discipline of implicit typing and another which requires user-supplied type constraints, but only for structurally-polymorphic definitions. The purely implicit system suffers from a lack of principal typing and poses a difficult type inference problem (we suspect it is undecidable, though we have found no proof). The second system supports automatic type inference with only a modest extension of the traditional algorithm. Although both systems require a limited form of dynamic typing, we present experimental results which support our claim that the second system is both feasible and useful in practice.