Abstract
A fundamental aspect of object-oriented languages is how recursive functions are defined. One semantic approach is to use simple record types and explicit recursion (i.e. fix) to define mutually recursive units of functionality. Another approach is to use records and recursive types to describe recursion through a “self” parameter. Many systems rely on both semantic approaches as well as combinations of universally quantified types, existentially quantified types, and mixin operators to encode patterns of method reuse, data encapsulation, and “open recursion” through self. These more complex mechanisms are needed to support many important use cases, but they often lack desirable theoretical properties, such as decidability, and can be difficult to implement, because of the equirecursive interpretation that identifies mu-types with their unfoldings. Furthermore, these systems do not apply to languages without explicit recursion (such as JavaScript, Python, and Ruby). In this paper, we present a statically typed calculus of functional objects called ISOLATE that can reason about a pattern of mixin composition without relying on an explicit fixpoint operation. To accomplish this, ISOLATE extends a standard isorecursive type system with a mechanism for checking the “mutual consistency” of a collection of functions, that is, that all of the assumptions about self are implied by the collection itself. We prove the soundness of ISOLATE via a type-preserving translation to a calculus with F-bounded polymorphism. Therefore, ISOLATE can be regarded as a stylized subset of the more expressive calculus that admits an interesting class of programs yet is easy to implement. In the future, we plan to investigate how other, more complicated forms of mixin composition (again, without explicit recursion) may be supported by lightweight type systems.
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
Ancona, D., Zucca, E.: A Calculus of Module Systems. Journal of Functional Programming (JFP) (2002)
Baldan, P., Ghelli, G., Raffaetà, A.: Basic Theory of F-bounded Quantification. Information and Computation (1999)
Boudol, G.: The Recursive Record Semantics of Objects Revisited. Journal of Functional Programming (JFP) (2004)
Bracha, G.: The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance. PhD thesis, University of Utah (1992)
Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing Object Encodings. Information and Computation (1999)
Canning, P., Cook, W., Hill, W., Olthoff, W., Mitchell, J.C.: F-bounded Polymorphism for Object-oriented Programming. In: Functional Programming Languages and Architecture (FPCA) (1989)
Cardelli, L.: A Semantics of Multiple Inheritance. In: Plotkin, G., MacQueen, D.B., Kahn, G. (eds.) Semantics of Data Types 1984. LNCS, vol. 173, pp. 51–67. Springer, Heidelberg (1984)
Cardelli, L.: Amber. In: Cousineau, G., Curien, P.-L., Robinet, B. (eds.) LITP 1985. LNCS, vol. 242, pp. 21–47. Springer, Heidelberg (1986)
Cardelli, L., Wegner, P.: On Understanding Types, Data Abstraction, and Polymorphism. Computing Surveys (1985)
Chugh, R.: IsoLate: A Type System for Self-Recursion, Extended Version (2015)
Damas, L., Milner, R.: Principal Type-Schemes for Functional Programs. In: Principles of Programming Languages (POPL) (1982)
Dreyer, D.: A Type System for Well-Founded Recursion. In: Principles of Programming Languages (POPL) (2004)
Dreyer, D.: A Type System for Recursive Modules. In: International Conference on Functional Programming (ICFP) (2007)
Duggan, D., Sourelis, C.: Mixin Modules. In: International Conference on Functional Programming, (ICFP) (1996)
Fisher, K., Reppy, J.: A Typed Calculus of Traits. In: Workshop on Foundations of Object-Oriented Programming (FOOL) (2004)
Ghelli, G.: Recursive Types Are Not Conservative Over Fsub. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 146–162. Springer, Heidelberg (1993)
Greenman, B., Muehlboeck, F., Tate, R.: Getting F-Bounded Polymorphism Back in Shape. In: Programming Language Design and Implementation (PLDI) (2014)
Gunter, C.A., Mitchell, J.C. (eds.): Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. MIT Press (1994)
Hirschowitz, T., Leroy, X.: Mixin Modules in a Call-by-Value Setting. In: ACM Transactions on Programming Languages and Systems (TOPLAS) (2005)
Igarashi, A., Viroli, M.: Variant Parametric Types: A Flexible Subtyping Scheme for Generics. In: ACM Transactions on Programming Languages and Systems (TOPLAS) (2006)
Im, H., Nakata, K., Garrigue, J., Park, S.: A Syntactic Type System for Recursive Modules. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) (2011)
Jim, T.: What Are Principal Typings and What Are They Good For? In: Principles of Programming Languages (POPL) (1996)
Kennedy, A.J., Pierce, B.C.: On Decidability of Nominal Subtyping with Variance, 2006. In: FOOL-WOOD (2007)
Leroy, X., Doligez, D., Frisch, A., Rémy, D., Vouillon, J.: OCaml System Release 4.02: Documentation and User’s Manual (2014), http://caml.inria.fr/pub/docs/manual-ocaml-4.02/
Mycroft, A.: Polymorphic Type Schemes and Recursive Definitions. In: Paul, M., Robinet, B. (eds.) Programming 1984. LNCS, vol. 167, pp. 217–228. Springer, Heidelberg (1984)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual Modal Type Theory. Transactions on Computational Logic (2008)
Petricek, T., Orchard, D., Mycroft Coeffects, A.: Coeffects: Unified Static Analysis of Context-Dependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 385–397. Springer, Heidelberg (2013)
Benjamin, C.: Pierce. Bounded Quantification is Undecidable. In: Principles of Programming Languages (POPL) (1992)
Pierce, B.C.: Types and Programming Languages. MIT Press (2002)
Pierce, B.C., Turner, D.N.: Simple Type-Theoretic Foundations for Object-Oriented Programming. Journal of Functional Programming (JFP) (1994)
Rémy, D., Vouillon, J.: Objective ML: A Simple Object-Oriented Extension of ML. In: Principles of Programming Languages (POPL) (1997)
Rossberg, A., Dreyer, D.: Mixin’ Up the ML Module System. In: ACM Transactions on Programming Languages and Systems (TOPLAS) (2013)
Russo, C.: Recursive Structures for Standard ML. In: International Conference on Functional Programming (ICFP) (2001)
Torgersen, M., Hansen, C.P., Ernst, E.: Adding Wildcards to the Java Programming Language. Journal of Object Technology (2004)
Wand, M.: Complete Type Inference for Simple Objects. In: Logic in Computer Science (LICS) (1987)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chugh, R. (2015). IsoLATE: A Type System for Self-recursion. In: Vitek, J. (eds) Programming Languages and Systems. ESOP 2015. Lecture Notes in Computer Science(), vol 9032. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46669-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-662-46669-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46668-1
Online ISBN: 978-3-662-46669-8
eBook Packages: Computer ScienceComputer Science (R0)