agda
Why we should revert stdlib to `--without-K` instead of using `--cubical-compatible`
Here is a minimal example of the ills that we get with --cubical-compatible that we don't with --without-K:
{-# OPTIONS --cubical-compatible --safe #-}
module MWE where
open import Data.Nat.Base using (ℕ; _≤_; z≤n; s≤s)
open import Data.Vec.Base using (Vec; _∷_; zipWith; truncate)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
private
variable
a b c : Level
A : Set a
B : Set b
C : Set c
m n : ℕ
truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
zipWith f (truncate m≤n xs) (truncate m≤n ys) ≡ truncate m≤n (zipWith f xs ys)
truncate-zipWith f z≤n xs ys = refl
truncate-zipWith f (s≤s m≤n) (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (truncate-zipWith f m≤n xs ys)
If you try to load that, you get the following warnings:
/Users/carette/Downloads/MWE.agda:20,1-22,49
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.
Reason: It relies on injectivity of the data constructor ℕ.suc,
which is not yet supported
when checking the definition of truncate-zipWith
/Users/carette/Downloads/MWE.agda:20,1-22,49
warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.
Reason: It relies on injectivity of the data constructor ℕ.suc,
which is not yet supported
when checking the definition of truncate-zipWith
Of course, I could shrink the example further to trigger the warning -- any pattern matching on _≤_ will do that. The above is a real example drawn from real code.
Basically the proof idiom above is a perfectly good one to use in stdlib and should give no warnings. Nothing in Cubical Agda should interfere with stdlib -- but it does.
I think that until agda itself is fixed, we should go back to --without-K.
Pinging @andreasabel who made the original change in the other direction.
Wow? #2767 works for padRight (by similar kinds of pattern match), but analogous proofs fail for truncate!? Oh dear...
... but what is surprising is that we do have existing code that does pattern matching on _≤_, including its inversion principles, so what's going on?
Pinging @plt-amy .
What's the strategy here?
(I would simply suppress this warning by putting flags: -WnoUnsupportedIndexMatch in the .agda-lib file.)
Hmmm... I just rechecked your MWE with agda-2.8.0 (and v2.6.3 and v2.7.0, just to be sure) and it seems to work just fine!?
(That doesn't invalidate my support for the proposal itself... I've grown tired of error messages and diagnostics during typechecking associated with transport which are out-of-scope for stdlib, but I had reluctantly made peace with cubical-compatible...)
What's the strategy here?
Suppressing the warning is what we all do, but, like... Does anyone use the standard library with cubical code? Despite being technically supported we all want to get away from setoid hell. Generating the support code is a significant time cost. I don't see a reason to stay --cubical-compatible. IMO switch back to without-K and gain a free speedup and in the extremely unlikely event someone yells, this comment will look very silly and you can add the flag to disable the warning.
@JacquesCarette wrote:
Pinging @andreasabel who made the original change in the other direction.
For the record, that was actually @nad .
- https://github.com/agda/agda-stdlib/pull/1854
This was previously discussed in https://github.com/agda/agda-stdlib/issues/1939, in which @nad said he was using stdlib with cubical code.
I wonder if there's space to split up the library into a --cubical-compatible core, with types where we are happy to use propositional equality (e.g. Bool, ℕ, possibly List), and then a library of setoid-y stuff on top of that that uses --without-K.
@JacquesCarette is this a reproducible v2.8.0 bug or not? And if it is, why can't I reproduce it!?
are you next to https://github.com/agda/agda-stdlib/blob/604b1f431a7409042b1e56c2a54c7a9e76ff681f/standard-library.agda-lib#L4 ?
@plt-amy Whoa! Did I do that!? No... that was you, back in 2022, and I blindly followed it in #2775 ... sigh.
Going back to the op on this issue:
Basically the proof idiom above is a perfectly good one to use in stdlib and should give no warnings
it is and it won't as long as you put it in the stdlib repo. if you put it outside the stdlib repo then it's on that project to decide whether or not it cares about proofs computing at transport along indexed inductives
This code development was indeed done "outside stdlib" while prototyping stuff to go into stdlib, and thus the warning had not been shut off.
While I disagree with @plt-amy about Setoid hell, I completely agree that it makes little sense to combine cubical with stdlib. stdlib is built for a different type theory. A lot of the design choices of stdlib make no sense if you've got cubical!! The Cubical library already "duplicates" a fair bit of stdlib as it is. A bit more is fine.
Yes, there is at least one user of that combination. But the efficiency loss is significant.
Suggest this as part of the wholesale breaking we are considering for v3.0, but not for v2.x?
Arguably, it was the original change that was breaking but only mildly (new warnings). So this could be seen as a bug fix.
Recent work on Agda performance provides quite a bit more ammunition for doing this. stdlib uses IndexedMatch a lot (3926 times apparently). It's a perfectly fine feature but incompatible with --cubical-compatible.
Ahead of v3.0, is it possible to document, on a per-module basis, which modules/definitions, trigger IndexedMatch?
As an old-school type theorist, I find it hard to imagine working in anger with inductive families without support for these kind of definitions.
That said, it's clear that in some places (eg truncate etc. #2770 / #2787 ) we have perhaps been over eager (literally and figuratively) to rely on matching on proofs, so it would be good to identify what might be modifiable to avoid this problem, and what are 'essential' uses.
But as @JacquesCarette says, and as an old-timer, I see few problems working in the non-cubical setting. I'm very happy committing to a fully constructive, setoid-based, library, just as I am with cubical users following their own path.
My concern, obviously, would be if we reached a point in Agda development where the two styles could not both be supported. I think that I had (mistakenly?) understood cubical-conpatible as the (necessary?) way to tie those things together.
So a cautious, qualified, 👍 to the proposal.
Is there space for a --cubical-compatible library or section for certain things for which propositional equality is what stdlib wants to use (e.g. Data.Nat), that --cubical dependents can use without worry, and then for things that want to be more setoid-y we use --without-K?
Good question @Taneb ... one reason I might prefer a revert to --without-K on a per-module basis (as above), if we are able to localise where we need IndexedMatch... but I think I've lost track of how the (co-)infectivity rules apply to mixing --without-K and cubical-compatible code. Does a global --cubical-compatible flag (supplied to agda) override a module-local --without-K (so that a single library could be checked under multiple 'modes'/flags, according to mode-of-use/deployment)?
It would be a middle-ground rather than @JacquesCarette 's root-and-branch solution, though, which has the merits both of simplicity, and (perhaps more notably) efficiency, wrt typechecking time (and space, I think).
I think with all these things, and past actions on our part, we've tried to avoid unnecessary forks in the stdlib codebase, for the sheer maintenance headache alone. But perhaps if GenerateEverything maintained an EverythingCubical list of modules... ugh I have a headache even trying to think about how to manage/organise such things... mutter mutter (Abstract)Factory mutter mutter...
Having a quick experiment... this would be an even more substantial change than I envisioned. Data.Nat.Base, what I picked out as the most obviously useful for --cubical downstream use, has several unsupported index matches that would need to be moved to a different module
Ah, yes... the various s≤s⁻¹ inversion principles... sigh.
Downstream, I could imagine (esp. eg @JacquesCarette himself ;-)) wanting to refactor even Data.Nat.Base to tease apart the ordering relations from that base... but not now, I think!
All of these things... like pulling on a loose thread, until the entire thing unravels in your hand. Sigh harder...
BTW, this is not really breaking. This is gaining back some efficiency that we lost without sufficient discussion. One could consider this a bug fix.