在 Agda 中使用证明验证时，我意识到我对某些类型显式地使用了归纳原则，而在其他情况下则使用了模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字：“在 Agda 中，依赖类型的模式匹配是该语言的一种原语，核心语言没有模式匹配所转换的归纳/递归原则。”
那么，由于 Agdas 模式匹配，Agda 中的类型理论归纳和递归原则（定义类型上的函数）是否完全多余？像这样的东西（隐含的路径归纳）只有教学价值。
http://en.wikipedia.org/wiki/Agda_%28programming_language%29#Dependently_typed_pattern_matching
我对 Agda 不熟悉，但我认为在这一点上，它与 Coq 类似，我可以回答 Coq 的相应问题。两种语言都基于具有归纳类型的直觉类型理论。
在直觉主义类型理论中，可以从足够通用的固定点组合器以及依赖模式匹配中推导出递归原理。模式匹配是不够的：虽然这允许破坏归纳类型，但单独的模式匹配不允许在该类型上编写递归函数。以维基百科为例：
add zero n = n add (suc n) m = suc (add n m)
这个定义是良构的这一事实不需要 ℕ 上的归纳原理。但是除了对 的第一个参数进行模式匹配之外add，它还需要一个规则来说明第二种情况下的递归调用是格式良好的。
通过模式匹配和递归，归纳原则可以定义为一等对象：
nat_ind f_zero f_suc zero = f
nat_ind f_zero f_suc (suc n) = f_suc (nat_ind f_zero f_suc n)
我不会说它们是完全不相关的：它们是组合器，因此可以帮助您构建您的开发、您思考它们的方式并帮助您编写更少（重复）的代码。
以 Haskell 为例：模式匹配在 Haskell 中也是原始的，但通常你会求助于fmap, bind,fold或traverse编写更少的代码或提供更通用、更健壮的实现。