search

mortberg / cubicaltt

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

Type-checking performance issues #38

Closed gullcomb closed 8 years ago

gullcomb commented 8 years ago

I am a newcomer to cubicaltt. As part of my experiments, I wrote the following function mapping equivalences to their inverse

import equiv
invEquiv (A B : U) (f : equiv A B) : equiv B A
    = (invEq A B f, gradLemma B A (invEq A B f) f.1 (secEq A B f) (retEq A B f))

together with a proof that this operation is an involution.

invEquiv_invol (A B : U) (f : equiv A B)
    : Id (equiv A B) (invEquiv B A (invEquiv A B f)) f
    = <i> (f.1, propIsEquiv A B f.1 (invEquiv B A (invEquiv A B f)).2 f.2 @ i)

The latter takes a long time (25s on my laptop) to type-check. This is very surprising because type-checking this

invEquiv_invol2 (A B : U) (f : equiv A B)
    : Id (isEquiv A B f.1) (invEquiv B A (invEquiv A B f)).2 f.2
    = propIsEquiv A B f.1  (invEquiv B A (invEquiv A B f)).2 f.2

is very fast, so I would expect the type-checker to be able to extract the endpoints when i = 0 or i = 1.

However (from what I understand of the code), since propIsEquiv is a defined identifier, it expands the invEquiv_invol2 subterm of invEquiv_invol into a path abstraction. Then, it uses substitution of path variables (act) to propagate the value of i, which involves a lot of redundant calls to support (if i is in the support of a value, then act recurses into its subterms and calls support again).

I have a patch that makes path abstraction evaluate to closures (as lambda-abstractions currently do), which fixes this issue. However, it slows down most of the examples (multS1.ctt is the noticeable exception). This is probably because the equality on closure values also compares the environments, including all the previous definitions (which themselves have an environment; although most of it is shared, the derived Eq instances don't know and compare everything).

I have not tried to modify the evaluation strategy so that head variables are not unfolded when applying a path to 0 or 1 (so that Eval.inferType can be used to extract the endpoints) but this seems also doable. Fixing correctly the issues about pointless comparison of environments seems much more involved, though.

gullcomb commented 8 years ago

Because of the recent work, in particular the 'explicitnames' branch, I looked again at this issue and I have new remarks. It is now possible to solve this particular case by using opaque propIsEquiv, but other improvements are still possible.

 

First, I noticed that the implementation of compLine is naive. It applies a fresh variable to values that are likely to be path abstractions, so this will call act and possibly compLine recursively. Then compLine calls comp, which will wrap these values again in a path abstraction if it can't simplify. Moreover, if comp simplifies because the system has become trivial, then using fresh variables was unnecessary and 1 can be directly used instead.

Moreover, profiling shows that it is unlikely for comp to simplify: usually less than 20% for the example files, 0.6% in my example. And when it does, it's often because the system is trivial: usually between 60% and 80%.

I think this comes from the mismatch between the VComp constructor and the comp* functions. The former is not a binder while the latter are implemented in terms of comp, which behaves like a binder. I'm not sure whether it's better to make VComp a binder or to reimplement the comp-like functions in terms of compLine rather than comp.

 

The profiling also shows that for certain files cubical spends more than 50% of the time comparing environments' declarations (Def constructor for Ctxt). And very few of such comparisons return false: 6 out of 1.2 million for category.ctt and csystem.ctt, 12 out of 850 millions for torsor.ctt and none for the others.

The easiest way to solve this would be to tag declarations with their origin (i.e. file and line number) so that if the origin is the same there is no need to compare the contents. Unfortunately, there is no way to get this information from the parser. Instead StateT or IO can be added to the Resolver monad to generate unique identifiers.

mortberg commented 8 years ago

Interesting! Maybe we should rethink how we implement comp (I think we had a version before which contained the name?).

I also noticed that comparison of environments takes a lot of time. Try to comment out the test whether u == v in conv and then recheck csystem. Implementing something more clever like what you suggest sounds like a good idea. I can try to do it next week, or if you want you can do it and file a PR if it makes things faster (if you do please check so that complicated files like hz, csystems and torsor all get faster).

mortberg commented 8 years ago

I'm going to close this now that https://github.com/mortberg/cubicaltt/pull/44 has been merged. The PR improves typechecking performance a lot. Here are some benchmarks:

Without the PR: hz: 0m11s torsor: 4m18s csystem: 8m49s

With the PR: hz: 0m3s torsor: 0m45s csystem: 0m16s

So all of the large files takes under a minute now which I think is reasonable. Thanks a lot for investigating and implementing this!

I should also add that I experimented with adding explicit support (i.e. pass the support around as an extra argument everywhere instead of recomputing it). Strangely this didn't speed things up everywhere (some files took longer to typecheck), so that change is not as good as I thought. Note that the computation of large normal forms (i.e. of univalence) is much faster with explicit support though, so it could be worth having a flag to enable it (implemented using the unsafePerformIO hack).