Fritz Henglein. Breaking through the $n^3$ barrier: Faster object type inference. In Proc.\ 4th Int'l Workshop on Foundations of Object-Oriented Languages (FOOL), Paris, France, Benjamin Pierce (ed.), Also DIKU TOPPS Report D-317, January 1997.
Download paper:
Adobe portable document (pdf)
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Abadi and Cardelli have presented and investigated object calculi that model most object-oriented features found in actual object-oriented programming languages. The calculi are innate object calculi in that they are \emph{not} based on $\lambda$-calculus. They present a series of type systems for their calculi, four of which are first-order. Palsberg has shown how typability in each one of these systems can be decided in time $O(n^3)$, where $n$ is the size of an untyped object expression, using an algorithm based on dynamic transitive closure. He also shows that each of the type inference problems is hard for polynomial time under log-space reductions. In this paper we show how we can break through the \emph{(dynamic) transitive closure bottleneck} and improve each one of the four type inference problems from $O(n^3)$ to the following time complexities: \begin{center} \begin{tabular}{|l|c|c|} \hline & no subtyping & subtyping \\ \hline w/o rec. types & $O(n)$ & $O(n^2)$ \\ with rec. types & $O(n \log^2 n)$ & $O(n^2)$ \\ \hline \end{tabular} \end{center} % Furthermore, for each of the four calculi we present a principal % typing characterization for typable object expression which can be % computed in the given times. The key ingredient that lets us ``beat'' the worst-case time complexity induced by using general dynamic transitive closure or similar algorithmic methods is that object subtyping is \emph{invariant}: an object type is a subtype of a ``shorter'' type with a subset of the field names if and only if the common fields have \emph{equal} types
[ Parametricity ] [ Dyntyp ]
@InProceedings{henglein97f,
Author = {Henglein, Fritz},
Title = {Breaking through the $n^3$ barrier: Faster object type inference},
BookTitle = {Proc.\ 4th Int'l Workshop on Foundations of Object-Oriented Languages (FOOL), Paris, France},
editor = {Pierce, Benjamin},
Month = {January},
Year = {1997}
}
Get EndNote Reference (.ref)