Using Coq to Understand Nested Datatypes

  • A. Blanco
  • J. E. Freire
  • J. L. Freire
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4739)


Nested datatypes can be defined in a Hindley-Milner system but it is difficult to implement functions on them. This paper analyzes the requirements that must be satisfied in order to implement programs (catamorphisms and anamorphisms) on these types. A solution, using Hagino’s approach, is carried out here both in Haskell, using rank 2 signatures, and in the Coq proof assistant system where we have polymorphic recursion and also the capability to prove the correspondent programs specifications.


Recursive Call Information Processing Letter Regular Type Nest Type Interactive Theorem Prove 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bertot, I., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  2. 2.
    Bird, R., Meertens, L.: Nested datatypes. Mathematical foundations for computing. LNCS (1998)Google Scholar
  3. 3.
    Bird, R., Paterson, R.: de Bruijn notation as a nested datatype. Journal of Functional Programming 9(1) (1999)Google Scholar
  4. 4.
    Bird, R., Paterson, R.: Generalised folds for nested datatypes. Formal Aspects of Computing 11 (1999)Google Scholar
  5. 5.
    Blampied, P.A.: Structural Recursion for non-Uniform Data Types. Phd. Thesis. University of Nottingham (2000)Google Scholar
  6. 6.
    Martin, C., Gibbons, J.: On the Semantics of Nested Datatypes. Information Processing Letters 80 (2001)Google Scholar
  7. 7.
    Hagino, T.: A categorical programming language, PhD. Thesis. Edinburgh University (1987)Google Scholar
  8. 8.
    Hall, C.V., Hammond, K., Peyton Jones, S.L., Wadler, P.L.: Type classes in Haskell. ACM Transactions on Programning Languages and Systems (1996)Google Scholar
  9. 9.
    Hinze, R.: Numerical Representations as Higher–Order Nested Datatypes (1998),
  10. 10.
    Hinze, R.: Efficient Generalized Folds. In: Proceedinga of the Second Workshop on Generic Programming, WGP 2000 (2000)Google Scholar
  11. 11.
    Matthes, R.: Verification of programs on truly nested datatypes in intensional type theory. Mathematically Structured Functional Programming (2006)Google Scholar
  12. 12.
    Okasaki, C.: From Fast Exponentiation to Square Matrices: an Adventure in Types. ACM 1-58113-111-9/99/0009 (1999)Google Scholar
  13. 13.
    Rodriguez, D.: Verification of Iteration and Coiteration Schemes for Nested Datatypes in Coq. Institut für Informatik der Ludwig–Maximilians–Universität, München. Technical Report (2006)Google Scholar
  14. 14.
    Vene, V.: Categorical Programming with Inductive and Coinductive Types. Dissertationes Mathematicae Universitatis Tartuensis, 23 (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • A. Blanco
    • 1
  • J. E. Freire
    • 1
  • J. L. Freire
    • 1
  1. 1.University of A Coruña, Spain, University of A Coruña, LFCIA, Dept. of Computer Science, Faculty of Informatics, 15071 A CoruñaSpain

Personalised recommendations