10
$\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?

$\endgroup$
  • $\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 Mar 23 '18 at 20:10
  • $\begingroup$ @Gilles My understanding was that Coq didn't use eliminators, but instead uses separate match and (guarded) fix operators. $\endgroup$ – jmite Mar 23 '18 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 Mar 24 '18 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 Mar 24 '18 at 12:11
8
$\begingroup$

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

$\endgroup$
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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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