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.)

  • 1
    $\begingroup$ 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. $\endgroup$ May 25, 2023 at 22:12
  • 1
    $\begingroup$ I took the liberty of editing the question. Please feel free to revert my changes if you dislike them. $\endgroup$ May 25, 2023 at 22:41
  • $\begingroup$ @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. $\endgroup$ May 25, 2023 at 23:10
  • $\begingroup$ (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.) $\endgroup$ May 25, 2023 at 23:20
  • 1
    $\begingroup$ 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. $\endgroup$ May 26, 2023 at 14:11


Your Answer

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

Browse other questions tagged or ask your own question.