Combinatorial explosion

[guillaumebrunerie]

This is today’s example of combinatorial explosion (the same issue is present in cubicaltt), which might be why we didn’t manage to compute pi_4(S^3) yet.

Each test has twice as many comp’s as the previous one, but takes about 10 times longer to type check.

For instance test7 is basically the composition of 127 copies of the identity function, so it shouldn’t take as long as 102 second to apply it.

Defined test3 (0.025483s).
Defined test4 (0.156837s).
Defined test5 (1.337610s).
Defined test6 (12.062524s).
Defined test7 (102.599208s).

import path
import unit

let A : type
 = unit

let a : A
 = triv

let testpath : Path^1 type A A
 = λ i → comp 0 1 A [ i=0 ⇒ λ _ → A | i=1 ⇒ λ _ → A ]

let testpath2 : Path^1 type A A
 = λ i → comp 0 1 A [ i=0 ⇒ testpath | i=1 ⇒ testpath ]

let testpath3 : Path^1 type A A
 = λ i → comp 0 1 A [ i=0 ⇒ testpath2 | i=1 ⇒ testpath2 ]

let testpath4 : Path^1 type A A
 = λ i → comp 0 1 A [ i=0 ⇒ testpath3 | i=1 ⇒ testpath3 ]

let testpath5 : Path^1 type A A
 = λ i → comp 0 1 A [ i=0 ⇒ testpath4 | i=1 ⇒ testpath4 ]

let testpath6 : Path^1 type A A
 = λ i → comp 0 1 A [ i=0 ⇒ testpath5 | i=1 ⇒ testpath5 ]

let testpath7 : Path^1 type A A
 = λ i → comp 0 1 A [ i=0 ⇒ testpath6 | i=1 ⇒ testpath6 ]

let test3 : A
 = coe 0 1 a in λ i → testpath3 i

let test4 : A
 = coe 0 1 a in λ i → testpath4 i

let test5 : A
 = coe 0 1 a in λ i → testpath5 i

let test6 : A
 = coe 0 1 a in λ i → testpath6 i

let test7 : A
 = coe 0 1 a in λ i → testpath7 i

[guillaumebrunerie]

I just tried test8 and it took 814 seconds while also using quite a lot of memory (maybe 6GB).

[jonsterling]

Thank you! I'm curious to see if we can improve it :smile:

[ecavallo]

In case it's useful for diagnosis, I'll repeat the observation from #250 that times can vary drastically depending on how one composes.

[jonsterling]

Hi @guillaumebrunerie, I've re-tested this example now and there is still an explosion, but it is generally much faster now. Here's the results on my laptop:

Defined test3 (0.021283s).
Defined test4 (0.027573s).
Defined test5 (0.193763s).
Defined test6 (1.072293s).
Defined test7 (7.735767s).
Defined test8 (46.797967s).

Here is your code updated to work on the latest version of redtt:

import path
import unit

let A : type
 = unit

let a : A
 = triv

let testpath : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → refl ]

let testpath2 : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → testpath ]

let testpath3 : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → testpath2 ]

let testpath4 : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → testpath3 ]

let testpath5 : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → testpath4 ]

let testpath6 : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → testpath5 ]

let testpath7 : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → testpath6 ]

let testpath8 : path^1 type A A
 = λ i → comp 0 1 A [ ∂[i] → testpath7 ]

let test3 : A
 = coe 0 1 a in testpath3

let test4 : A
 = coe 0 1 a in testpath4

let test5 : A
 = coe 0 1 a in testpath5

let test6 : A
 =
 coe 0 1 a in testpath6

let test7 : A
 = coe 0 1 a in testpath7

 let test8 : A
  = coe 0 1 a in testpath8