[Prev][Next][Index][Thread]

Hindley-Milner type inference in pseudo-linear time.


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]


The following paper contains, amoung other results, a proof that
Hilndley-Milner type inference can be in pseudo-linear time
for programs of bounded order and arity [O(n alpha(n)) where
alpha is the inverse of Ackerman's function].

TITLE: Inferring Recursive Data Types

AUTHOR: David McAllester (dmac@research.att.com)

ABSTRACT: This paper contains five results on the problem of inferring
types.  The first is that type inference over recursive types with
unions and data constructors can be done in cubic time using a flow
analysis.  The second is a general theorem characterizing the time
complexity of bottom-up logic programs.  The $O(n^3)$ running time of
the flow analysis is a corollary of this bottom-up run time theorem.
The third is that for shallow case statements typability by the
semantic types of Aiken, Wimmers and Lakshman is equivalent to
typability by recursive types and hence can be determined by flow
analysis.  The fourth is that, even for first order programs of arity
one, typability by recursive types is \mtt{PSPACE} hard for
polymorphic programs.  The final result is that for any fixed bound on
order and arity Hindley-Milner typability can be determined in
pseudo-linear time, i.e., $O(n\alpha(n))$ where $\alpha$ is the
inverse Ackerman function.  The last two results suggest that
let-polymorphism over simple types is fundamentally more tractable
than let-polymorphism over recursive types.

URL: http://www.ai.mit.edu/people/dam/rectypes.ps