<p>By &quot;practical applications&quot; I mean in usual programming/industry. I am particularly interested in cases where the inductive-inductive types cannot be easily replaced by inductive-recursive types.</p>
<p>One example that comes to mind is writing other programing languages. What are some others?</p>
<p>I would consider the following use of inductive-recursive types to be somewhat practical:</p>
<pre><code>module _ (A : Set) (_#_ : A → A → Set) where
  data Dlist : Set
  Fresh : Dlist → A → Set

  data Dlist where
    nil : Dlist
    cons : (b : A) (u : Dlist) (b' : Fresh u b) → Dlist

  Fresh nil a = 
  Fresh (cons b u b') a = (b # a) × Fresh u a
</code></pre>
<p>(Though it's arguable if it's just easier to use plain inductive types with extra data.)</p>

CC BY-SA 4.0
2023-05-25T22:12:23.050Z
At the very least, if you don't want to turn off people and have them downvote you (llike I did), try to ask more positively: "*In addition* to such-and-such uses of inductive-inductive types, what *other* uses are there, especially ones that can have practical value?" Using derision quotes, prohibiting people from mentioning certain uses etc., that's not a good way to communicate.
Andrej Bauer
CC BY-SA 4.0
2023-05-25T22:41:00.667Z
I took the liberty of editing the question. Please feel free to revert my changes if you dislike them.
Andrej Bauer
CC BY-SA 4.0
2023-05-25T23:10:26.480Z
@AndrejBauer Thanks for the changes, it was not my intention to ask negatively. I agree this is a much better way to ask, and will do so in the future.
Fernando Chu
CC BY-SA 4.0
2023-05-25T23:20:08.017Z
(Also, my quotes were not meant to be used for derision, but to acknowledge that what is practical and what is not is fuzzy at best. In retrospective, I see now that my intended meaning was not clear at all. I apologize for any misunderstandings.)
Fernando Chu
CC BY-SA 4.0
2023-05-26T14:11:17.430Z
I always assumed your question was well-meaning. Now it's my turn to apologize for making rather stern comments, I could have been more welcoming too.
Andrej Bauer
<soft-question><dependent-type>
What are some practical applications of inductive-inductive types?
Fernando Chu
# What are some practical applications of inductive-inductive types?

(Asked by: username_0 on 2023-05-25)

By "practical applications" I mean in usual programming/industry. I am particularly interested in cases where the inductive-inductive types cannot be easily replaced by inductive-recursive types.
One example that comes to mind is writing other programing languages. What are some others?
I would consider the following use of inductive-recursive types to be somewhat practical:
module _ (A : Set) (_#_ : A → A → Set) where
  data Dlist : Set
  Fresh : Dlist → A → Set

  data Dlist where
    nil : Dlist
    cons : (b : A) (u : Dlist) (b' : Fresh u b) → Dlist

  Fresh nil a = 
  Fresh (cons b u b') a = (b # a) × Fresh u a

(Though it's arguable if it's just easier to use plain inductive types with extra data.)

**Tags:** soft-question, dependent-type

> **Comments:**
> **username_1**: At the very least, if you don't want to turn off people and have them downvote you (llike I did), try to ask more positively: "*In addition* to such-and-such uses of inductive-inductive types, what *other* uses are there, especially ones that can have practical value?" Using derision quotes, prohibiting people from mentioning certain uses etc., that's not a good way to communicate.  
> **username_1**: I took the liberty of editing the question. Please feel free to revert my changes if you dislike them.  
> **username_0**: @AndrejBauer Thanks for the changes, it was not my intention to ask negatively. I agree this is a much better way to ask, and will do so in the future.  
> **username_0**: (Also, my quotes were not meant to be used for derision, but to acknowledge that what is practical and what is not is fuzzy at best. In retrospective, I see now that my intended meaning was not clear at all. I apologize for any misunderstandings.)  
> **username_1**: I always assumed your question was well-meaning. Now it's my turn to apologize for making rather stern comments, I could have been more welcoming too.  

---

## 0 answers

