Definition of a function by induction principles in Agda
When playing around with proof checking in Agda, I realized that I was using induction principles explicitly for some types and the istead pattern of matching in other cases. Finally, I found some text about pattern matching principles and induction principle on wikipedia: "In Agda, dependent pattern matching is a primitive language, the main language has no induction / recursion principles that pattern matching".
So the theoretical principles of type induction and recursion (for defining functions on types) in Agda are completely redundant due to the Agdas pattern matching? Something like this ( implies induction of the path ) will only have a didactic meaning.
http://en.wikipedia.org/wiki/Agda_%28programming_language%29#Dependently_typed_pattern_matching
source to share
I wouldn't say they are completely irrelevant: they are combinators and, as such, can help you structure your designs, the way you think about them, and help you write less (repetitive) code.
Look in Haskell, for example, pattern matching is also primitive in the Haskell, but most often you resort to fmap
, bind
, fold
or traverse
, to write less code or give a more general, more secure implementation.
source to share
I'm not familiar with Agda, but I think it looks like Coq in this particular case, and I can answer the related question for Coq. Both languages are based on intuitionistic type theory with inductive types .
In intuitionistic-type theory, recursion principles can be derived from a fairly general fixed-point combinator as well as dependent pattern matching. Pattern matching is not enough: while it breaks an inductive type, pattern matching prevents recursive functions of that type from being written. Example from Wikipedia:
add zero n = n
add (suc n) m = suc (add n m)
The fact that this definition is well formed does not require an induction principle on ℕ. But in addition to the pattern matching formed on the first argument add
, it requires a rule indicating that the recursive call in the second case is well-formed.
Given 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)
source to share