Abstract
Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus 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 D\(_{<:}\) and demonstrates the expressiveness of DOT by modeling a range of Scala constructs in it.
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
Similar content being viewed by others
Notes
- 1.
The definition of \(t^*\) assumes a countable supply of fresh names x, \(X \notin { fv}(t)\).
- 2.
The full development on paper and in Coq is at http://wadlerfest.namin.net.
- 3.
The example is based on a talk by Jon Pretty (2015).
- 4.
Having both kind of bounds is essential in DOT to model type aliases; if we would replace bounds by aliases we would run into the same problems.
References
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15(4), 575–631 (1993)
Amin, N., Moors, A., Odersky, M.: Dependent object types. In: FOOL (2012)
Amin, N., Rompf, T., Odersky, M.: Foundations of path-dependent types. In: OOPSLA (2014)
Ariola, Z.M., Maraist, J., Odersky, M., Felleisen, M., Wadler, P.: A call-by-need lambda calculus. In: POPL (1995)
Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of system F with subtyping. Inf. Comput. 109(1/2), 4–56 (1994)
Clarke, D., Drossopoulou, S., Noble, J., Wrigstad, T.: Tribe: a simple virtual class calculus. In: AOSD (2007)
Coppo, M., Dezani-Ciancaglini, M., Sallé, P.: Functional characterization of some semantic equalities inside lambda-calculus. In: Automata, Languages and Programming, 6th Colloquium (1979)
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)
Cretin, J., Rémy, D.: System F with coercion constraints. In: CSL-LICS (2014)
Dreyer, D., Rossberg, A.: Mixin’ up the ML module system. In: ICFP (2008)
Ernst, E.: Family polymorphism. In: Lindskov Knudsen, J. (ed.) ECOOP 2001. LNCS, vol. 2072, p. 303. Springer, Heidelberg (2001)
Ernst, E.: Higher-order hierarchies. In: ECOOP (2003)
Ernst, E., Ostermann, K., Cook, W.R.: A virtual class calculus. In: POPL (2006)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)
Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: POPL (1994)
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)
Leroy, X.: Manifest types, modules and separate compilation. In: POPL (1994)
Macqueen, D.: Using dependent types to express modular structure. In: POPL (1986)
Montagu, B., Rémy, D.: Modeling abstract types in modules with open existential types. In: POPL (2009)
Moors, A., Piessens, F., Odersky, M.: Safe type-level abstraction in scala. In: FOOL (2008)
Odersky, M., Cremet, V., Röckl, C., Zenger, M.: A nominal theory of objects with dependent types. In: ECOOP (2003)
Odersky, M., Petrashko, D., Martres, G., others.: The dotty project (2013). https://github.com/lampepfl/dotty
van der Ploeg, A.: The HMap package (2013). https://hackage.haskell.org/package/HMap
Pretty, J.: Minimizing the slippery surface of failure. Talk at Scala World (2015). https://www.youtube.com/watch?v=26UHdZUsKkE
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
Rossberg, A.: 1ML - core and modules united (f-ing first-class modules). In: ICFP (2015)
Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. J. Funct. Program. 24(5), 529–607 (2014)
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)
Tate, R., Leung, A., Lerner, S.: Taming wildcards in java’s type system. In: PLDI (2011)
Torgersen, M., Ernst, E., Hansen, C.P.: WildFJ. In: FOOL (2004)
Acknowledgments
Adriaan Moors, Donna Malayeri and Geoffrey Washburn have contributed to previous versions of DOT. We thank the anonymous reviewers of Wadlerfest for helpful comments on this paper. For insightful discussions we thank Amal Ahmed, Derek Dreyer, Erik Ernst, Matthias Felleisen, Paolo Giarrusso, Scott Kilpatrick, Grzegorz Kossakowski, Alexander Kuklev, Viktor Kuncak, Jon Pretty, Didier Rémy, Lukas Rytz, Miles Sabin, Ilya Sergey, Jeremy Siek, Josh Suereth and Phil Wadler. Contributors to the Dotty project include Dmitry Petrashko, Guillaume Martres, Vladimir Nikolaev, Ondřej Lhoták, Vera Salvisberg and Jason Zaugg. This research was supported by the European Research Council (ERC) under grant 587327 DOPPLER and the Swiss National Science Foundation under grant “Foundations of Scala”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Additional Rules and Detailed Proofs
A Additional Rules and Detailed Proofs
1.1 A.1 Typing of Dependent Sums/\(\varSigma \)s
There are one subtyping rule and four typing rules (all admissible in D\(_{<:}\)) associated with the encoding of dependent sums given in Sect. 2.1.
The proofs of admissibility are left as an (easy) exercise to the reader.
1.2 A.2 Proof of Theorem 2
We want to show that the translation \(-^*\) preserves typing, i.e. if \(\varGamma \,\vdash _{F}\, t: T\) then \(\varGamma ^* \,\vdash _{D}\, t^*: T^*\).
We start by stating and proving two helper lemmas. Write \([x.A:=U]T\) for the capture-avoiding substitution of \(x.A\) for U in T.
Lemma 6
Substitution of type variables for types commutes with translation of types, i.e.
Proof
The proof is by straight-forward induction on the structure of T.
Lemma 7
The following subtyping rules are admissible in D\(_<\):
Proof
The proof is by induction on the structure of T.
Proof
(Theorem 2 ). Proof is by induction on (F\(_{<:}\)) typing derivations. The case for subsumption follows immediately from preservation of subtyping (Theorem 1). The only remaining non-trivial cases are type and term application.
Term Application Case. We need to show that
is admissible. First note that z is not in \({ fv}(T^*)\), hence \([z:=y]T^* = T^*\) for all y. In particular, using (Var) and (All-E), we have
where \(\varGamma ' = \varGamma ^*, x: \forall (z\!:\!S^*)T^*, y: S^*\). Applying the induction hypothesis, context weakening and (Let), we obtain
The result follows by applying the induction hypothesis once more:
Type Application Case. By preservation of subtyping, we have \(\varGamma ^* \,\vdash \,U^* <:S^*\), hence it suffices to show that
is admissible. By context weakening, (Typ-\(<:\)-Typ), (Bot) and (Sub), we have
where \(\varGamma ' = \varGamma ^*, x: \forall (x_X\!:\!\{A: \bot ..S^*\})T^*, y_Y: \{A: U^*..U^*\}\). By (Var) and (All-E), we have
Next, we observe that, by Lemma 6
By Lemma 7, (Var) and (Sub), we thus have
The result follows from applying (Let) twice. Note that, being fresh, neither x nor \(y_Y\) appear free in \(([X:=U]T)^*\), hence the hygiene condition of (Let) holds.
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Amin, N., Grütter, S., Odersky, M., Rompf, T., Stucki, S. (2016). The Essence of Dependent Object Types. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds) A List of Successes That Can Change the World. Lecture Notes in Computer Science(), vol 9600. Springer, Cham. https://doi.org/10.1007/978-3-319-30936-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-30936-1_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-30935-4
Online ISBN: 978-3-319-30936-1
eBook Packages: Computer ScienceComputer Science (R0)