What are the practical implications of homotopy type theory in programming?

Question

I am just beginning to learn Haskell, after coming from the JavaScript/Ruby worlds. I have come across https://github.com/HoTT and the Homotopy Type Theory book, which I am very eager to read.

However, I will be learning the math and type theory concepts as I go, so it seems like it will take a long time before I understand what homotopy type theory will mean to a practicing programmer.

Could you describe what impact homotopy type theory will have on programming in practice, for a layman? For example, will it make certain things easier to easier to write? If so, which things? Or will it allow for you to do new things in programming that weren't previously possible? If so, which things?

Thanks, very much looking forward to wrapping my head around it at a more basic level.

Answer 1

One of the powerful things compilers are able to do during their optimization phase is to swap out inefficient representations for equivalent ones. For example, in Haskell you could use a lazy list to compute a sum of numbers, but the GHC Haskell compiler will recognize that this is equivalent to using iteration with a temporary variable. That way, you get to program against a simple abstraction that's easy to reason about, while your executable takes advantage of a representation better suited to the hardware platform (and that happens to be much harder to reason about at scale).

However, equivalences known to the compiler are mostly restricted to well known and researched data structures, such as stream fusion for lists. You could define your own equivalences in source code (using a pair of conversion functions that compose to identity in either direction), but you'd have to apply them manually, and it can get tricky to choose the right type to use in all places in order to avoid excessive conversions.

Now let's imagine a world where you get to define "higher inductive types", say a canonical lookup map. This type has several constructors for the various kinds of maps: binary search, AVL, red-black, Trie, Patricia, etc. Along with the typical data constructors, you also define an equivalence type capturing possibly multiple conversions between these representations, where different conversions offer varying dimensions of efficiency (i.e., time vs. memory).

What if the compiler were able to use this notion to transparently rewrite map representations, the same way it can do today with list fusion? Meanwhile, in your code you get to work with the construction that is simplest to reason about (and makes proof work easier, if you are in such an environment). This may sound just like an abstract interfaces with multiple implementations, but it includes the freedom to choose any implementation and have the compiler transparently substitute another as needed, without affecting the meaning of the program.

HoTT gives us a type theoretic foundation to justify this fancy rewriting mechanism and these richly defined types, because it promotes the notion of equivalence to being equivalent to equality. It remains to be seen how this will actually play out in practice, but it gives us the theoretical framework on which to base future work.