What are the applications of homotopy type theory to everyday programming?

I know of only two applications, neither of which I understand:

Is there a capsule summary of how HoTT is relevant to these problems?

Is there a general kind of programming problem for which HoTT is suited? Based on the applications so far, is it likely that future applications will all have to do with program efficiency? Or might there be applications to distributed systems, for example?

Higher inductive types strike me as the most obviously "new" thing from a programmer's point of view. Is there a capsule summary of why programmers might use higher inductive types? Do these applications only have to do with program correctness, or do they also give us the ability to solve problems differently?

I know it's early days and that we probably don't know what the applications may be, but it's also likely that more is known now than several years ago when the articles above were written.


Found one more application! When implementing APL/J's notion of "rank" (generalized operations over multidimensional arrays), it can help to have a more flexible notion of equality. See Section 3.1 of "Multi-dimensional Arrays with Levels" by Artjoms Šinkarovs

Thanks James Wood for pointing me toward this paper



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.