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?


1 Answer 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


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.