6 ms·
Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll
by Kutta 11y ago
Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation.
The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum containing True and False. But we could rename the values to Foo and Bar and it would be still a fine implementation, because it's easy to convert between the two representations. We can imagine more far-fetched representations too, with more complicated conversion functions.
But in type theory, if two types are equal, then we can freely substitute one for another in any context! For example, if we have a function "Bool -> Bool", and we know that Bool is equal to Bool2, then we can coerce the function to type "Bool2 -> Bool2".
Imagine a complex program that uses a complex piece of data type. If we can provide a correct conversion function to another type (i. e. prove that the type is equivalent to another one), then the univalence axiom can take the conversion function and our program as input, and spits out a new program that uses the new data type, and also preserves all properties of the program. By our current standards of generic programming, this is just insane!
Now, the issue is that currently we don't actually have a computational interpretation for the univalence axiom, so the above magic doesn't yet work. But there is meaningful progress towards that, and there are already some experimental implementations that can do some magic, for example this one:
https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt
- YorkshireSeason 11y agoWhat is the state of the art of the research on the computational interpretation of univalence? What's working, what's not working? I seem to remember that A Jeffrey said not too long ago that he had a working interpretation.
- gallabytes 11y agoA lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.
- igravious 11y agoWhen you think about it we do have a computational meaning and interpretation for the univalence axiom. Your very comment was such an exposition! What we perhaps don't have is an automated implementation of your exposition. What you're talking about is typecasting where all the terms of one type map to all the terms of another type. And that once shown this the machine could perform type substitution kind of like how type inference works now. (And maybe the machine wouldn't always have to be shown??) Neat idea. Automatic type inference is pretty powerful. Automatic type substitution could be just as powerful perhaps.
- tmvphil 11y agoI must be missing something. A proof that Bool and Bool2 are equal is a bijection f :: Bool -> Bool2. So given any g :: Bool -> Bool we have (f . g . f^-1) :: Bool2 -> Bool2. So it seems trivial.
- jules 11y agoYes, that's pretty much it. Doing this systematically for all types including dependent types that quantify over Bool, as well as for user defined higher inductive types is another matter.
- Kutta 11y agoA more interesting example: substitute natural numbers with binary trees. After all, they're equivalent. Now univalence would have to implement the binary tree analogue for every function on naturals, in a way that preserves semantics with respect to our conversion function.
- kazinator 11y agoIn C, you can convert back and forth between void * and some integer type, aliased as intptr_t since C99, so they must be equal under the univalence axiom. Ah, "nuclear weapon" ... gotcha!
- rndn 11y agoDoesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is undecidable)?
- gallabytes 11y agoWhy would it do that? Univalence is unrelated to the halting problem. What the univalence axiom says is that you can treat types you have proven isomorphic as equal.
- eli_gottlieb 11y agoNo. Homotopy Type Theory is a total language, so even type-level programming simply has to terminate, or the proof-checker won't accept it. Proving that nontrivially recursive programs terminate can be a bugger.
- jonsterling 11y agoYou do not in general decide whether two types are equivalent. You prove it...
- cbd1984 11y ago> The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). So strings are equivalent to everything, and vice-versa. > Now, the issue is that currently we don't actually have a computational interpretation for the univalence axiom JSON? Sexps?