A Proper Extension of ML with an Effective Type-Assignment

Abstract

We extend the functional language ML by allowing the recursive calls to a function F on the right-hand side of its definition to be at different types, all generic instances of the (derived) type of F on the left-hand side of its definition. The original definition of ML does not allow this feature. This extension does not produce new types beyond the usual universal polymorphic types of ML and satisfies the properties already enjoyed by ML: the principal-type property and the effective type-assignment property.