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.

  • I expect that it is, and always will remain inscrutable to practicing programmers. At best, we might get faster compilers or magical black boxes that take advantage of the mathematical-fu. – Telastyn Nov 10 '14 at 22:58
  • Haha this is what I've been thinking so far too. I am still wondering though, is this the answer or is there something beyond what you've said? For example, could databases benefit from this? Or anything like that. – Lance Pollard Nov 11 '14 at 0:34
  • 1
    I have no idea. I read the abstract and promptly dropped it into the bucket for inscrutable academic mumbo-jumbo. – Telastyn Nov 11 '14 at 1:11
  • recommended reading: How do I explain ${something} to ${someone}? – gnat Nov 11 '14 at 6:27
  • 4
    @Telastyn: If you download a book in Portuguese it will also be inscrutable as long as you haven't tried to learn the language. Why publicly denounce Portuguese books by the derogatory term mumbo-jumbo? Gödels motivation for introducing primitive recursive functions was extremely academic, in particular because the world didn't even run any programs in the 30's. I don't think just because one is a practicing programmer, academic topics will "always remain inscrutable" to your capabilities. – Nikolaj-K Apr 17 '15 at 13:56

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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