3 ms·
HoTT changes what equal means. In order for univalence to work you must be comfortable with arbitrary code running to perform the necessary substitutions. Isomo
by voxl 6y ago
HoTT changes what equal means. In order for univalence to work you must be comfortable with arbitrary code running to perform the necessary substitutions. Isomorphism isn't for free, you can do some fancy cast-conversions (where cast is an identity function) that has been explored in generic zero-cost reuse [1] but this is not HoTT and uses essentially an UIP equality (which is inconsistent with HoTT).
Your usage of the word "cast" in the second paragraph is a misnomer, because no systems programmer is going to want to perform an expensive transporation in HoTT!
[1] https://arxiv.org/abs/1803.08150 https://arxiv.org/abs/1803.08150
- rocqua 6y agoThat sounds like, for performance reasons, you want control over the actual types used. But you could eliminate those changes from affecting the semantic representation of your program. Or at the very least with an easy check that the optimization doesn't affect your semantics.
- chriswarbo 6y agoThat's what I was getting at w.r.t. naive vs smart implementations. The point of univalence is that, from a logical/functional perspective, `slowFoo(slowX)` is indistinguishable from `fastToSlow(fastFoo(slowToFast(slowX)))`. Applying this to composite expressions will produce lots of calls like `slowToFast(fastToSlow(x))` which can be optimised down to `x`. The problem, of course, is that we can't enforce this within the logic (since those expressions are indistinguishable), so we must rely on compiler optimisations (i.e. deforestation/fusion). That link looks interesting, but appears to be more about re-using the same computational-content/runtime-representation for multiple compile-time/proof-context semantics (akin to McBride's "ornaments"), which seems more like a dual problem to that of swapping out slow representations for fast ones.