4 ms·
And how does it compare to Arend? Does anybody know? Are there any other HOT based languages out there? (Agda seems to have also some support for the "cubic ve
by still_grokking 4y ago
And how does it compare to Arend? Does anybody know?
Are there any other HOT based languages out there? (Agda seems to have also some support for the "cubic version"; whatever this means, I'm actually clueless).
- jshaqaw 4y agoCubical type theory is a way to get to a purely constructive foundation for Homotopy Type Theory. Super cool stuff from a foundations of math perspective and has some surprising applications to topological quantum computing but if it isn’t your rabbit hole you can probably not pay too much attention to it.
- still_grokking 4y agoThe whole "foundations of math" part is extremely exciting! But I'm not an mathematician so I don't understand much (if anything). More in the programming languages "department" of interests. But if something is "good enough" to describe whole math it could be useful for getting strong guaranties about programs, I guess. So I would be quite interested how this HOT stuff could be useful in practice. What could type systems based on this enable? My limited understanding is that you get additionally "paths" between types and type constructor which denote equivalence between them. But I have no clue what one could do with that (besides doing math, of course).