3 ms·

Yes, that is the gist of it: we can't do this. Negative results need to be communicated, too! But that's not all there is to it. The fact we do present a type a

Yes, that is the gist of it: we can't do this. Negative results need to be communicated, too! But that's not all there is to it. The fact we do present a type almost identical to Path and Interval with self-types, and the fact that such type has almost identical proofs of relevant theorems (like `funext`), yet no proof of the very important `transp`, does make a strong hint that further additions to the core are necessary. It also gives us a direction, and even some hints of how the implementation could be simplified. Keep in mind that cubical type theories are somewhat complex (in sheer amount of code), but there is no evidence they can't be simplified further. Kind has a goal to keep its core as simple as possible. Being able to express all the Coq inductive proofs in a 700-LOC core is a miracle, isn't it? > I suspect you will never be able to! That makes no sense! In the worst case we could just go ahead and implement CubicalTT on Kind's Core. We just don't want to commit to that until we're sure there isn't a way to simplify it, even if slightly.

creata 5y ago
> 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.
- LangMakers 5y ago
  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.
NieDzejkob 5y ago
Does the 700 LoC core include a termination checker? If I understood your other comments correctly, that's planned for later, no? If so, I don't think this is a very apples-to-apples comparison.

creata 5y ago

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

LangMakers 5y ago
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.

NieDzejkob 5y ago

Does the 700 LoC core include a termination checker? If I understood your other comments correctly, that's planned for later, no? If so, I don't think this is a very apples-to-apples comparison.