3 ms·

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 los

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 lists of key/value pairs, etc.), then cast these to more efficient types (e.g. machine words, arrays, tries, etc.) for the final program. It's still ongoing, and a naive approach would simply lead to a bunch of conversion functions being scattered around (making the program even slower), so a smart approach would be needed, e.g. where compilers can fuse away these conversions.

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 ago
  That 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 ago
  That'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.
jerf 6y ago
I remember when that first came out. I have not checked in on it in a while. Do you have any links to communities/reddits/etc working with that? (/r/haskell was very excited for a while, but then the energy went somewhere else, and I don't know where.) One of the things I only alluded to in my third paragraph, but very much had this sort of thing in mind, is that it's going to take a lot of type work and a lot of thinking in properties (like Traversable, Functor, etc. in Haskell) to make this work out well, because a lot of these rewrites to underlying representation will have manifestations at the property level (this array is now Traversable but no longer RandomAccessible, etc.).

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 ago
That 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 ago
That'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.

jerf 6y ago

I remember when that first came out. I have not checked in on it in a while. Do you have any links to communities/reddits/etc working with that? (/r/haskell was very excited for a while, but then the energy went somewhere else, and I don't know where.) One of the things I only alluded to in my third paragraph, but very much had this sort of thing in mind, is that it's going to take a lot of type work and a lot of thinking in properties (like Traversable, Functor, etc. in Haskell) to make this work out well, because a lot of these rewrites to underlying representation will have manifestations at the property level (this array is now Traversable but no longer RandomAccessible, etc.).