Not only do the dependent datatypes code up more precisely the data we wish to capture, excluding redundant or ill-formed elements at the typechecking stage (and that is reason enough to use them), they also buy us more structural programs, because we can compute over the indices as well as the terms.

The elimination rule technology developed to support LEGO programming in the pattern matching style invites exploitation for eliminating things other than datatypes. I think the examples in this talk motivate strongly the use of elim rules for `outward-looking' specifications of programs. In particular elimination rules for function applications need not reflect their equational behaviour at the computational level, and hence they allow changes of implementation within components of modular developments. (See also Henrik Persson's work on polynomial rings in Agda.)

Next: where now? | Prev: base cases | Up: contents