ohadProve dozens of syntactic substitution lemmata in one fell swoop with an induction principle with only two cases? Check.
Compositionality needs three cases though. :(
There are grad students younger than this proof that are cursing and cussing because they need to deal with bazillion-many cases for every SIGPLAN submission.
Jacques Carette@ohad Now you need to teach this to proof assistants, i.e. they should internalize this.
@JacquesC2 I already taught the computational content of this proof to a dependently-typed compiler. This means I can already manipulate families of well-scoped, well-typed AST representations without metaprogramming the AST traversals for substitution and splicing.
Happy to help a proof assistant teacher of a proof assistant with a reasonable theory and meta-theory and a reasonable development team. I suspect I'm already doing it vacuously. I'd be even happier to discover I'm not doing it vacuously anymore.
@ohad Work on convincing @totbwf . That won't help with any current proof assistant, but... it'll likely help.
Then I'd say convince @AndrasKovacs .
Conor Titania Mc Bride@JacquesC2 @ohad @totbwf @AndrasKovacs I am, of course, already convinced, and have been for twenty years.
@pigworker @ohad @totbwf @AndrasKovacs The convinced people need to find the convinceable people who have the skils+desire+energy to change the current systems.
I'm convinced, but I don't have the cycles to get to the point where I could modify a current system adequately.
@JacquesC2 @pigworker @totbwf @AndrasKovacs if you're convinced, find the convinceable people. I'm happy to explain how this works to any language designer.
@ohad @JacquesC2 @totbwf @AndrasKovacs We have a bag of tricks, underexploited. Good tricks. At the very least we should make them free tricks. I'd love to figure out how to go about making new tricks. But the old tricks are transformative, so for God's sake let's have them!
@pigworker @ohad @totbwf @AndrasKovacs In my books, the first step is to have "theory" be a first-class object. Neither records nor nested Sigma types are adequate representations.
Then we'd have a hope of making the old free tricks work nicely. And then on to new tricks we could go!
@JacquesC2 @ohad @totbwf @AndrasKovacs I agree that theories have to be a thing, but I'm anxious about them being first class, exactly because I don't want them to be records. Once you see that quotability is the primary virtue, you're heavily kicked towards syntax.
@pigworker @ohad @totbwf @AndrasKovacs [Veering discussion again - now: status of "theory" representation in a language.]
I can easily agree with that, i.e. what's important is quotability. And to be disciplined, you need some way to know (1) what the meta-theory of the thing you're quoting, and (2) what the vocabulary you'll land on.
@JacquesC2 @ohad @totbwf @AndrasKovacs This is right. And this is where we need to create. Two monoids make a rig. How do we tell them apart? How do we know they're both monoids? Some new modes of construction will matter. Some new forms of locality also. I don't have all the answers, but I am actively pursuing the questions.
@pigworker @ohad @totbwf @AndrasKovacs You already know my answer: you look at the (theory) morphisms that you used to create these things, not at the things themselves.
A 'flat' rig has forgotten whence it came. But if you've created your rig in a sensible way, the knowledge of those two monoids is in your hands, as is the way to tell them apart.
Typical category-theory answer: the answer lies in the morphisms, not the objects.
@JacquesC2 @ohad @totbwf @AndrasKovacs And this is how we frame the question of how to write it down. Algebras by name.