Цитата для памяти
Как лучше делать сопоставление с образцом в языке с зависимыми типами?
Coq's inductive types are implemented using separate "match" and "fix" constructions, which allow for deep matching, mutual matching, etc. Similarly, Agda allows function definition by pattern matching with a separate termination checker. However, this approach is only justified semantically by translating it into eliminators, and it is hard to make sense of for higher inductive types. On the other hand, deep matching is very useful for functional programmers.
One potential solution to this problem is the approach used in Epigram, where there is a "pattern matching" syntax that is extensible rather than baked into the system. Any term whose type has "the form of an induction principle" can be used to justify a pattern-matching syntax. Thus, although each inductive definition comes with its defining induction principle, the user can prove their own new induction principles (such as for deep matching, mutual recursion, etc.) and then use those elimination rules with the same sort of pattern-matching syntax.
This may be especially nice for higher inductive types, where preliminary experiments suggest that there can be meaningful notions of "deep recursion" and "mutual recursion" in particular cases, but it seems difficult to give one general formulation of such principles.
Originally posted at http://deniok.dreamwidth.org/47054.html. Feel free to comment here or there.