12
$\begingroup$

In dependently-typed programming, there are two main ways of decomposing data and performing recursion:

  • Dependent pattern matching: function definitions are given as multiple clauses. Unification ensures that all omitted cases are impossible, and an external solver ensures that recursion is well-founded.
  • Eliminators: Each inductive datatype $D$ has an associated constant $E_D$, which acts as an induction principle, and as recursive function that decomposes values of type $D$. These are more verbose, but have the advantage of being total (all cases are covered by $E_D$) and terminating by construction.

I've seen eliminators for common datatypes, like $Nat$, where the eliminator is basically mathematical induction, or $List$, where the eliminator is basically a fold.

I've been reading several papers on dependent pattern matching, and many refer to type theories in which datatypes can be defined, and eliminators are provided by the theory. For example, Eliminating Dependent Pattern Matching describes how UTT is based on eliminators, and how pattern matching can be converted to elimination in the presence of axiom $K$. My understanding is that, once a datatype is defined, the theory provides the eliminator.

What I haven't found (or at least, haven't recognized if I've seen it) is a good description of how one can derive the eliminators, both their types and their semantics.

Can someone point me to a reference that describes how one can obtain an eliminator from the definition of a datatype?

Improve this question
$\endgroup$
4
  • $\begingroup$ I'm sure there's a description in the calculus of constructions or Coq literature (for strictly positive types — Coq's eliminators on more complex types aren't fully general). $\endgroup$
    – Gilles 'SO- stop being evil'
    Commented Mar 23, 2018 at 20:10
  • $\begingroup$ @Gilles My understanding was that Coq didn't use eliminators, but instead uses separate match and (guarded) fix operators. $\endgroup$
    – Joey Eremondi
    Commented Mar 23, 2018 at 20:27
  • 3
    $\begingroup$ The core language doesn't use eliminators, but when you define a type, Coq generates an eliminator which is defined in terms of fix and match. I don't have a reference at hand, but I know I've read something about how this eliminator is generated. cs.stackexchange.com/questions/104/… may be of interest. $\endgroup$
    – Gilles 'SO- stop being evil'
    Commented Mar 24, 2018 at 8:17
  • $\begingroup$ For any inductive type T, Coq defines an induction principle T_ind which is a dependent eliminator. This is defined in terms of recursion and pattern matching, but you could in principle assume it as a new constant having the same type (with the same semantics). $\endgroup$
    – chi
    Commented Mar 24, 2018 at 12:11

2 Answers 2

Reset to default
8
$\begingroup$

The canonical reference for this is Peter Dybjer, Inductive Families, which gives a pretty comprehensive treatment of inductive families based on eliminators.

Improve this answer
$\endgroup$
0
6
$\begingroup$

You might find some of our recent papers on this useful, as we derive eliminators for lambda-encoded datatypes. For example, see this one for generic derivation of eliminators, and this one for the basic technique applied just to the Nat type.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.