Reasoning about transport is very slow #296
Labels
Comments
|
I would suppose that using transports on sigma types instead of heterogeneous equality falls into the projection blowup case. I'm still in the process of adapting categories/ to my latest implementation which has native projections, hopefully we can play with it soon! |
|
If this can be fixed by native projections, I'd be very delighted. I look forward to playing with it! (If I can do anything to help adapt categories/, let me know.) |
|
Does this use fast projections? On Sun, Apr 27, 2014 at 8:22 AM, Jason Gross [email protected]:
|
|
@spitters, I am not using fast projections, as the latest version does not compile enough of categories to get to this point (lax comma categories) (see, for example, HoTT/coq#108). There are also a number of issues with Set/Prop (see, e.g., HoTT/coq#119), but these can be worked around by not letting anything go into Set or Prop. It's hard to compare timings when so many files don't compile, but initial results don't look super-promising: The N/A files are ones where the dependencies can't be compiled. Here are the files that trunk-polyproj is currently erroring on: It's also getting a stack overflow in |
|
Note that I haven't turned on primitive projections with any special command, so I might be missing out on speedups due to that. |
|
If you didn’t turn it on then there’s no way it’s gonna use them :) On 28 avr. 2014, at 00:50, Jason Gross [email protected] wrote:
|
|
Excellent! I'll rerun the timing data. Does this fix the slow-down of f_equal applied Will the version merged into trunk have eta for records? Last I checked, -Jason
|
|
On checking again, the issue (HoTT/coq#124) is that setting universe polymorphism seems to break eta for records. |
Indeed. Unfortunately, trunk-polyproj seems to have enough trouble that I can't test them out for categories. For example, (But, please, don't let my open bugs delay merging into trunk. :-) ) |
|
The newest version does not seem to have improved performance over the older trunk-polyproj on the |
|
Here are the files that still don't compile: Updated timing data: |
|
@JasonGross What is left in this issue? |
|
It should be noted that we do in fact have heterogeneous equality in the library now. It is under the name DPath in the Cubical library. |
|
Sometimes "heterogeneous equality" refers to the univalence-incompatible version; I'm not sure what @JasonGross meant here 6 years ago. |
|
I was in fact referring to |
|
What can JMeq do that DPath's can't? Or is it something to do with axiom K? |
|
The axiom |
|
I suspect that this issue is stale and should be closed, but I'll let @JasonGross opine. |
|
Oh ok that explains it. Regarding this issue however, if transports are slow I am curious to see if DPaths do any better, since I would expect there to be less unfolding. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I have some proofs that I ported from catdb which slowed down immensely when moving from using heterogeneous equality to using transport and PathGroupoids, namely JasonGross/HoTT@master...finished-but-slow-exponential-laws and JasonGross/HoTT@master...finished-but-slow-adjoint-pointwise. The proofs aren't doing much interesting, but are about an order of magnitude slower than most of the other files in HoTT (the exception being categories/Comma/ProjectionFunctors.v). It would be nice to have a better way of reasoning about paths quickly (perhaps by reflective automation, or an extension, or a well-tuned tactic).
The text was updated successfully, but these errors were encountered: