Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 23 / Issue 1

available in:   PDF (188 kB) PS (302 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-023-01-0063


Higher Inductive Types in Programming

Henning Basold (Radboud University and CWI Amsterdam, The Netherlands)

Herman Geuvers (Radboud University and Technical University Eindhoven, The Netherlands)

Niels van der Weide (Radboud University, The Netherlands)

Abstract: We propose general rules for higher inductive types with non-dependent and dependent elimination rules. These can be used to give a formal treatment of data types with laws as has been discussed by David Turner in his earliest papers on Miranda [Turner(1985)]. The non-dependent elimination scheme is particularly useful for defining functions by recursion and pattern matching, while the dependent elimination scheme gives an induction proof principle. We have rules for non-recursive higher inductive types, like the integers, but also for recursive higher inductive types like the truncation. In the present paper we only allow path constructors (so there are no higher path constructors), which is sufficient for treating various interesting examples from functional programming, as we will briefly show in the paper: arithmetic modulo, integers and finite sets.

Keywords: functional programming, higher inductive types, homotopy type theory

Categories: D.3.1, F.4.m