Document Open Access Logo

Martin Hofmann’s Case for Non-Strictly Positive Data Types

Authors Ulrich Berger , Ralph Matthes , Anton Setzer

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2018.1.pdf
  • Filesize: 0.55 MB
  • 22 pages

Document Identifiers

Author Details

Ulrich Berger
  • Dept. of Computer Science, Swansea University, United Kingdom
Ralph Matthes
  • IRIT (CNRS and University of Toulouse), France
Anton Setzer
  • Dept. of Computer Science, Swansea University, United Kingdom

Funding

The second and third authors got financial support by the COST action CA15123 EUTYPES.
  • Berger, Ulrich: Work supported by CORCON FP7 Marie Curie International Research Project, PIRSES-GA-2013-612638; COMPUTAL FP7 Marie Curie International Research Project, PIRSES-GA-2011-294962, CID FP7 Marie Curie International Research Project, H2020-MSCA-RISE-2016-731143
  • Setzer, Anton: Work supported by EPSRC grant EP/G033374/1 Theory and Applications of Induction Recursion; CORCON FP7 Marie Curie International Research Project, PIRSES-GA-2013-612638; COMPUTAL FP7 Marie Curie International Research Project, PIRSES-GA-2011-294962, CID FP7 Marie Curie International Research Project, H2020-MSCA-RISE-2016-731143

Acknowledgements

This paper is dedicated to the memory of the late Martin Hofmann. Martin was one of the leading researchers in the field of functional programming and type theory. This article is based on his notes [Martin Hofmann, 1993; Martin Hofmann, 1995], which is only one example of the inspiration he has given to many researchers. His tragic unexpected death was a deep loss for the community.

Cite AsGet BibTex

Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2018.1

Abstract

We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Software and its engineering → Abstract data types
  • Software and its engineering → Recursion
  • Software and its engineering → Software verification
  • Software and its engineering → Coroutines
Keywords
  • non strictly-positive data types
  • breadth-first traversal
  • program verification
  • Mendler-style recursion
  • System F
  • theorem proving
  • Coq
  • Agda
  • Haskell

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel and Ralph Matthes. Fixed Points of Type Constructors and Primitive Recursion. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, Karpacz, Poland, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 190-204. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_17.
  2. Ulrich Berger, Ralph Matthes, and Anton Setzer. Git repository of code supplementing the present paper. https://github.com/rmatthes/breadthfirstalahofmann, 2018-2019.
  3. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse de Doctorat d'État, Université de Paris VII, 1972. Google Scholar
  4. Jean-Yves Girard. Proofs and types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, Cambridge, 1989. Google Scholar
  5. Robert Harper and John C. Mitchell. Parametricity and variants of Girard’s J operator. Information Processing Letters, 70:1-5, 1999. Google Scholar
  6. Martin Hofmann. Non Strictly Positive Datatypes in System F, February 1993. Email on types mailing list, URL: http://www.seas.upenn.edu/~sweirich/types/archive/1993/msg00027.html.
  7. Martin Hofmann. Approaches to Recursive Datatypes - a Case Study, April 1995. LaTeX draft, 5 pages. Circulated by email. Google Scholar
  8. Geraint Jones and Jeremy Gibbons. Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips. Technical Report No. 71, Dept of Computer Science, University of Auckland, 1993. IFIP Working Group 2.1 working paper 705 WIN-2. URL: http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/linear.ps.gz.
  9. Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Doktorarbeit (PhD thesis), LMU München, 1998. Available via the homepage URL: http://www.irit.fr/~Ralph.Matthes/works.html.
  10. Ralph Matthes. Tarski’s fixed-point theorem and lambda calculi with monotone inductive types. Synthese, 133(1):107-129, 2002. Google Scholar
  11. Paul F. Mendler. Inductive Definition in Type Theory. Technical Report 87-870, Cornell University, Ithaca, N.Y., September 1987. PhD. Thesis (Paul F. Mendler = Nax P. Mendler). Google Scholar
  12. Chris Okasaki. Simple and Efficient Purely Functional Queues and Deques. J. Funct. Program., 5(4):583-592, 1995. URL: https://doi.org/10.1017/S0956796800001489.
  13. Chris Okasaki. Breadth-first numbering: lessons from a small exercise in algorithm design. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000., ICFP '00, pages 131-136, New York, NY, USA, 2000. ACM. URL: https://doi.org/10.1145/351240.351253.
  14. John C. Reynolds. Towards a Theory of Type Structure. In B. Robinet, editor, Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer, 1974. Google Scholar
  15. John C. Reynolds. Polymorphism is not Set-Theoretic. In Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin, editors, Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings, volume 173 of Lecture Notes in Computer Science, pages 145-156. Springer, 1984. URL: https://doi.org/10.1007/3-540-13346-1_7.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact