Principal Typing And Mutual Recursion

Lucilia Figueiredo and Carlos Camarão

In Proc. of the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001) , Report No. 2017, University of Kiel

Abstract

As pointed out by Damas[Damas84],the Damas-Milner system (ML) has principal types, but not principal typings. Damas also defined in his thesis a slightly modified version of ML, which we call ML', which given a typing context and an expression, derives exactly the same types, and provided an algorithm (named as T) that infers principal typings for ML'. This work extends each of ML' and T with a new rule for typing mutually recursive let-bindings. The proposed rule can type more expressions than the corresponding rule used in ML, by allowing mutually recursive definitions to be used polymorphically by other definitions.