Function definition by induction principles in Agda

Question

When playing around with proof verification in Agda, I realised that I used induction principles for some types explicitly and in other cases used pattern matching istead. I finally found some text about pattern matching and induction principles on wikipedia: "In Agda, dependently typed pattern matching is a primitive of the language, the core language doesn't have the induction/recursion principles that pattern matching translates to."

So are type theoretic induction and recursion principles (to define functions on types) in Agda completely redundant because of Agdas pattern matching? Something like this (Path induction implied) would have only didactical value then.

http://en.wikipedia.org/wiki/Agda_%28programming_language%29#Dependently_typed_pattern_matching

Answer 1

I'm not familiar with Agda, but I think that on this particular point, it is similar to Coq, and I can answer the corresponding question for Coq. Both languages are based on intuitionistic type theory with inductive types.

In intuitionistic type theory, it is possible to derive recursion principles from a sufficiently general fixpoint combinator, plus dependent pattern matching. Pattern matching isn't enough: while this allows an inductive type to be destructed, pattern matching alone doesn't allow writing recursive functions on that type. Taking the example from Wikipedia:

add zero n = n
add (suc n) m = suc (add n m)

The fact that this definition is well-formed doesn't require an induction principle on ℕ. But in addition to the pattern matching beformed on the first argument of add, it requires a rule that states that the recursive call in the second case is well-formed.

With pattern matching and recursion, induction principles can be defined as first-class objects:

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)