Very bad performance when filling high dimensional cubes

[3abc]

In cubical mode I tried to use hcomp to fill a high dimensional cube. The performance is very bad.

For the 6d-cube it takes about 100s to type check. But for the 7d-cube it simply eats up more than 16 GB RAM and never ended (my computer died). Both file are python generated.

As a (maybe unfair) comparison, a similar 7-cube in redtt takes less than 2 seconds to type check.

[mortberg]

Very interesting!

Can you redo the redtt experiment with iterated path types so that we can see if it's the extension types that are helping or not? An obvious difference is that the Agda version of the 7d cube takes over 2000 arguments while the redtt one only takes about 20.

[3abc]

Can you redo the redtt experiment with iterated path types so that we can see if it's the extension types that are helping or not? An obvious difference is that the Agda version of the 7d cube takes over 2000 arguments while the redtt one only takes about 20.

I do want to try that, but I cannot find any document for redtt. Do you know any?

[mortberg]

I do want to try that, but I cannot find any document for redtt. Do you know any?

I don't think there is any detailed documentation yet. But the Path types are defined at the top of

https://github.com/RedPRL/redtt/blob/master/library/prelude/path.red

(their path type is our ≡ and their pathd is our PathP type)

[3abc]

redo the redtt experiment with iterated path types

I just did. Now it's a lot slower. 5d-cube took 60 seconds, and I expect 6d-cube to take 20 minutes and for 7d-cube maybe 6 hours. I'm running them now, the memory consumption is only about 100 MB at this moment.

So extension types do help. But cubical Agda's memory consumption is still an issue.

[3abc]

The 6d-cube for redtt is not done yet, after 100 minutes. So maybe it will take days for 7d-cube to run (given that 5d -> 1 minute, 6d -> at least 100 min, if 7d-cube takes more than 10000 min then it's about a week).

[mortberg]

I think the conclusion of this experiment is that we need extension types in Cubical Agda. These are not only great from the point of view of efficiency; they should also make the treatment of HITs a bit more canonical and elegant. Thanks for doing the benchmarks!

[3abc]

I think the conclusion of this experiment is that we need extension types in Cubical Agda. These are not only great from the point of view of efficiency; they should also make the treatment of HITs a bit more canonical and elegant. Thanks for doing the benchmarks!

Yeah. BTW Defined comp6Cube (7536.535629s).

[3abc]

And I can see how extension types are simpler both homotopically and combinatorially. After all assembling a 4d-cube from a 3d-base + 6 3d-sides is simpler than from 16 vertices, 32 edges, 24 faces, and 8 cells.

[molikto]

@mortberg it seems to me extension type requires subtyping.

def test (A : type ) (x y : A) (q : path A x y) : 𝕀 → A = q

I am under the impression Agda don't have any form of subtyping. Or this proposal is about adding extension type without removing path type and without subtyping?