Normalizing proof of commutativity +-comm about cubical

[Saizan]

I will close this as my testing indicates it's much better now.

[mortberg]

That is very strange! There seems to be an exponential blow-up. This does not happen for +-suc, so I think the problem must come from the use of compPath which builds a bunch of hcomp's. The number of them should be linear though, so I would expect this to be linear as well.

@Saizan Thoughts?

[Saizan]

I think you are right that the culprit is compPath, it seems more expensive to increase the second argument, which is the one creating more compositions.

Also, using _□_ seems to make things faster regardless.

[Saizan]

Ok, it's a problem of sharing for partial elements, basically hcomp has to look at the partial elements to decide if they are a constructor and then recurse. However, because of how partial elements are manipulated, the recusive call has to reduce the original partial element from scratch.

The reason for this inefficiency is that there isn't a good way to generate partial elements during reduction at the moment. Currently the only way to produce non-trivial partial elements on the fly is primPOr which is a single disjunction, so things might get a little ugly if reducing an hcomp on an inductive type leads to a term with a bunch of nested primPOr, though it would be more efficient.
Maybe the solution is an n-ary version of primPOr.

For naturals and other builtin types with literals we should also have custom implementations that take advantage of the compact representation available for closed terms. E.g., for Nat, hcomp [phi -> 100] 100 should compute to 100 directly rather than going through 1 + hcomp [phi -> 99] 99.
This is actually orthogonal and would be sufficient for +-comm 4 6.

[mortberg]

I noticed a massive speed-up in cubicaltt when computing hcomp as you suggest for closed terms of datatypes. It's not clear to me how we can utilize this in the presence of open terms though... But if we write an efficient closed term evaluator we should definitely use this optimization.

[Saizan]

In agda's internals, 100 is represented as LitNat _ 100 where LitNat :: Range -> Integer -> Literal, so even in the evaluator for open terms we could have a special case for when all the sides are of the form Literal l.

[mortberg]

Won't this force the sides to always be evaluated? I tried this in cubicaltt and it made things extremely slow because we couldn't rely on laziness to avoid unfolding things

[Saizan]

For open computation we have to reduce the sides to WHNF anyway.

For compositions that are known to be closed we can just use the base, that would be a different optimization.

[mortberg]

I see. Please try to optimization then! A good benchmark is: https://github.com/agda/cubical/blob/master/Cubical/Experiments/Problem.agda#L69

It should evaluate to refl at pos 0. I cubicaltt it is instant (with the optimization for hcomp in nat) but in Cubical Agda it never terminated for me.

[Saizan]

A good benchmark is: https://github.com/agda/cubical/blob/master/Cubical/Experiments/Problem.agda#L69

Might be good, but unless I'm missing something it's not a benchmark involving hcomp on inductive types much. Seems like it's all about HITs and the universe.

[Saizan]

Optimized hcomp for data types and especially literals in Agda master, agda/agda@fdbe073

Normalizing +-comm 4 6 is much faster, and things scale reasonably to larger numbers (+-comm can't get better than linear in the second argument).

@wvhulle would you like to test it out?