×

The essence of dependent object types. (English) Zbl 1343.68046

Lindley, Sam (ed.) et al., A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday. Cham: Springer (ISBN 978-3-319-30935-4/pbk; 978-3-319-30936-1/ebook). Lecture Notes in Computer Science 9600, 249-272 (2016).
Summary: Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus \(\text{D}_{<:}\) of dependent functions, it adds records, intersections and recursion to arrive at DOT, a calculus for dependent object types. The paper shows an encoding of System F with subtyping in \(\text{D}_{<:}\) and demonstrates the expressiveness of DOT by modeling a range of Scala constructs in it.
For the entire collection see [Zbl 1333.68014].

MSC:

68N18 Functional programming and lambda calculus
03B70 Logic in computer science
68N15 Theory of programming languages

Software:

Scala; 1ML; GitHub; Tribe; HMap; Dotty; MixML
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15(4), 575–631 (1993) · doi:10.1145/155183.155231
[2] Amin, N., Moors, A., Odersky, M.: Dependent object types. In: FOOL (2012)
[3] Amin, N., Rompf, T., Odersky, M.: Foundations of path-dependent types. In: OOPSLA (2014) · doi:10.1145/2660193.2660216
[4] Ariola, Z.M., Maraist, J., Odersky, M., Felleisen, M., Wadler, P.: A call-by-need lambda calculus. In: POPL (1995) · Zbl 0908.03017 · doi:10.1145/199448.199507
[5] Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of system F with subtyping. Inf. Comput. 109(1/2), 4–56 (1994) · Zbl 0805.03008 · doi:10.1006/inco.1994.1013
[6] Clarke, D., Drossopoulou, S., Noble, J., Wrigstad, T.: Tribe: a simple virtual class calculus. In: AOSD (2007) · doi:10.1145/1218563.1218578
[7] Coppo, M., Dezani-Ciancaglini, M., Sallé, P.: Functional characterization of some semantic equalities inside lambda-calculus. In: Automata, Languages and Programming, 6th Colloquium (1979) · Zbl 0411.03013
[8] Cremet, V., Garillot, F., Lenglet, S., Odersky, M.: A core calculus for scala type checking. In: Královič, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 1–23. Springer, Heidelberg (2006) · Zbl 1132.68320 · doi:10.1007/11821069_1
[9] Cretin, J., Rémy, D.: System F with coercion constraints. In: CSL-LICS (2014) · Zbl 1394.03025 · doi:10.1145/2603088.2603128
[10] Dreyer, D., Rossberg, A.: Mixin’ up the ML module system. In: ICFP (2008) · Zbl 1323.68069
[11] Ernst, E.: Family polymorphism. In: Lindskov Knudsen, J. (ed.) ECOOP 2001. LNCS, vol. 2072, p. 303. Springer, Heidelberg (2001) · Zbl 0982.68637 · doi:10.1007/3-540-45337-7_17
[12] Ernst, E.: Higher-order hierarchies. In: ECOOP (2003) · doi:10.1007/978-3-540-45070-2_14
[13] Ernst, E., Ostermann, K., Cook, W.R.: A virtual class calculus. In: POPL (2006) · Zbl 1369.68072 · doi:10.1145/1111037.1111062
[14] Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060
[15] Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: POPL (1994) · doi:10.1145/174675.176927
[16] Adsul, B., Viroli, M.: On variance-based subtyping for parametric types. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, p. 441. Springer, Heidelberg (2002) · Zbl 1049.68791
[17] Leroy, X.: Manifest types, modules and separate compilation. In: POPL (1994) · doi:10.1145/174675.176926
[18] Macqueen, D.: Using dependent types to express modular structure. In: POPL (1986) · doi:10.1145/512644.512670
[19] Montagu, B., Rémy, D.: Modeling abstract types in modules with open existential types. In: POPL (2009) · Zbl 1315.68103
[20] Moors, A., Piessens, F., Odersky, M.: Safe type-level abstraction in scala. In: FOOL (2008)
[21] Odersky, M., Cremet, V., Röckl, C., Zenger, M.: A nominal theory of objects with dependent types. In: ECOOP (2003) · doi:10.1007/978-3-540-45070-2_10
[22] Odersky, M., Petrashko, D., Martres, G., others.: The dotty project (2013). https://github.com/lampepfl/dotty
[23] van der Ploeg, A.: The HMap package (2013). https://hackage.haskell.org/package/HMap
[24] Pretty, J.: Minimizing the slippery surface of failure. Talk at Scala World (2015). https://www.youtube.com/watch?v=26UHdZUsKkE
[25] Rompf, T., Amin, N.: From F to DOT: Type soundness proofs with definitional interpreters. Purdue University, Technical report (2015). http://arxiv.org/abs/1510.05216 · Zbl 1380.68111
[26] Rossberg, A.: 1ML - core and modules united (f-ing first-class modules). In: ICFP (2015) · Zbl 1360.68338 · doi:10.1145/2784731.2784738
[27] Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. J. Funct. Program. 24(5), 529–607 (2014) · Zbl 1322.68048 · doi:10.1017/S0956796814000264
[28] Scherer, G., Rémy, D.: Full reduction in the face of absurdity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 685–709. Springer, Heidelberg (2015) · Zbl 1335.68065 · doi:10.1007/978-3-662-46669-8_28
[29] Tate, R., Leung, A., Lerner, S.: Taming wildcards in java’s type system. In: PLDI (2011) · doi:10.1145/1993498.1993570
[30] Torgersen, M., Ernst, E., Hansen, C.P.: WildFJ. In: FOOL (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.