JUCS - Journal of Universal Computer Science 23(1): 63-88, doi: 10.3217/jucs-023-01-0063
Higher Inductive Types in Programming
expand article infoHenning Basold, Herman Geuvers§, Niels Van Der Weide|
‡ Radboud University and CWI Amsterdam, Nijmegen, Netherlands§ Radboud University and Technical University Eindhoven, Nijmegen, Netherlands| Radboud University, Nijmegen, Netherlands
Open Access
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.
functional programming, homotopy type theory, higher inductive types