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
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