Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

A Calculus with Recursive Types, Record Concatenation and Subtyping

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 13658))

Included in the following conference series:

  • 300Accesses

Abstract

Calculi with subtyping, a form of record concatenation and recursive types are useful to model objects with multiple inheritance. Surprisingly, almost no existing calculi supports the three features together, partly because the combination of subtyping and record concatenation is already known to be troublesome. Recently, a line of work ondisjoint intersection types with amerge operator has emerged as a new approach to deal with the interaction between subtyping and record concatenation. However, the addition of recursive types has not been studied.

In this paper we present a calculus that combinesiso-recursive types with disjoint intersection types and a merge operator. The merge operator generalizes symmetric record concatenation, and the calculus supports subtyping as well as recursive types. We build on recent developments on the theory of iso-recursive subtyping using the so-callednominal unfolding rules to add iso-recursive types to a calculus with disjoint intersection types and a merge operator. The main challenge lies in the disjointness definition with iso-recursive subtyping. We show the type soundness of the calculus, decidability of subtyping, as well as the soundness and completeness of our disjointness definition. All the proofs are mechanized in the Coq theorem prover.

This is a preview of subscription content,log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 7435
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 9294
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide -see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Similar content being viewed by others

Notes

  1. 1.

    We assume the presence of recursive functions, and that records are lazy in the example.

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Springer, New York (1996).https://doi.org/10.1007/978-1-4419-8598-9

    Book MATH  Google Scholar 

  2. Alpuim, J., Oliveira, B.C.S., Shi, Z.: Disjoint polymorphism. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 1–28. Springer, Heidelberg (2017).https://doi.org/10.1007/978-3-662-54434-1_1

    Chapter  Google Scholar 

  3. Amin, N., Rompf, T., Odersky, M.: Foundations of path-dependent types. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications. OOPSLA 2014. Association for Computing Machinery (2014)

    Google Scholar 

  4. Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symb. Logic48(4), 931–940 (1983)

    Article MathSciNet MATH  Google Scholar 

  5. Bi, X., Oliveira, B.C.d.S.: Typed first-class traits. In: 32nd European Conference on Object-Oriented Programming (ECOOP 2018) (2018)

    Google Scholar 

  6. Bi, X., Oliveira, B.C.d.S., Schrijvers, T.: The essence of nested composition. In: 32nd European Conference on Object-Oriented Programming (ECOOP 2018) (2018)

    Google Scholar 

  7. Bi, X., Xie, N., Oliveira, B.C.S., Schrijvers, T.: Distributive disjoint polymorphism for compositional programming. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 381–409. Springer, Cham (2019).https://doi.org/10.1007/978-3-030-17184-1_14

    Chapter  Google Scholar 

  8. Bierman, G., Abadi, M., Torgersen, M.: Understanding typescript. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 257–281. Springer, Heidelberg (2014).https://doi.org/10.1007/978-3-662-44202-9_11

    Chapter  Google Scholar 

  9. Bruce, K., Cardeli, L., Castagna, G., Group, T.H.O., Leavens, G.T., Pierce, B.: On binary methods. Theory Pract. Object Syst.1(3) (1996)

    Google Scholar 

  10. Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing object encodings155(1/2), 108–133 (1999).http://www.cis.upenn.edu/bcpierce/papers/compobj.ps

  11. Cardelli, L.: A semantics of multiple inheritance. In: Semantics of Data Types (1984)

    Google Scholar 

  12. Cardelli, L.: Amber. In: Cousineau, G., Curien, P.-L., Robinet, B. (eds.) LITP 1985. LNCS, vol. 242, pp. 21–47. Springer, Heidelberg (1986).https://doi.org/10.1007/3-540-17184-3_38

    Chapter  Google Scholar 

  13. Cardelli, L.: Extensible Records in a Pure Calculus of Subtyping. Digital, Systems Research Center (1992)

    Google Scholar 

  14. Cardelli, L.: A language with distributed scope. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1995, pp. 286–297 (1995)

    Google Scholar 

  15. Cardelli, L., Mitchell, J.C.: Operations on records. Math. Struct. Comput. Sci.1(1), 3–48 (1991)

    Article MathSciNet MATH  Google Scholar 

  16. Castagna, G., Frisch, A.: A gentle introduction to semantic subtyping. In: Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 198–199 (2005)

    Google Scholar 

  17. Compagnoni, A.B., Pierce, B.C.: Higher-order intersection types and multiple inheritance. Math. Struct. Comput. Sci. (MSCS)6(5), 469–501 (1996)

    Article MathSciNet MATH  Google Scholar 

  18. Cook, W.R., Hill, W., Canning, P.S.: Inheritance is not subtyping. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1990, pp. 125–135 (1989)

    Google Scholar 

  19. Cook, W.R., Palsberg, J.: A denotational semantics of inheritance and its correctness. In: Object-Oriented Programming: Systems, Languages and Applications (OOPSLA) (1989)

    Google Scholar 

  20. Damm, F.M.: Subtyping with union types, intersection types and recursive types. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 687–706. Springer, Heidelberg (1994).https://doi.org/10.1007/3-540-57887-0_121

    Chapter  Google Scholar 

  21. Davies, R., Pfenning, F.: Intersection types and computational effects. In: International Conference on Functional Programming (ICFP) (2000)

    Google Scholar 

  22. Dunfield, J.: Elaborating intersection and union types. J. Funct. Program.24(2–3), 133–165 (2014)

    Article MathSciNet MATH  Google Scholar 

  23. Ernst, E.: Family polymorphism. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 303–326. Springer, Heidelberg (2001).https://doi.org/10.1007/3-540-45337-7_17

    Chapter  Google Scholar 

  24. Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 137–146. IEEE (2002)

    Google Scholar 

  25. Giarrusso, P.G., Stefanesco, L., Timany, A., Birkedal, L., Krebbers, R.: Scala step-by-step: soundness for dot with step-indexed logical relations in iris. Proc. ACM Program. Lang.4(ICFP) (2020)

    Google Scholar 

  26. Glew, N.: An efficient class and object encoding. In: Proceedings of the 15th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA 2000, pp. 311–324. Association for Computing Machinery (2000)

    Google Scholar 

  27. Hu, J.Z., Lhoták, O.: Undecidability of DSUB and its decidable fragments. Proc. ACM Program. Lang.4(POPL), 1–30 (2019)

    Google Scholar 

  28. Huang, X., Oliveira, B.C.d.S.: A type-directed operational semantics for a calculus with a merge operator. In: 34th European Conference on Object-Oriented Programming (ECOOP 2020), vol. 166 (2020).https://doi.org/10.4230/LIPIcs.ECOOP.2020.26

  29. Huang, X., Zhao, J., Oliveira, B.C.d.S.: Taming the merge operator: a type-directed operational semantics approach. J. Funct. Program. (2021)

    Google Scholar 

  30. Jones, T., Pearce, D.J.: A mechanical soundness proof for subtyping over recursive types. In: Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, pp. 1–6 (2016)

    Google Scholar 

  31. Mackay, J., Potanin, A., Aldrich, J., Groves, L.: Decidable subtyping for path dependent types. Proc. ACM Program. Lang.4(POPL), 1–27 (2019)

    Google Scholar 

  32. Microsoft: Typescript (2021).https://www.typescriptlang.org/

  33. Oliveira, B.C.d.S., Shi, Z., Alpuim, J.: Disjoint intersection types. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, pp. 364–377 (2016)

    Google Scholar 

  34. Palsberg, J., Zhao, T.: Type inference for record concatenation and subtyping. Inf. Comput.189(1) (2004)

    Google Scholar 

  35. Pearce, D.J.: Rewriting for sound and complete union, intersection and negation types. ACM SIGPLAN Not.52(12), 117–130 (2017)

    Article  Google Scholar 

  36. Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238–248. Springer, Cham (2013).https://doi.org/10.1007/978-3-319-02654-1_13

    Chapter  Google Scholar 

  37. Pierce, B.C.: Bounded quantification is undecidable. Inf. Comput.112(1), 131–165 (1994)

    Article MathSciNet MATH  Google Scholar 

  38. Pottier, F.: A 3-part type inference engine. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 320–335. Springer, Heidelberg (2000).https://doi.org/10.1007/3-540-46425-5_21

    Chapter  Google Scholar 

  39. Rémy, D.: A case study of typechecking with constrained types: typing record concatenation (1995). Presented at the Workshop on Advances in Types for Computer Science at the Newton Institute, Cambridge, UK

    Google Scholar 

  40. Reynolds, J.C.: Preliminary design of the programming language Forsythe (1988)

    Google Scholar 

  41. Rompf, T., Amin, N.: Type soundness for dependent object types (DOT). In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 624–641 (2016)

    Google Scholar 

  42. The CoQ Development Team: CoQ (2019).https://coq.inria.fr

  43. Wadler, P.: The expression problem (1998). Discussion on the Java Genericity mailing list

    Google Scholar 

  44. Wang, F., Rompf, T.: Towards strong normalization for dependent object types (DOT). In: 31st European Conference on Object-Oriented Programming (ECOOP 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  45. Zhang, W., Sun, Y., Oliveira, B.C.d.S.: Compositional programming. ACM Trans. Program. Lang. Syst. (TOPLAS), 1–60 (2021)

    Google Scholar 

  46. Zhou, Y., Oliveira, B.C.d.S., Fan, A.: A calculus with recursive types, record concatenation and subtyping (artifact) (2022).https://doi.org/10.5281/zenodo.7003284

  47. Zhou, Y., Zhao, J., Oliveira, B.C.d.S.: Revisiting ISO-recursive subtyping. ACM Trans. Program. Lang. Syst. (TOPLAS) (2022).https://doi.org/10.1145/3549537

Download references

Acknowledgement

We thank the anonymous reviewers for their helpful comments. This work has been sponsored by Hong Kong Research Grant Council projects number 17209519, 17209520 and 17209821.

Author information

Authors and Affiliations

  1. The University of Hong Kong, Hong Kong, Hong Kong SAR, China

    Yaoda Zhou & Bruno C. d. S. Oliveira

  2. Zhejiang University, Hangzhou, China

    Andong Fan

Authors
  1. Yaoda Zhou

    You can also search for this author inPubMed Google Scholar

  2. Bruno C. d. S. Oliveira

    You can also search for this author inPubMed Google Scholar

  3. Andong Fan

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence toYaoda Zhou.

Editor information

Editors and Affiliations

  1. National University of Singapore, Singapore, Singapore

    Ilya Sergey

Rights and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zhou, Y., Oliveira, B.C.d.S., Fan, A. (2022). A Calculus with Recursive Types, Record Concatenation and Subtyping. In: Sergey, I. (eds) Programming Languages and Systems. APLAS 2022. Lecture Notes in Computer Science, vol 13658. Springer, Cham. https://doi.org/10.1007/978-3-031-21037-2_9

Download citation

Publish with us

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 7435
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 9294
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide -see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

[8]ページ先頭
©2009-2025 Movatter.jp