walker (Jan 30 2023 at 16:16): walker (Jan 30 2023 at 16:16):Question says it it all, all the time if you add a new variant to an inductive type, or make any minor modification, everything breaks until that modification is reflected else where, is there a way to minimize the effort needed for this kind of modify/experiment style of development ?
Meven Lennon-Bertrand (Jan 30 2023 at 16:29):Sadly, modularity with respect to changes of inductive types is hard… At least, proof assistants are nice, as they let you know exactly what breaks and where, while with pen and paper you can just throw away your proof and start a new one.
Meven Lennon-Bertrand (Jan 30 2023 at 16:29):Afaict, the state of the art with respect to modular inductive types is https://dl.acm.org/doi/abs/10.1145/3372885.3373817
Meven Lennon-Bertrand (Jan 30 2023 at 16:30):Regarding reparation of code, you can look up @Talia Ringer's work, I think she is the expert on the question :)
Pierre-Marie Pédrot (Jan 30 2023 at 19:21):In the PL world this phenomenon even has a designated nickname, the famous expression problem. AFAIK it's still an open problem although many people came up with very different solutions to the problem. Proof assistants just make the problem harder as they rule out some approaches like e.g. those relying on impredicative encodings.
Alexander Gryzlov (Jan 30 2023 at 19:36):In the context of dependent types solutions to the expression problem typically end up being some form of datatype-generic programming, e.g. stuff like containers, ornaments and levitation
Paolo Giarrusso (Jan 30 2023 at 19:44):Having seen some of the solutions outside proof assistants, I must ask: have you seen solutions that you'd actually want to use and are worth the trouble, compared to "just patch the code when needed"? That's not an option if somebody else must be able to write extensions, but that's not part of @walker's stated requirements...
Paolo Giarrusso (Jan 30 2023 at 19:47):I should say: I considered Scala case classes to be reasonable, but they interfered with exhaustivity checking
Meven Lennon-Bertrand (Jan 31 2023 at 09:55):In the current state of things it is still somewhat science fiction, but in the context of MetaCoq I think quite a few of us wish we could have something like Coq à la Carte, so that we can play around with a toy subsystem when wanting to test things and not bother about the full-blown system
Meven Lennon-Bertrand (Jan 31 2023 at 09:56):But yeah, right now the existing solutions are still not quite mature enough… Although I guess the only way to help them become more mature is to get experience with them by trying to use them?
walker (Feb 02 2023 at 14:32):coq ala carte looks really really promising, I watched the presentation couple times and I think I am close to the edge of my personal capability of having to go many times through the proofs of toy subsystems.
Last updated: Apr 19 2024 at 21:01 UTC