<p>As far as I know, the software industry remains blissfully unaware of dependent types in general, and of inductive-inductive types and inductive-recursive types in particular. Intersection types have barely come to the attention, and only in the most superficial, object-oriented forms.</p>
<p>I would like very much to see an explanation about how dependent types help programmers write better web servers, databases, or graphical user interfaces. So far, the only attempt to bring dependent types a little closer to industry relevance is the &quot;Ur/Web&quot; language by A. Chlipala. <a href="https://github.com/urweb/urweb" rel="nofollow noreferrer">https://github.com/urweb/urweb</a></p>

CC BY-SA 4.0
2024-03-21T15:44:13.440Z
2024-03-21T15:44:13.440Z
winitzki
<p>Since this question got not many answers Im hoping asking again could convey that this has some importance.</p>
<p>Anyway so in undergraduate education, I was working on research to implement dependent-intersection types. These type encodings are specifically used to encode inductive-inductive and inductive-recursive types. I wanted to see if this dependent intersection can be implemented as a straightforward way by extending plain old Sigma Types (Dependent types). One of the key extra ingredients (beyond dependent functions) is dependent intersection types which allow us to layer multiple additional specifications about what code does after it has already been defined with an original type.</p>
<p>To conclude and summarize, when I think of dependent intersection types here's what I think:</p>
<ol>
<li>The type itself defines the structure or nature of data.</li>
<li>The property associated with that type provides additional information or constraints about the data in terms of its relationship with other data or its adherence to certain rules or conditions as we saw with the induction property on booleans.</li>
</ol>
<p>So now im just curious what would some practical applications of inductive-inductive and inductive-recursive types be in the industry?</p>

<type-theory><dependent-type><calculus-of-constructions>
What are some practical applications of inductive-inductive and inductive-recursive types?
AnonymousThunk
# What are some practical applications of inductive-inductive and inductive-recursive types?

(Asked by: username_0 on 2024-03-20)

Since this question got not many answers Im hoping asking again could convey that this has some importance.

Anyway so in undergraduate education, I was working on research to implement dependent-intersection types. These type encodings are specifically used to encode inductive-inductive and inductive-recursive types. I wanted to see if this dependent intersection can be implemented as a straightforward way by extending plain old Sigma Types (Dependent types). One of the key extra ingredients (beyond dependent functions) is dependent intersection types which allow us to layer multiple additional specifications about what code does after it has already been defined with an original type.

To conclude and summarize, when I think of dependent intersection types here's what I think:

1. The type itself defines the structure or nature of data.
2. The property associated with that type provides additional information or constraints about the data in terms of its relationship with other data or its adherence to certain rules or conditions as we saw with the induction property on booleans.

So now im just curious what would some practical applications of inductive-inductive and inductive-recursive types be in the industry?

**Tags:** type-theory, dependent-type, calculus-of-constructions

---

## 1 answers

### Answer by username_1 on 2024-03-21. Score: 1

As far as I know, the software industry remains blissfully unaware of dependent types in general, and of inductive-inductive types and inductive-recursive types in particular. Intersection types have barely come to the attention, and only in the most superficial, object-oriented forms.

I would like very much to see an explanation about how dependent types help programmers write better web servers, databases, or graphical user interfaces. So far, the only attempt to bring dependent types a little closer to industry relevance is the "Ur/Web" language by A. Chlipala. <https://github.com/urweb/urweb>


---

