Abstract
We show how higher kinded generic programming can be represented faithfully within a dependently typed programming system. This development has been implemented using the Oleg system.
The present work can be seen as evidence for our thesis that extensions of type systems can be done by programming within a dependently typed language, using data as codes for types.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35672-3_13
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Thorsten Altenkirch and Conor McBride. OLEG code for Generic Programming Within Dependently Typed Programming. Available from http://www.dur.ac.uk/c.t.mcbride/generic/ 2002.
Thorsten Altenkirch, Bernhard Reus. Monadic presentations of lambda-terms using generalized inductive types. In Computer Science Logic 1999, 1999.
Lennart Augustsson. Cayenne—a language with dependent types. In ACM International Conference on Functional Programming. ACM, September 1998.
Roland Backhouse, Patrik Jansson, Johan Jeuring, and Lambert Meertens. Generic Programming—An Introduction. In S. Doaitse Sweierstra, Pedro R. Henriques, José N. Oliveira, editors, Advanced Functional Programming, Third International Summer School (AFP ‘88); Braga, Portugal, LNCS 1608, pages 28–115. Springer-Verlag, 1998.
Marcin Benke. Towards generic programming in Type Theory. Talk at the workshop TYPES 2002, Berg en Dal, Netherlands, April 2002.
Richard Bird, Ross Paterson. de Bruijn notation as a nested datatype. Journal of Functional Programming, 9 (1): 77–92, 1999.
Dave Clarke, Ralf Hinze, Johan Jeuring, Andres Löh, and Jan de Wit. The Generic Haskell user’s guide. Technical Report UU-CS-2001–26, Utrecht University, 2001.
Thierry Coquand. Pattern Matching with Dependent Types. In Proceedings of the Logical Framework workshop at Bdstad, June 1992.
Peter Dybjer. Inductive Sets and Families in Martin-Löf’s Type Theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. CUP, 1991.
Ralf Hinze. Generic programs and proofs. Habilitationsschrift, Universität Bonn, 2000.
Ralf Hinze, Johan Jeuring, and Andres Löh. Type-indexed data types. In Mathematics of Progam Construction, LNCS 2386, pages 148–174, 2002.
Ralf Hinze, Simon Peyton Jones. Derivable type classes. In Graham Hutton, editor, Proceedings of the Haskell Workshop 2000, 2000.
Haruo Hosoya, Jerome Vouillon, Benjamin C. Pierce. Regular expression types for XML. In International Conference on Functional Programming, pages 11–22, 2000.
Patrik Jansson, Johan Jeuring. PolyP—a polytypic programming language extension. In Proceedings of POPL ‘87, pages 470–482. ACM, January 1997.
C. Barry Jay, Gianna Belle, Eugenio Moggi. Functorial ML. Journal of Functional Programming, 8 (6): 573–619, 1998.
Zhaohui Luo, Randy Pollack. LEGO Proof Development System: User’s Manual. Technical Report ECS-LFCS-92–211, Laboratory for Foundations of Computer Science, University of Edinburgh, May 1992.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.
Conor McBride. The Derivative of a Regular Type is its Type of One-Hole Contexts. Electronically available, 2001.
Conor McBride. Faking It: Simulating Dependent Types in Haskell. J. Functional Programming,2002. Accepted; to appear.
Conor McBride, James McKinna. The view from the left. Submitted to the Journal of Functional Programming, Special Issue: Dependent Type Theory Meets Programming Practice, December 2001.
Bengt Nordström, Kent Petersson, Jan M. Smith. Programming in MartinLöf’s Type Theory. An Introduction. OUP, 1990.
Chris Okasaki. From Fast Exponentiation to Square Matrices: An Adventure in Types. In ACM International Conference on Functional Programming ‘89, 1999.
Simon Peyton Jones, John Hughes, et al. Haskell 98: A non-strict purely functional language. Available from: http://www.haskell.org 1999.
Simon Peyton Jones,d Erik Meijer. Henk: a typed intermediate language, 1997. ACM Workshop on Types in Compilation.
H. Pfeifer, H. Rueß. Polytypic abstraction in type theory. In Roland Back-house and Tim Sheard, editors, Workshop on Generic Programming (WGP’98). Dept. of Computing Science, Chalmers Univ. of Techn. and Göteborg Univ., June 1998.
Jan-Willem Roorda, Johan Jeuring. Pure type systems for functional programming. In preparation, 2001.
Mark Tullsen. The Zip Calculus. In Roland Backhouse and José Nuno Oliviera, editors, Mathematics of Program Construction, LNCS 1837, pages 2844. Springer-Verlag, 2000.
Philip Wadler. Views: A way for pattern matching to cohabit with data abstraction. In POPL’87. ACM, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Altenkirch, T., Mcbride, C. (2003). Generic Programming within Dependently Typed Programming. In: Gibbons, J., Jeuring, J. (eds) Generic Programming. IFIP — The International Federation for Information Processing, vol 115. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35672-3_1
Download citation
DOI: https://doi.org/10.1007/978-0-387-35672-3_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5320-2
Online ISBN: 978-0-387-35672-3
eBook Packages: Springer Book Archive