Abstract
We propose a novel approach to constraint-based type inference based on coinductive logic. Constraint generation corresponds to translation into a conjunction of Horn clauses P, and constraint satisfaction is defined in terms of the coinductive Herbrand model of P. We illustrate the approach by formally defining this translation for a small object-oriented language similar to Featherweight Java, where type annotations in field and method declarations can be omitted.
In this way, we obtain a very precise type inference and provide new insights into the challenging problem of type inference for object-oriented programs. Since the approach is deliberately declarative, we define in fact a formal specification for a general class of algorithms, which can be a useful road map to researchers.
Furthermore, despite we consider here a particular language, the methodology could be used in general for providing abstract specifications of type inference for different kinds of programming languages.
This work has been partially supported by MIUR EOS DUE - Extensible Object Systems for Dynamic and Unpredictable Environments.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agesen, O.: The cartesian product algorithm. In: Olthoff, W. (ed.) ECOOP 1995. LNCS, vol. 952, pp. 2–26. Springer, Heidelberg (1995)
Amadio, R., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Ancona, D., Ancona, M., Cuni, A., Matsakis, N.: RPython: a Step Towards Reconciling Dynamically and Statically Typed OO Languages. In: OOPSLA 2007 Proceedings and Companion, DLS 2007: Proceedings of the 2007 Symposium on Dynamic Languages, pp. 53–64. ACM, New York (2007)
Ancona, D., Lagorio, G.: Type systems for object-oriented languages based on coinductive logic. Technical report, DISI - Univ. of Genova (2008) (submitted for publication)
Ancona, D., Damiani, F., Drossopoulou, S., Zucca, E.: Polymorphic bytecode: Compositional compilation for Java-like languages. In: ACM Symp. on Principles of Programming Languages 2005, January 2005. ACM Press, New York (2005)
Ancona, D., Lagorio, G., Zucca, E.: True separate compilation of Java classes. In: PPDP 2002 - Principles and Practice of Declarative Programming, pp. 189–200. ACM Press, New York (2002)
Ancona, D., Lagorio, G., Zucca, E.: Type inference for polymorphic methods in Java-like languages. In: Italiano, G.F., Moggi, E., Laura, L. (eds.) ICTCS 2007 - 10th Italian Conf. on Theoretical Computer Science 2003, eProceedings. World Scientific, Singapore (2007)
Ancona, D., Lagorio, G., Zucca, E.: Type inference for Java-like programs by coinductive logic programming. Technical report, Dipartimento di Informatica e Scienze dell’Informazione, Università di Genova (2008)
Ancona, D., Zucca, E.: Principal typings for Java-like languages. In: ACM Symp. on Principles of Programming Languages 2004, pp. 306–317. ACM Press, New York (2004)
Barbanera, F., Dezani-Cincaglini, M., de’Liguoro, U.: Intersection and union types: Syntax and semantics. Information and Computation 119(2), 202–230 (1995)
Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 63–81. Springer, Heidelberg (1997)
Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundam. Inform. 33(4), 309–338 (1998)
Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169 (1983)
Furr, M., An, J., Foster, J.S., Hicks, M.: Static type inference for Ruby. In: SAC 2009: Proceedings of the 2009 ACM symposium on Applied computing. ACM Press, New York (to appear, 2009)
Igarashi, A., Nagira, H.: Union types for object-oriented programming. Journ. of Object Technology 6(2), 47–68 (2007)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23(3), 396–450 (2001)
Lagorio, G., Zucca, E.: Just: safe unknown types in java-like languages. Journ. of Object Technology 6(2), 69–98 (2007); special issue: OOPS track at SAC 2006
Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: Extending logic programming with coinduction. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 472–483. Springer, Heidelberg (2007)
Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive logic programming. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 330–345. Springer, Heidelberg (2006)
Wang, T., Smith, S.: Polymorphic constraint-based type inference for objects. Technical report, The Johns Hopkins University (2008) (submitted for publication)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ancona, D., Lagorio, G., Zucca, E. (2009). Type Inference by Coinductive Logic Programming . In: Berardi, S., Damiani, F., de’Liguoro, U. (eds) Types for Proofs and Programs. TYPES 2008. Lecture Notes in Computer Science, vol 5497. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02444-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-02444-3_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02443-6
Online ISBN: 978-3-642-02444-3
eBook Packages: Computer ScienceComputer Science (R0)