Indexed Containers
24TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS(2009)
摘要
We show that the syntactically rich notion of inductive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. Indexed containers generalize simple containers, capturing strictly positive families instead of just strictly positive types, without having to extend the core type theory. Other applications of indexed containers include datatype-generic programming and reasoning about polymorphic functions. The construction presented here has been formalized using the Agda system.
更多查看译文
关键词
Type Theory,functional programming
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络