FAQ
We've been working on Mikan for about two weeks. Over this time, private discussions about the project have surfaced some questions that I feel are worth addressing with the announcement. They're frequently asked but with very low frequency.
Have there actually been concrete improvements?
I think the first question to address is whether we're actually doing positive work, or just cutting a bunch of features because we're Mad On The Internet while talking big possible improvements that will fizzle out because they only exist as vague plans. This is a legitimate question: the majority of work in the fork has been deleting upstream code. However, I would like to call attention to the following work that has been happening concurrently with the axing.
mikan#21 fixes a difference in behaviour betwen --without-K (code accepted) and --cubical-compatible (elaborator explodes). This is, in all, a minor bug, but I'm including it as demonstration of how difficult it is to keep these in sync. Similarly, mikan#67 and mikan#73 fix another four internal errors between them.
mikan#26 allows combining structural recursion and copattern matching --without-K. The code in the example is rejected upstream because of a naïve attempt at fixing agda#1023, a proof of false. Upstream issue agda#5910 demonstrates how this naïve fix is easily fooled; our refined implementation also pushes back on this.
mikan#41 fixes "the primary motivation for Propω", namely families of propositions indexed by a value in Typeω. The upstream test case for this feature has never actually tested its functioning, instead relying on the coincidence that, when the test was written and --with-K, the default behaviour (--large-indices) is to not sort-check datatype indices at all. When --large-indices was spun off into a flag, it was added to the test case for Propω, thus ensuring that the test case would still not test what it was meant to.
If you allow me to be annoying, removing sized types (done) and irrelevance (coming up) fixes both known proofs of false and the new one that we stumbled into. Removing irrelevance also by fiat removes all the broken scheduling interactions between Prop and irrelevance.
@totbwf has been hard at work simplifying our build system. The entire test suite has been ported to tasty tests, so we can now build and test with cabal. Our plan is to eventually cut the Makefile-based build system entirely, retaining only a minimal, dependency-free Makefile as a friendly entry point for the cabal commands.
Will Mikan keep support for book HoTT?
In a sense, yes and no: Mikan supports the indexed inductive identity type with the same caveats as Cubical Agda (depending on the specifics of the index at which you're matching, the functions may not compute when applied to cubical primitives).
All accepted functions will compute as-is when applied to the refl constructor, and many functions (roughly, those which only match on elements of Id with fully general parameters, like J but also sym and trans and such) will compute even when applied to "cubical" elements of the identity type.
However, we have no plans to support a flag like --without-K. Synchronising its behaviour with the actual main mode of use we plan to support is a pretty significant challenge. You can, of course, continue to postulate or locally assume funext/univalence/HITs/etc instead of deriving them from cubical features.
There are two specific breaking changes of note:
Mikan does not currently support inferring types for lambda abstractions. This is because we do not currently have a strategy for postponing the decision of whether an abstraction λ x → ... introduces a function or path type, which also means that we can not easily infer this from how the bound variable is used in the body. You can recover the old behaviour by annnotating the expression with a type like ∀ x → _, or, if possible, by annotating the domain with a non-underscore type, like λ (x : Nat) → _.
Pattern matching on an indexed Type that involves transporting a value whose type lives in Typeω (e.g. the function's result, or an argument depending on one of the indices) is currently rejected with an error message about generating f (transpX (transpX …)) clauses.
The concrete reason for this is that types living in Typeω do not yet support the Kan operations transp and hcomp, so we literally can not implement the behaviour of pattern matching on (e.g.) the identity type for these. The difficulty here is that internal quantification over the i in Typeωᵢ is impossible, and the current representation of primitive functions in internal syntax makes it tricky to support something like hcompωᵢ without losing the ᵢ.
I plan to fold this failure into the dreaded UnsupportedIndexedMatch warning in the near future, so that these pattern matching functions will go from the very annoying "rejected" to the mildly disappointing but status-quo "doesn't compute on transp". This will be a stop-gap solution until we work out a satisfactory design for Kan operations in Typeω (this also applies to type families in Prop and Propω).
Will Mikan be faster than Agda?
For non-cubical code, the immediate answer is "no", since pattern-matching on indexed types now always incurs the cost of supporting matching on transported elements. We would of course like to make this code faster in the future but it is unlikely that we can make it as cheap as not reifying the equivalence generated by LHS unification.
For cubical code, the answer, immediately, is "perhaps slightly". A lot of the features we're removing, like the modal systems and local rewrite rules, incur bookkeeping costs in many parts of the elaborator, even if they are not actively being used. These costs are nontrivial but marginal.
In the longer term, we would like to make use of the simpler language and backwards compatibility break provided by the fork as a jumping-off point for further optimisations. We do have concrete examples of these:
At present time, parallel type-checking has considerable overhead when importing modules due to being unable to avoid the repeated work shared with the logic for importing modules in sequential checking.
The technical details are somewhat beside the point, but the gist is that, when a new type-checking worker is ready to do its job, it has to "replay" the import of all its transitive dependencies. This is because importing a module does nontrivial work in the TC state: first, there is the compatibility check for infective/coinfective options; second, importing a module with rewrite rules has to update some bookkeeping information for every definition that appears as the head of a rewrite rule, and the confluence check must be re-run for every new import.
Simplifying the options compatibility check to a single bit (--safe vs. not) and removing rewrite rules will pave the way to eliminate this overhead, by changing the logic for imported things from having imports affect the local TC state to looking up remote things in self-contained data structures associated to each module.
Last year, I merged a significant performance improvement to the implementation of parametrised modules. This was reverted, in part, because it changed the behaviour of caching (skipping the type-checking of a prefix of the module), but only in modules that have no interaction points.
I disagreed at the time, and still disagree, that "appending new code with no interaction points and reloading" is a mode of use to which we should be beholden. A fork is a perfect time to bring this optimisation back, make sure the implementation is up to par, and crown the new caching behaviour.
Rewrite rules are actually pretty useful!
That's a statement, not a question, but I don't disagree. However, they are, fundamentally, a form of equality reflection, and, since we're removing support for --with-K, there would be no language variant left for them to be safely used with. Moreover, upstream already claims that confluence checking is not supported with --cubical, so even the check that the loaded rewrite rules aren't nonsense would not be usable.
If you were using rewrite rules to implement higher inductive types, consider replacing them with cubical higher inductive types: the generating paths do not need to be exported, and can be made into abstract generating identities if you don't want to see cubical stuff cropping up when you apply (e.g.) apply J to a path constructor. This will let you --safely have HITs with computation on the point constructors.
Do all the modalities have to go?
In general, please understand that all the modal systems upstream supports are ill-understood in combination with cubical type theory, and that none of us are experts in modal type theory. There are also the following specific points:
Erasure (
@0) is primarily useful in combination with compilation, which has never been supported for the cubical mode and so has been removed from Mikan. While "erased cubical" existed, it was impossible to adopt without complete buy-in from the library, since any definitions in a --cubical module would become erased when imported from an --erased-cubical module, including those that didn't use any erased-only primitives.
Irrelevance (
@irr/.A) is inconsistent, as mentioned above, and nobody knows what shape-irrelevance (
@shirr/..A) does. We could remove shape-irrelevance and keep playing whac-a-mole with irrelevance, as I'm sure upstream will when they learn of our new proof of false, but Prop is well-understood (so what remains to integrate it smoothly with Mikan is engineering work, not Ph.D. thesis work) and serves our need for definitional proof-irrelevance (only ¬¬-stable propositions) perfectly well.
Guarded (
@lock) integrates poorly with postponement, is somewhat inelegant in that locks must both live in a special universe and be marked with a modality, and only serves to permit safely postulating Löb induction.
