Skip to main content

2019 | OriginalPaper | Buchkapitel

Code Generation for Higher Inductive Types

A Study in Agda Metaprogramming

verfasst von : Paventhan Vivekanandan

Erschienen in: Functional and Constraint Logic Programming

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
2.
Zurück zum Zitat Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theor. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRef Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theor. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRef
3.
Zurück zum Zitat Altenkirch, T.: Containers in homotopy type theory, talk at Mathematical Structures of Computation, January 2014 Altenkirch, T.: Containers in homotopy type theory, talk at Mathematical Structures of Computation, January 2014
5.
Zurück zum Zitat 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 2017 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 2017
6.
Zurück zum Zitat 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 2014 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 2014
7.
Zurück zum Zitat Basold, H., Geuvers, H., van der Weide, N.: Higher inductive types in programming. J. Univ. Comput. Sci. 23(1), 63–88 (2017)MathSciNet Basold, H., Geuvers, H., van der Weide, N.: Higher inductive types in programming. J. Univ. Comput. Sci. 23(1), 63–88 (2017)MathSciNet
8.
Zurück zum Zitat Brunerie, G.: Custom definitional equalities in agda, talk at Univalent Foundations and Proof Assistants session of the 5th International Congress on Mathematical Software, July 2016 Brunerie, G.: Custom definitional equalities in agda, talk at Univalent Foundations and Proof Assistants session of the 5th International Congress on Mathematical Software, July 2016
10.
Zurück zum Zitat 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 2010 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 2010
11.
Zurück zum Zitat Christiansen, D.: Practical reflection and metaprogramming for dependent types. Ph.D. thesis, IT University of Copenhagen (2016) Christiansen, D.: Practical reflection and metaprogramming for dependent types. Ph.D. thesis, IT University of Copenhagen (2016)
12.
Zurück zum Zitat 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 2016 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 2016
13.
Zurück zum Zitat Cockx, J., Abel, A.: Sprinkles of extensionality for your vanilla type theory. In: 22nd International Conference on Types for Proofs and Programs, May 2016 Cockx, J., Abel, A.: Sprinkles of extensionality for your vanilla type theory. In: 22nd International Conference on Types for Proofs and Programs, May 2016
14.
Zurück zum Zitat 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 2014 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 2014
15.
Zurück zum Zitat 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 2015 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 2015
17.
Zurück zum Zitat Dybjer, P., Moeneclaey, H.: Finitary higher inductive types in the groupoid model. Electro. Notes Theor. Comput. Sci. 336, 119–134 (2018)MathSciNetCrossRef Dybjer, P., Moeneclaey, H.: Finitary higher inductive types in the groupoid model. Electro. Notes Theor. Comput. Sci. 336, 119–134 (2018)MathSciNetCrossRef
18.
Zurück zum Zitat 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 2017 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 2017
19.
Zurück zum Zitat 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 2018 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 2018
22.
Zurück zum Zitat 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 2011 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 2011
23.
Zurück zum Zitat Mimram, S., Giusto, C.D.: A categorical theory of patches. Electron. Notes Theor. Comput. Sci. 298, 283–307 (2013)MathSciNetCrossRef Mimram, S., Giusto, C.D.: A categorical theory of patches. Electron. Notes Theor. Comput. Sci. 298, 283–307 (2013)MathSciNetCrossRef
24.
Zurück zum Zitat Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology, Göteborg, Sweden (2007) Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology, Göteborg, Sweden (2007)
25.
26.
Zurück zum Zitat 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) 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)
27.
Zurück zum Zitat Roundy, D.: Darcs: distributed version management in haskell. In: Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell, September 2005 Roundy, D.: Darcs: distributed version management in haskell. In: Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell, September 2005
28.
Zurück zum Zitat 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)CrossRef 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)CrossRef
30.
Zurück zum Zitat 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. https://doi.org/10.29007/tvpp 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. https://​doi.​org/​10.​29007/​tvpp
31.
Zurück zum Zitat van der Walt, P.: Reflection in agda. Master’s thesis. Utrecht University, Utrecht, Netherlands (2012) van der Walt, P.: Reflection in agda. Master’s thesis. Utrecht University, Utrecht, Netherlands (2012)
Metadaten
Titel
Code Generation for Higher Inductive Types
verfasst von
Paventhan Vivekanandan
Copyright-Jahr
2019
DOI
https://doi.org/10.1007/978-3-030-16202-3_2