Syntactic Type Polymorphism for Recursive Function Definitions

. Higher-order programming languages, such as ML, permit a flexible programming style by using compile-time type inference together with the concept of type polymorphism, which allows to specify the types of generic functions. In ML, however, recursive functions must always be given a unique (monomorphic) type inside their definition. Giving polymorphic types to recursive functions is known as the problem of polymorphic recursion which has been shown equivalent to the problem of semi-unification, known as undecidable. We show that the absence of a decidable specification to give polymorphic types for recursive definitions lies on the non-adequacy of representing type polymorphism by using type variables as primitive elements. We introduce the notion of syntactic type polymorphism to relate polymorphic types with syntactic information. We formulate a decidable calculus which gives polymorphic types to recursive functions in ML. We present an inference algorithm which we prove the term..