Abstract
Although theories of equivalence or subtyping for recursive types have been extensively investigated, sophisticated interaction between recursive types and abstract types has gained little attention. The key idea behind type theories for recursive types is to use syntactic contractiveness, meaning every μ-bound variable occurs only under a type constructor such as → or ∗. This syntactic contractiveness guarantees the existence of the unique solution of recursive equations and thus has been considered necessary for designing a sound theory for recursive types. However, in an advanced type system, such as OCaml, with recursive types, type parameters, and abstract types, we cannot easily define the syntactic contractiveness of types. In this paper, we investigate a sound type system for recursive types, type parameters, and abstract types. In particular, we develop a new semantic notion of contractiveness for types and signatures using mixed induction and coinduction, and show that our type system is sound with respect to the standard call-by-value operational semantics, which eliminates signature sealings. Moreover we show that while non-contractive types in signatures lead to unsoundness of the type system, they may be allowed in modules. We have also formalized the whole system and its type soundness proof in Coq.
An expanded version of this paper, containing detailed proofs and omitted definitions, and the Coq development are available at http://toccata.lri.fr/~im .
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
OCaml, http://caml.inria.fr/ocaml/
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
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)
Crary, K., Harper, R., Puri, S.: What is a recursive module? In: PLDI 1999 (1999)
Danielsson, N.A., Altenkirch, T.: Subtyping, declaratively: an exercise in mixed induction and coinduction. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 100–118. Springer, Heidelberg (2010)
Gapeyev, V., Levin, M.Y., Pierce, B.C.: Recursive subtyping revealed. Journal of Functional Programming 12(6), 511–548 (2002)
Im, H., Nakata, K., Garrigue, J., Park, S.: A syntactic type system for recursive modules. In: OOPSLA 2011 (2011)
Komendantsky, V.: Subtyping by folding an inductive relation into a coinductive one. In: Peña, R., Page, R. (eds.) TFP 2011. LNCS, vol. 7193, pp. 17–32. Springer, Heidelberg (2012)
MacQueen, D., Plotkin, G., Sethi, R.: An ideal model for recursive polymorphic types. In: POPL 1984 (1984)
Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic 51(1-2), 159–172 (1991)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press (1997)
Montagu, B.: Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types. PhD thesis, École Polytechnique, Palaiseau, France (December 2010)
Montagu, B., Rémy, D.: Modeling abstract types in modules with open existential types. In: POPL 2009 (2009)
Nakata, K., Uustalu, T.: Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: An exercise in mixed induction-coinduction. In: SOS 2010, pp. 57–75 (2010)
Rossberg, A., Dreyer, D.: Mixin’ up the ML module system. ACM Transactions on Programming Languages and Systems 35(1), 2:1–2:84 (2013)
Sénizergues, G.: The equivalence problem for deterministic pushdown automata is decidable. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 671–681. Springer, Heidelberg (1997)
Solomon, M.: Type definitions with parameters (extended abstract). In: POPL 1978 (1978)
Stone, C.A., Schoonmaker, A.P.: Equational theories with recursive types (2005), http://www.cs.hmc.edu/~stone/publications.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Im, H., Nakata, K., Park, S. (2013). Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds) Automata, Languages, and Programming. ICALP 2013. Lecture Notes in Computer Science, vol 7966. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39212-2_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-39212-2_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39211-5
Online ISBN: 978-3-642-39212-2
eBook Packages: Computer ScienceComputer Science (R0)