2
$\begingroup$

I've read here that in HoTT, compilers could swap out less efficient representations of data for more efficient ones and I'm wondering whether my interpretation of that statement is correct.

Say we have two different ways of representing the natural numbers, unary (zero and successor) and binary. Here is a function that checks evenness on the former representation:

even : UnaryNat -> Bool
even zero = true
even (succ zero) = false
even (succ (succ n)) = even n

If we then have an isomorphism between the unary and binary representations, we trivially get an evenness function for the binary representation "for free", simply by converting a given binary natural number to a unary one, applying the even function, and converting the result back to the binary representation. Obviously, this is not very efficient, and we also don't need HoTT for this.

A better way to check whether a binary natural number is even would be to check if its least significant digit is a zero. My question is: Could we derive this more efficient algorithm for binary natural numbers from our definition of evenness for unary natural numbers using HoTT? If so, would this also be possible for other data types? I haven't studied any HoTT yet and since its appears to be a pretty complex subject I would like to find out whether it's as exciting as I think it is. Thanks!

$\endgroup$
4
  • $\begingroup$ Not exactly the same, but there's quite some research on how to get rid of all the proof-stuff in dependently typed languages, which isn't needed at runtime and can be erased. Cf. idris2.readthedocs.io/en/latest/updates/updates.html#erasure. $\endgroup$ – phipsgabler Jun 7 '20 at 10:36
  • $\begingroup$ @phipsgabler How does that relate to the topic of this question? $\endgroup$ – malte-v Jun 7 '20 at 10:57
  • $\begingroup$ In that it is about a compiler using type theory to make dependently typed programs more efficient? $\endgroup$ – phipsgabler Jun 7 '20 at 13:03
  • 1
    $\begingroup$ @phipsgabler Idris 2 uses Quantitative Type Theory for erasing compile-time terms. This question is about using Homotopy Type Theory to derive better algorithms. Two different type theories, two different optimizations. I don't see the connection. $\endgroup$ – malte-v Jun 7 '20 at 13:07
3
$\begingroup$

You ask if we could derive a more efficent way to compute even? Yes, we could of course. The point however is that compilers could not.

Having a compiler automatically perform very fancy optimization techniques is a hard problem. In fact, if you ask for too much the problem may become undecidable, and for almost all interesting cases at least extremely hard. Even just asking whether two simple types are isomorphic quickly leads to open research questions.

What we have gained from HoTT is not a magic wand, but rather a formalism that provides a very good and structured way of thinking and reasoning about isomorphism, equivalence and equality in general. One can think easily enough about "small scale" notion of equivalence, for example when we focus just on one particular data structure, such as a dictionary, but it's a whole other matter to be able to talk about all notions of equivalence at the same time.

In your particular case it is easy to see what it would mean to have an equivalence between two implementations of natural numbers. But how about equivalence of large software components? Or equivalence of implementations of partial differential equation solvers? How do we even being to think about it? HoTT has an answer.

$\endgroup$

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.