Hacker News Reader

> Keep in mind that cubical type theories are somewhat complex (in sheer amount of code),

And in computational efficiency, no? I think making an efficient implementation of a cubical type theory is still an ongoing effort.

View on HN

Yep, there is that, too. You lose the ability to erase types when compiling, so you must have a representation of types at runtime, and you need to pattern-match on them. That inefficiency won't show up in normal programs, though, but if, for some reason, your program depends on a program that depends on a program (...) that uses Paths and `transp`, then you'll have to pay. This is kind of unavoidable and not that bad, though. We're more worried about the complexity of the built-in `transp` that must be part of Core. Currently, our core has only two computational primitives: beta-reduction and dereference. These are orders of magnitude simpler than `transp`, which looks extremely artificial. I'm very confident there are simpler primitives that would allow `transp` to be derived.

Reply on news.ycombinator.com