search

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

No support for recursive HITs, but forward instead of squeeze and transp #62

Closed mortberg closed 7 years ago

mortberg commented 7 years ago

This PR attempts to fix the composition for directly recursive HITs like propositional truncation. It also implements the forward function instead of transp and squeeze that Simon and I came up with last week. Most things seem to work, in particular the first example provided in https://github.com/mortberg/cubicaltt/issues/35 now typechecks.

However there is something very strange going on, we ported the setquot code to use the HIT version of propositional truncation instead of the impredicative encoding. The whole file typechecks, but when we try to compute some simple examples it never terminates (I killed the process after ~24h, with the impredicative encoding it terminates in 0.5s...). So there is either a bug in the implementation or the HITs are just very inefficient. I still vote for merging this code in order to make it easier to debug and try simpler examples.

Note that the bug in https://github.com/mortberg/cubicaltt/issues/47 is not fixed yet. That issue has to do with HITs where the path constructor involves a function (like in pushouts and coequalizers). If one runs the example in that file one sees that the f is not on the right side of the comp, so we have to use pres (from the paper) to correct it. Doing this in general for functions with more than 1 argument (where the arguments form a telescope) has to be worked out, but hopefully one can just directly generalize the pres operation from the paper.

spitters commented 7 years ago

Nice! Did you try profiling? We discussion about performance of setquot last year and at that them computing the support was very expensive.

mortberg commented 7 years ago

No, we didn't investigate this carefully yet.

I implemented a very simple test: I proved that Unit is equal to its propositional truncation (using univalence) and transported inc tt and tt along this equality:

foo : Path U tU Unit =
  <i> (uahp (tU,pTruncIsProp Unit) (Unit,propUnit) f1 f2 @ i).1

test1 : Unit = transport foo (inc tt)
test2 : tU = transport (<i> foo @ -i) tt

the result when computing these are:

> test1
EVAL: tt
> test2
EVAL: hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (hComp (pTrunc Unit) (inc tt) []) []) []) []) []) []) []) []) []) []) []) []) []

So when we transport tt into the propositional truncation we get 13 hComp's with the empty system... This might be what makes the much more complicated examples in setquot so slow, but the strange thing is that the memory consumption doesn't seem to be going up.

CohenCyril commented 7 years ago

This pull request does not match the initial goal anymore.