[Prev][Next][Index][Thread]
HindleyMilner type inference in pseudolinear time.

To: types@dcs.gla.ac.uk

Subject: HindleyMilner type inference in pseudolinear time.

From: David McAllester <dmac@research.att.com>

Date: Fri, 1 Nov 1996 10:59:06 0500 (EST)

Approved: types@dcs.gla.ac.uk
[ The Types Forum  http://www.dcs.gla.ac.uk/~types ]
The following paper contains, amoung other results, a proof that
HilndleyMilner type inference can be in pseudolinear 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 bottomup logic programs. The $O(n^3)$ running time of
the flow analysis is a corollary of this bottomup 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 HindleyMilner typability can be determined in
pseudolinear time, i.e., $O(n\alpha(n))$ where $\alpha$ is the
inverse Ackerman function. The last two results suggest that
letpolymorphism over simple types is fundamentally more tractable
than letpolymorphism over recursive types.
URL: http://www.ai.mit.edu/people/dam/rectypes.ps