I know of only two uses of induction-recursion:

  1. Encoding universes as a type, as shown in the Agda docs for recursion
  2. Encoding Finite sets as shown in Conor Mc'Bride's "datatypes of datatypes", Chapter 6, Induction-Recursion. I don't understand the point of this example, so I feel like I'm missing something.

I'd like answers to be examples of where induction-recursion is used. To quote Halmos:

A good stack of examples, as large as possible, is indispensable for a thorough understanding of any concept,and when I want to learn something new, I make it my first job to build one.


Here is one article that discussed induction-recursion. Here's their code:

  data Lang : Set
  ⟦_⟧ : Lang → Set

  data Lang where
    Zero One Two : Lang
    Pair Fun Tree : (A : Lang) (B : ⟦ A ⟧ → Lang) → Lang

  ⟦ Zero ⟧ = ⊥
  ⟦ One ⟧ = ⊤
  ⟦ Two ⟧ = Bool
  ⟦ Pair A B ⟧ = Σ ⟦ A ⟧ λ a → ⟦ B a ⟧
  ⟦ Fun A B ⟧ = (a : ⟦ A ⟧) → ⟦ B a ⟧
  ⟦ Tree A B ⟧ = W ⟦ A ⟧ λ a → ⟦ B a ⟧

There is a related feature in Agda called interleaved mutual definition which is an even stronger variant of induction-recursion. You can look at their examples.

Here is one indirect example (which is actually induction-induction): the definition of a dependent type theory. The definitions of context, type, and term are mutually recursive as terms are only defined in a context (so the definition of term requires context), while context contains types, and in a dependent type systems types are just terms. So here we have an inductive-inductive definition if term and context are defined as inductive types. This is similar to induction-recursion to some extent.


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.