Advertisement

A Dependently Typed Multi-stage Calculus

  • Akira KawataEmail author
  • Atsushi Igarashi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11893)

Abstract

We study a dependently typed extension of a multi-stage programming language à la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and an evaluation construct for execution of programs dynamically generated by this code manipulation. Dependent types are expected to bring to multi-stage programming enforcement of strong invariant—beyond simple type safety—on the behavior of dynamically generated code. An extension is, however, not trivial because such a type system would have to take stages of types—roughly speaking, the number of surrounding quotations—into account.

To rigorously study properties of such an extension, we develop \(\lambda ^{\text {MD}}\), which is an extension of Hanada and Igarashi’s typed calculus \(\lambda ^{\triangleright \%}\) with dependent types, and prove its properties including preservation, confluence, strong normalization for full reduction, and progress for staged reduction. Motivated by code generators that generate code whose type depends on a value from outside of the quotations, we argue the significance of cross-stage persistence in dependently typed multi-stage programming and certain type equivalences that are not directly derived from reduction rules.

Keywords

Multi-stage programming Cross-stage persistence Dependent types 

Notes

Acknowledgments

We would like to thank John Toman, Yuki Nishida, and anonymous reviewers for useful comments.

References

  1. 1.
    Aspinall, D., Hofmann, M.: Dependent types. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, chap. 2. MIT press, Cambridge (2005)Google Scholar
  2. 2.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
  3. 3.
    Benaissa, Z.E.A., Moggi, E., Taha, W., Sheard, T.: Logical modalities and multi-stage programming. In: Federated Logic Conference (FLoC) Satellite Workshop on Intuitionistic Modal Logics and Applications (IMLA) (1999)Google Scholar
  4. 4.
    Berger, M., Tratt, L.: Program logics for homogeneous generative run-time meta-programming. Logical Methods Comput. Sci. 11(1) (2015). https://lmcs.episciences.org/929
  5. 5.
    Brady, E., Hammond, K.: Dependently typed meta-programming. In: Trends in Functional Programming (2006)Google Scholar
  6. 6.
    Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages using ASTs, gensym, and reflection. In: Pfenning, F., Smaragdakis, Y. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 57–76. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-39815-8_4CrossRefGoogle Scholar
  7. 7.
    Chen, C., Xi, H.: Meta-programming through typeful code representation. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming ICFP 2003, pp. 275–286. ACM, New York (2003)Google Scholar
  8. 8.
    Chlipala, A.: Ur: statically-typed metaprogramming with type-level record computation. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2010, pp. 122–133. ACM, New York (2010)Google Scholar
  9. 9.
    Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2–3), 95–120 (1988)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Davies, R.: A temporal-logic approach to binding-time analysis. In: Proceedings of Eleventh Annual IEEE Symposium on Logic in Computer Science LICS 1996, pp. 184–195. IEEE (1996)Google Scholar
  11. 11.
    Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555–604 (2001)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. PACMPL 1(ICFP), 34:1–34:29 (2017)CrossRefGoogle Scholar
  13. 13.
    Fogarty, S., Pasalic, E., Siek, J., Taha, W.: Concoqtion: indexed types now! In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation PEPM 2007, pp. 112–121. ACM, New York (2007)Google Scholar
  14. 14.
    Hanada, Y., Igarashi, A.: On cross-stage persistence in multi-stage programming. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 103–118. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-07151-0_7CrossRefzbMATHGoogle Scholar
  15. 15.
    Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Kim, I., Yi, K., Calcagno, C.: A polymorphic modal type system for lisp-like multi-staged languages. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2003), pp. 257–268 (2006)Google Scholar
  17. 17.
    Kiselyov, O.: Reconciling abstraction with high performance: a MetaOCaml approach. Found. Trends Program. Lang. 5(1), 1–101 (2018)Google Scholar
  18. 18.
    Kiselyov, O.: The design and implementation of BER MetaOCaml - system description. In: Proceedings of the 12th International Symposium on Functional and Logic Programming, FLOPS 2014, Kanazawa, Japan, 4–6 June 2014, pp. 86–102 (2014)CrossRefGoogle Scholar
  19. 19.
    Leijen, D., Meijer, E.: Domain specific embedded compilers. In: Proceedings of the 2nd Conference on Domain-Specific Languages (DSL 1999), pp. 109–122 (1999)Google Scholar
  20. 20.
    Mainland, G.: Explicitly heterogeneous metaprogramming with metahaskell. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming ICFP 2012, pp. 311–322. ACM, New York (2012)Google Scholar
  21. 21.
    Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Logic Colloquium, vol. 80, p. 73, January 1973CrossRefGoogle Scholar
  22. 22.
    Meyer, A.R., Reinhold, M.B.: “Type” is not a type. In: Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 1986, pp. 287–295. ACM, New York (1986)Google Scholar
  23. 23.
    Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348–375 (1978)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Moggi, E., Taha, W., Benaissa, Z.E.-A., Sheard, T.: An idealized metaML: simpler, and more expressive. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 193–207. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-49099-X_13CrossRefGoogle Scholar
  25. 25.
    Nanevski, A., Pfenning, F.: Staged computation with names and necessity. J. Funct. Program. 15(5), 893–939 (2005)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Pasalic, E., Taha, W., Sheard, T.: Tagless staged interpreters for typed languages. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming ICFP 2002, pp. 218–229. ACM, New York (2002)Google Scholar
  27. 27.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  28. 28.
    Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A type system for certified binaries. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2002, pp. 217–232. ACM, New York (2002)Google Scholar
  29. 29.
    Taha, W.: A gentle introduction to multi-stage programming, part II. In: Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2007. LNCS, vol. 5235, pp. 260–290. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-88643-3_6CrossRefGoogle Scholar
  30. 30.
    Taha, W., Nielsen, M.F.: Environment classifiers. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2003), pp. 26–37. ACM, New York (2003)Google Scholar
  31. 31.
    Taha, W., Sheard, T.: MetaML and multi-stage programming with explicit annotations. Theor. Comput. Sci. 248(1–2), 211–242 (2000)CrossRefGoogle Scholar
  32. 32.
    Tsukada, T., Igarashi, A.: A logical foundation for environment classifiers. Logical Methods Comput. Sci. 6(4), 1–43 (2010)Google Scholar
  33. 33.
    Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2003), pp. 224–235 (2003)Google Scholar
  34. 34.
    Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 1998), pp. 249–257 (1998)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Graduate School of InformaticsKyoto UniversityKyotoJapan

Personalised recommendations