4 ms·

This makes me better appreciate why Homotopy Type Theory might be useful in a type system: It allows for a simple but inefficient version of a type to coexist w

This makes me better appreciate why Homotopy Type Theory might be useful in a type system: It allows for a simple but inefficient version of a type to coexist with a faster variant of that type. The type system could be made aware that those are two different ways of representing the same mathematical object. Have GA people tried anything along this direction?

nextaccountic 3y ago
> This makes me better appreciate why Homotopy Type Theory might be useful in a type system: It allows for a simple but inefficient version of a type to coexist with a faster variant of that type. The type system could be made aware that those are two different ways of representing the same mathematical object. Okay I've been thinking a lot about this problem of multiple representations. Is there any language that actually uses this equivalence of types as a way to select between different ways to represent the same data? An use case would be something like, a smart list type that will select between a growable linear vector, a copy on write persistent list, etc. and select between them based on a) which operations you do to the list (for example, if you use it in a linear fashion, it doesn't need to be persistent), and b) user annotations in code. Another use case is to define unary peano numbers like data Nat = Zero | Succ Nat and have the type system understand automatically this doesn't need to be stored like this, and is in fact the same as a (big) int. Some languages have special-casing for this, but this could work generically as well.
- ogogmad 3y ago
  Cubical Agda is an example of a "programming language" which uses HoTT features: https://agda.readthedocs.io/en/v2.6.0/language/cubical.html https://agda.readthedocs.io/en/v2.6.0/language/cubical.html It's actually a proof assistant, but you can still write code in it - and perhaps even export it to code in other languages. Regarding the "smart" features you suggested, those sound interesting, but I'm not aware of any language having them. Could be useful.

nextaccountic 3y ago

> This makes me better appreciate why Homotopy Type Theory might be useful in a type system: It allows for a simple but inefficient version of a type to coexist with a faster variant of that type. The type system could be made aware that those are two different ways of representing the same mathematical object. Okay I've been thinking a lot about this problem of multiple representations. Is there any language that actually uses this equivalence of types as a way to select between different ways to represent the same data? An use case would be something like, a smart list type that will select between a growable linear vector, a copy on write persistent list, etc. and select between them based on a) which operations you do to the list (for example, if you use it in a linear fashion, it doesn't need to be persistent), and b) user annotations in code. Another use case is to define unary peano numbers like data Nat = Zero | Succ Nat and have the type system understand automatically this doesn't need to be stored like this, and is in fact the same as a (big) int. Some languages have special-casing for this, but this could work generically as well.

ogogmad 3y ago
Cubical Agda is an example of a "programming language" which uses HoTT features: https://agda.readthedocs.io/en/v2.6.0/language/cubical.html https://agda.readthedocs.io/en/v2.6.0/language/cubical.html It's actually a proof assistant, but you can still write code in it - and perhaps even export it to code in other languages. Regarding the "smart" features you suggested, those sound interesting, but I'm not aware of any language having them. Could be useful.