Conjunctive polymorphic type checking with explicit types

An expressive type language and the ability to do compile-time type inference are desirable goals in language design, but the attainment of the former may preclude the possibility of the latter. Specifically, the type conjunction operator (type intersection) induces a rich type language at the expense of decidability of the typeable expressions. Two extreme alternatives to this dilemma are to abandon type inference (and force the programmer to, essentially, supply a derivation for his type claims) or to abandon (or restrict) type conjunction. This work presents a third alternative in which the programmer, at times, may be required to supply explicit types in order for type inference to succeed. In this way, the power of conjunctive types is preserved, yet compile-time type inference can be done for a large class of polymorphic functions, including those typeable with parametric types.

To this end, we introduce a simple combinator based language with typing rules based on type conjunction and a subtype relation, of sorts, called "weaker." The validity of the type rules with respect to the usual interpretation of "type" is shown, along with the undecidability of the type relation. It is shown how the computational portion of the language can be modified to accommodate explicit type information which may direct an automatic type derivation. This new language has the principal type property with respect to a decidable relation, although deciding this relation is shown to be an NP-Complete problem. The language is extended to accommodate type fixed points, and extended further to allow all expressions with parametric types to be typed automatically, and to accommodate integers, pairs, sums, and abstract types in the form of type generators.