3 ms·

I think that's one downside to that kind of implementation. Computational performance and everything either requiring heap allocation or 2^n values, most of whi

I think that's one downside to that kind of implementation. Computational performance and everything either requiring heap allocation or 2^n values, most of which which are zero are others problems. My implementation generates a struct for each grade, even and odd grades (which perform transformations), and then a multivector type with everything. If you mistakenly add a scalar and a vector, you'll immediately see unexpected types in your inline type hints. The downside to my approach is a combinatorial explosion in the number of types and operations between them. Anyone know a seamless way to do lazy code generation in Rust?

ogogmad 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. 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.

ogogmad 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. 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.