Code Generation for Higher Inductive Types

A Study in Agda Metaprogramming
  • Paventhan VivekanandanEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11285)


Higher inductive types are inductive types that include nontrivial higher-dimensional structure, represented as identifications that are not reflexivity. While work proceeds on type theories with a computational interpretation of univalence and higher inductive types, it is convenient to encode these structures in more traditional type theories with mature implementations. However, these encodings involve a great deal of error-prone additional syntax. We present a library that uses Agda’s metaprogramming facilities to automate this process, allowing higher inductive types to be specified with minimal additional syntax.


Higher inductive type Elaboration Elimination rules Computation rules 



The author is greatly indebted to David Christiansen for his contributions and advice, and the anonymous reviewers for their valuable review comments.


  1. 1.
  2. 2.
    Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theor. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Altenkirch, T.: Containers in homotopy type theory, talk at Mathematical Structures of Computation, January 2014Google Scholar
  4. 4.
    Altenkirch, T., McBride, C., Morris, P.: Generic programming with dependent types. In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.) SSDGP 2006. LNCS, vol. 4719, pp. 209–257. Springer, Heidelberg (2007). Scholar
  5. 5.
    Angiuli, C., Harper, R., Wilson, T.: Computational higher-dimensional type theory. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL, Paris, France, pp. 680–693, January 2017Google Scholar
  6. 6.
    Angiuli, C., Morehouse, E., Licata, D.R., Harper, R.: Homotopical patch theory. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP, Gothenburg, Sweden, September 2014Google Scholar
  7. 7.
    Basold, H., Geuvers, H., van der Weide, N.: Higher inductive types in programming. J. Univ. Comput. Sci. 23(1), 63–88 (2017)MathSciNetGoogle Scholar
  8. 8.
    Brunerie, G.: Custom definitional equalities in agda, talk at Univalent Foundations and Proof Assistants session of the 5th International Congress on Mathematical Software, July 2016Google Scholar
  9. 9.
    Cavallo, E., Harper, R.: Computational higher type theory iv: inductive types, July 2018. arXiv:1801.01568
  10. 10.
    Chapman, J., Évariste Dagand, P., McBride, C., Morris, P.: The gentle art of levitation. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP, Baltimore, USA, September 2010Google Scholar
  11. 11.
    Christiansen, D.: Practical reflection and metaprogramming for dependent types. Ph.D. thesis, IT University of Copenhagen (2016)Google Scholar
  12. 12.
    Christiansen, D., Brady, E.: Elaborator reflection: extending Idris in Idris. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP, Nara, Japan, September 2016Google Scholar
  13. 13.
    Cockx, J., Abel, A.: Sprinkles of extensionality for your vanilla type theory. In: 22nd International Conference on Types for Proofs and Programs, May 2016Google Scholar
  14. 14.
    Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP, Gothenburg, Sweden, pp. 257–268, September 2014Google Scholar
  15. 15.
    Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. In: Proceedings of the 21st International Conference on Types for Proofs and Programs, Tallinn, Estonia, May 2015Google Scholar
  16. 16.
    Coquand, T., Huber, S., Mörtberg, A.: On higher inductive types in cubical type theory (2018). arXiv:1802.01170
  17. 17.
    Dybjer, P., Moeneclaey, H.: Finitary higher inductive types in the groupoid model. Electro. Notes Theor. Comput. Sci. 336, 119–134 (2018)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. In: Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming, ICFP, September 2017Google Scholar
  19. 19.
    Kaposi, A., Kovács, A.: A syntax for higher inductive-inductive types. In: Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, FSCD, Oxford, UK, July 2018Google Scholar
  20. 20.
    Kokke, P., Swierstra, W.: Auto in agda. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 276–301. Springer, Cham (2015). Scholar
  21. 21.
    Lumsdaine, P.L., Shulman, M.: Semantics of higher inductive types, May 2017. arXiv:1705.07088
  22. 22.
    Löh, A., Magalhães, J.P.: Generic programming with indexed functors. In: Proceedings of the 7th ACM SIGPLAN Workshop on Generic Programming, WGP, September 2011Google Scholar
  23. 23.
    Mimram, S., Giusto, C.D.: A categorical theory of patches. Electron. Notes Theor. Comput. Sci. 298, 283–307 (2013)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology, Göteborg, Sweden (2007)Google Scholar
  25. 25.
    Pelayo, A., Warren, M.: Homotopy type theory and Voevodsky’s univalent foundations, October 2012. arXiv:1210.5658
  26. 26.
    Popa, R.A., Redfield, C.M., Zeldovich, N., Balakrishnan, H.: CryptDB: protecting confidentiality with encrypted query processing. In: Proceedings of the 23rd ACM Symposium on Operating Systems Principles, SOSP, Cascais, Portugal (2011)Google Scholar
  27. 27.
    Roundy, D.: Darcs: distributed version management in haskell. In: Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell, September 2005Google Scholar
  28. 28.
    Stutterheim, J., Swierstra, W., Swierstra, S.D.: Forty hours of declarative programming: teaching prolog at the junior college utrecht. Electron. Proc. Theor. Comput. Sci. 106, 50–62 (2013)CrossRefGoogle Scholar
  29. 29.
    The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013).
  30. 30.
    Vivekanandan, P.: HoTT-Crypt: a study in homotopy type theory based on cryptography. In: Short Paper proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-22, Ethiopia, November 2018.
  31. 31.
    van der Walt, P.: Reflection in agda. Master’s thesis. Utrecht University, Utrecht, Netherlands (2012)Google Scholar
  32. 32.
    van der Walt, P., Swierstra, W.: Engineering proof by reflection in agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Indiana UniversityBloomingtonUSA

Personalised recommendations