Abstract
We consider the problem of type reconstruction for A-terms over a type system with recursive types and atomic subsumptions. This problem reduces to the problem of solving a finite set of inequalities over infinite trees. We show how to solve such inequalities by reduction to an infinite but well-structured set of inequalities over the base types. This infinite set of inequalities is solved using Büchi automata. The resulting algorithm is in DEXPTIME. This also improves the previous NEXPTIME upper bound for type reconstruction for finite types with atomic subtyping. We show that the key steps in the algorithm are PSPACE-hard.
This work was partly supported by NSF giants CCR-9002253 and CCR-9113196 and by Polish KBN grant No. 2 1192 91 01.
Work supported by the National Science Foundation under grants CCR-9002253 and CCR-9014603.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Roberto M. Amadio and Luca Cardelli. Subtyping Recursive Types. In Conf. Rec. 18th ACM Symposium on Principles of Programming Languages, pages 104–118, 1991.
Kim B. Bruce. A Paradigmatic Object-Oriented Programming Language: Design, Static Typing and Semantics. Technical Report CS-92-01, Williams College, January 1992.
William R. Cook, Walter L. Hill, and Peter S. Canning. Subtyping is not Inheritance. In Conf. Rec. 17th ACM Symposium on Principles of Programming Languages, pages 125–135, 1990.
Bruno Courcelle. Fundamental Properties of Infinite Trees. Theoretical Computer Science, 25:95–109, 1983.
Y.-C. Full and P. Mishra. Type Inference with Subtypes. In Proceedings European Symposium on Programming, pages 94–114, 1988.
Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient Inference of Partial Types. Technical Report DAIMI PB-394, Computer Science Department, Aarhus University, April 1992.
Patrick Lincoln and John C. Mitchell. Algorithmic Aspects of Type Inference with Subtypes. In Conf. Rec. 19th ACM Symposium on Principles of Programming Languages, pages 293–304, 1992.
John C. Mitchell. Coercion and Type Inference (summary). In Conf. Rec. 11th ACM Symposium on Principles of Programming Languages, pages 175–185, 1984.
John C. Mitchell. Type Inference with Simple Subtypes. Journal of Functional Programming, 1:245–285, 1991.
Patrick M. O'Keefe and Mitchell Wand. Type Inference for Partial Types is Decidable. In Bernd Krieg-Brückner, editor, European Symposium on Programming '92, volume 582 of Springer Lecture Notes in Computer Science, pages 408–17. Springer-Verlag, 1992.
Vaughn Pratt and Jerzy Tiuryn. Satisfiability of Inequalities in a Poset. to appear, 1992.
Michael O. Rabin. Weakly Definable Relations and Special Automata. In Y. BarHillel, editor, Mathematical Logic and the Foundations of Set Theory, pages 1–23, Amsterdam, 1970. North-Holland.
Satish Thatle. Type Inference with Partial Types. In Proceedings International Colloquium on Automata, Languages, and Programming '88, pages 615–29, 1988.
Jerzy Tiuryn. Subtype Inequalities. In Proc. 7th IEEE Symposium on Logic in Computer Science, pages 308–15, 1992.
Moshe Y. Vardi and Pierre Wolper. Automata-Theoretic techniques for modal logics of programs. J. Comp. Sys. Sci., 32:183–221, 1986.
Mitchell Wand. A Simple Algorithm and Proof for Type Inference. Fundamenta Informaticae, 10:115–122, 1987.
Mitchell Wand and. Patrick M. O'Keefe. On the Complexity of Type Inference with Coercion. In Conf. on Functional Programming Languages and Computer Architecture, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tiuryn, J., Wand, M. (1993). Type reconstruction with recursive types and atomic subtyping. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_98
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_98
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive