Conjunctive polymorphic type checking on a language of combinators

A typed language of combinators based on the type conjunction operator is defined and shown to be semantically sound. The undecidability of type checking can be overcome through the use of explicit user-supplied types at regular parts of an expression. Explicit types need only be given for expressions which themselves are not a functional application and which are applied to one or more subexpressions. This language has the `principal type property´, i.e. all typeable expressions have a principal type. A type checking algorithm for the simple language is given. Extensions to the language are discussed, including MacQueen´s (1984) type fixed-point operator and default explicit types. With default explicit types, type checking can proceed (via extended unification) when explicit types are omitted; thus, combinators which can be typed in the parametric type system of Milner (1978) need not be explicitly typed