<p>Here is <a href="http://spire-lang.org/blog/2014/08/04/inductive-recursive-descriptions" rel="nofollow noreferrer">one article</a> that discussed induction-recursion. Here's their code:</p>
<pre><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 ⟧
</code></pre>
<p>There is a related feature in Agda called <a href="https://github.com/agda/agda/issues/2858" rel="nofollow noreferrer">interleaved mutual definition</a> which is an even stronger variant of induction-recursion. You can look at their examples.</p>
<p>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.</p>

CC BY-SA 4.0
2021-06-08T22:31:17.010Z
2021-06-09T03:32:55.350Z
2021-06-09T03:32:55.350Z
ice1000
<p>I know of only two uses of <a href="https://en.wikipedia.org/wiki/Induction-recursion" rel="nofollow noreferrer">induction-recursion</a>:</p>
<ol>
<li>Encoding universes as a type, <a href="https://agda.readthedocs.io/en/v2.6.3/language/mutual-recursion.html" rel="nofollow noreferrer">as shown in the Agda docs for recursion</a></li>
<li>Encoding <a href="https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf" rel="nofollow noreferrer">Finite sets</a> as shown in Conor Mc'Bride's &quot;datatypes of datatypes&quot;, Chapter 6, Induction-Recursion. I don't understand the point of this example, so I feel like I'm missing something.</li>
</ol>
<p>I'd like answers to be examples of where induction-recursion is used. To quote Halmos:</p>
<blockquote>
<p>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.</p>
</blockquote>

<dependent-type><agda>
Example use cases for induction-recursion
Siddharth Bhat
# Example use cases for induction-recursion

(Asked by: username_0 on 2021-06-08)

I know of only two uses of [induction-recursion](https://en.wikipedia.org/wiki/Induction-recursion):

1. Encoding universes as a type, [as shown in the Agda docs for recursion](https://agda.readthedocs.io/en/v2.6.3/language/mutual-recursion.html)
2. Encoding [Finite sets](https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf) 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.

**Tags:** dependent-type, agda


---

## 1 answers

### Answer by username_1 on 2021-06-08. Score: 6 | Accepted answer

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.


---

