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