Post #2044537
2026-05-05 13:40 UTC
Replies (7)
-
@amy@types.pl 2026-05-05 13:41
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.
-
@5ht@mathstodon.xyz 2026-05-05 16:56
@amy@types.pl You guys know a very little about scaling software. Half of Agda committers lack simple education, you should start not from rewriting, but from requirements.
-
@foxy@blahaj.zone 2026-05-05 17:19
@amy@types.pl Best of luck! Will you be needing/accepting donations, e.g. LiberaPay? I haven't found this documented in the Codeberg repo. Should one use the individual maintainers' ko-fis?
-
@jeanas@mathstodon.xyz 2026-05-05 17:48
@amy @ncf @totbwf This is great news. If I have wishes for changes that the backwards compatibility break would make possible, where should I send them?
-
@jesper@agda.club 2026-05-05 19:37
@amy @ncf @totbwf I wish you all the best of luck with Mikan. Some of these changes are genuinely exciting, and I can't say I've never dreamed of getting rid of lots of the old cruft in the codebase (although I would have personally have removed a different set of features).
-
@mortberg@mathstodon.xyz 2026-05-05 20:02
@amy @ncf @totbwf Any thoughts about taking this opportunity to change the cubical type theory a bit? I think my dream system in terms of ergonomics would be cartesian Kan ops together with connections and reversals. I don't know how hard it would be to implement, but adapting the existing cubical libraries should be feasible. The main gain that I see is that we get rid of transp and replace it with coe r->s which is much easier to understand
-
@stschaef@mathstodon.xyz 2026-05-05 20:06
@amy @ncf @totbwf After looking at the gist I have a couple questions: 1. You write "types living in `Typeω` do not yet support the Kan operations `transp` and `hcomp`", and the last time I checked there was a similar message in the Agda documentation. I'm very curious what "yet" means in this context. The gist makes it sound infeasible at the moment, but the following paragraphs suggest there is reason to believe that these operations will eventually be worked out. Do you have thoughts in the direction of an implementation, or perhaps good pointers if one wished to take a stab at it? I've long wished to have a large path type, as it would allow for a nice implementation of large category theory. However, I don't have much experience with the Agda internals, so I do not know where to begin 2. Re "Rewrite rules are actually pretty useful!": The title of this section led me to believe that Mikan would encourage usage of rewrite rules, but the content of the section seems to suggest that rewrite rules must be dropped to preserve safety. Is this correct? Meaning that the correct interpretation of the second paragraph in this section is that in the absence of `--rewriting`, one can safely emulate their interface by using `J` on path constructors of a HIT? I have been working almost exclusively in the `--cubical` fragment of Agda, so I'm excited to see where this project goes! Best of luck!