Earlier quoted context omitted.
The idea of "univalence", being pursued in Homotopy Type Theory (AKA HoTT), is that isomorphic types (i.e. we can convert back and forth without information loss) are equal , and hence one can be used in place of the other. The dream scenario is to write all of our libraries and application code using types that are the most straightforward (e.g. counting in unary, mapping over linked-lists, looking up values from li…
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 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.