Hostname: page-component-8448b6f56d-m8qmq Total loading time: 0 Render date: 2024-04-16T10:10:55.024Z Has data issue: false hasContentIssue false
  • English
  • Français

Transporting functions across ornaments

Part of: JFP Research Articles

Published online by Cambridge University Press:  23 April 2014

PIERRE-ÉVARISTE DAGAND  and
CONOR McBRIDE
PIERRE-ÉVARISTE DAGAND
Affiliation:
Inria Rocquencourt, Le Chesnay, France (e-mail: pierre-evariste.dagand@inria.fr)
CONOR McBRIDE
Affiliation:
University of Strathclyde, Glasgow, UK (e-mail: conor@cis.strath.ac.uk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: We can finally write correct-by-construction software. However, this extreme accuracy is also a curse: A datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: The users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.

Type
Articles
Information
Journal of Functional Programming , Volume 24 , Issue 2-3: ICFP 2012 , May 2014 , pp. 316 - 383
Copyright
Copyright © Cambridge University Press 2014 

References

Atkey, R., Johann, P & Ghani, N. (2012) Refining inductive types. Logic. Methods Comput. Sci. 8 (2), 9. 10.2168/LMCS-8(2:9)2012.Google Scholar
Benton, N., Hur, C.-K., Kennedy, A. J. & Mcbride, C. (2012) Strongly typed term representations in coq. J. Autom. Reason. 49 (2), 141–159. 10.1007/s10817-011-9219-0.CrossRefGoogle Scholar
Bernardy, J.-P. & Guilhem, M. (2013) Type-theory in color. In Proceedings of the International Conference on Functional Programming, pp. 61–72. 10.1145/2500365.2500577.Google Scholar
Bernardy, J.-P. & Lasson, M. (2011) Realizability and parametricity in pure type systems. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 6604. Berlin, Germany: Springer, pp. 108–122. 10.1007/978-3-642-19805-28.Google Scholar
Bird, R. S. & de Moor, O. (1997). Algebra of Programming. Upper Saddle River, NJ: Prentice Hall.Google Scholar
Brady, E. & Hammond, K. (2010). Scrapping your inefficient engine: Using partial evaluation to improve domain-specific language implementation. In International Conference in Functional Programming, pp. 297–308. 10.1145/1863543.1863587.Google Scholar
Brady, E., McBride, C. & McKinna, J. (2003) Inductive families need not store their indices. Types for Proofs and Programs. Berlin, Germany: Springer. 10.1007/978-3-540-24849-18.Google Scholar
Chapman, J., Dagand, P.-É., McBride, C., & Morris, P. (2010). The gentle art of levitation. In International Conference on Functional Programming, pp. 3–14. 10.1145/1863543.1863547.Google Scholar
Cheney, J. & Hinze, R. (2003) First-Class Phantom Types. Technical Report. Cornell University, Ithaca, NY.Google Scholar
Dagand, P.-E. (2013) Reusability and Dependent Types. PhD thesis, University of Strathclyde, Glasgow, UK.Google Scholar
Dagand, P.-E. & McBride, C. (2012) Transporting functions across ornaments. In Proceedings of the 17th International Conference on Func tional Programming (ICFP 2012), pp. 103–114. 10.1145/2364527.2364544.Google Scholar
Dagand, P.-E. & McBride, C. (2013a) A categorical treatment of ornaments. In Twenty-Eighth Annual ACM/IEEE Symposium on Logics in Computer Science (LICS 2013). 10.1109/LICS.2013.60.Google Scholar
Dagand, P.-E. & McBride, C. (2013b) Elaborating inductive definitions. Journées francophones des langages applicatifs. Available at: http://hal.inria.fr/hal-00778975.Google Scholar
Dybjer, P. (1994) Inductive families. Form. Asp. Comput. 6 (4), 440–465. 10.1007/BF01211308.Google Scholar
Freeman, T. & Pfenning, F. (1991) Refinement types for ML. In Programming Language Design and Implementation, pp. 268–277. 10.1145/113445.113468.Google Scholar
Fumex, C. (2012) Induction and Coinduction Schemes in Category Theory. PhD thesis, University of Strathclyde, Glasgow, UK.Google Scholar
Gonthier, G., Mahboubi, A. & Tassi, E. (2008) A Small Scale Reflection Extension for the Coq System. Research Report RR-6455. Valbonne, France: INRIA.Google Scholar
Hermida, C. & Jacobs, B. (1998) Structural induction and coinduction in a fibrational setting. Inf. Computat. 145 (2), 107–152. 10.1006/inco.1998.2725.CrossRefGoogle Scholar
Hofmann, M. & Streicher, T. (1994) The groupoid model refutes uniqueness of identity proofs. Proceedings of the Symposium on Logic in Computer Science, pp. 208–212. 10.1109/LICS.1994.316071.Google Scholar
Ko, H.-S. & Gibbons, J. (2011) Modularising inductive families. Workshop on Generic Programming. ACM, pp. 13–24.Google Scholar
Lindblad, F. & Benke, M. (2004) A tool for automated theorem proving in Agda. In Types for Proofs and Programs. Berlin, Germany: Springer, pp. 154–169. 10.1007/1161799010.Google Scholar
McBride, C. (1999). Dependently Typed Functional Programs and Their Proofs. PhD thesis, LFCS, University of Edinburgh, Edinburgh, UK.Google Scholar
McBride, C. (2002). Elimination with a motive. In Types for Proofs and Programs. Berlin, Germany: Springer, 197–216. 10.1007/3-540-45842-513.Google Scholar
McBride, C. (to appear). Ornamental algebras, algebraic ornaments. J. Funct. Program.Google Scholar
McBride, C., Goguen, H. & McKinna, J. (2004) A few constructions on constructors. Proceedings of International Workshop, Types for Proofs and Programs (TYPES 2004), pp. 186–20010.1007/1161799012.Google Scholar
McBride, C. & McKinna, J. (2004). The view from the left. J. Funct. Program. 14 (1), 69–111. 10.1007/1178027427.Google Scholar
Morris, P., Altenkirch, T. & Ghani, N. (2009) A universe of strictly positive families. Int. J. Found. Comput. Sci. 20 (1), 83–107. 10.1142/S0129054109006462.Google Scholar
Paulin-Mohring, C. (1989) Extraction de Programmes dans le Calcul des Constructions. PhD thesis, Université Paris VII, France.Google Scholar
Schrijvers, T., Peyton Jones, S., Sulzmann, M. & Vytiniotis, D. (2009) Complete and decidable type inference for GADTs. In Proceedings of International Conference on Functional Programming, pp. 341–352. 10.1145/1596550.1596599.Google Scholar
Strub, P.-Y. (2010) Coq modulo theory. Comput. Sci. Logic. pp. 529–543. 10.1007/978-3-642-15205-440.Google Scholar
Swamy, N., Chen, J., Fournet, C., Strub, P.-Y., Bhargavan, K. & Yang, J. (2011) Secure distributed programming with value-dependent types. In Proceedings of International Conference on Functional Programming, pp. 266–278. 10.1145/2034773.2034811.Google Scholar
Wadler, P. (1989) Theorems for free! In Proceedings of Conference on Functional Programming Languages and Computer Architecture, pp. 347–359. 10.1145/99370.99404.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.