2
$\begingroup$

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

Improve this question
$\endgroup$
5
  • $\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$
    – Andrej Bauer
    May 25 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$
    – Andrej Bauer
    May 25 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$
    – Shiranai
    May 25 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$
    – Shiranai
    May 25 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$
    – Andrej Bauer
    May 26 at 14:11

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.