文章基本信息

标题：Higher Inductive Types in Programming
本地全文：下载
作者：Henning Basold ; Herman Geuvers ; Niels van der Weide 等
期刊名称：Journal of Universal Computer Science
印刷版ISSN：0948-6968
出版年度：2017
卷号：23
期号：1
页码：63-88
出版社：Graz University of Technology and Know-Center
摘要：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; higher inductive types; homotopy type theory