A Logical Algorithm for ML Type Inference

This paper gives a bottom-up logic programming formulation of the Hindley-Milner polymorphic type inference algorithm. We show that for programs of bounded order and arity the given algorithm runs in $O(nα(n) + dn)$ time where n is the length of the program, d is the "scheme depth" of the program, and $α$ is the inverse of Ackermann's function. It is argued that for practical programs d will not exceed 5 even for programs with hundreds of module layers. This formulation of the Hindley-Milner algorithm is intended as a case study in "logical algorithms", i.e., algorithms presented and analyzed as bottom-up inference rules.