Deep induction provides induction rules for deep data types, i.e., data types that are defined over, or mutually recursively with, (other) such data types. Deep induction is currently defined only for type-indexed types, such as ADTs, nested types, and GADTs. In this paper we show how to extend deep induction from data types with only type indices to data types with term indices as well. Specifically, we extend to inductive families—as found in dependently typed systems such as Agda, Epigram, and Idris—the methodology for deriving sound deep induction rules that was originally developed for nested types and has recently been extended to GADTs.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Deep Induction for Inductive Families

  • Patricia Johann,
  • Edward Morehouse

摘要

Deep induction provides induction rules for deep data types, i.e., data types that are defined over, or mutually recursively with, (other) such data types. Deep induction is currently defined only for type-indexed types, such as ADTs, nested types, and GADTs. In this paper we show how to extend deep induction from data types with only type indices to data types with term indices as well. Specifically, we extend to inductive families—as found in dependently typed systems such as Agda, Epigram, and Idris—the methodology for deriving sound deep induction rules that was originally developed for nested types and has recently been extended to GADTs.