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.
@JacquesC2 @ohad @totbwf @AndrasKovacs OK, maybe 15. We cooked substitution laws for free in PigWeek 2010.
@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 The principal virtue of a theory is quotability. That is, recognizing that the problem at hand is amenable to the theory. Records and God knows what do not recognize that reality.
@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.
@JacquesC2 @pigworker @totbwf @AndrasKovacs know where you are, whence you came from, and where you're heading to. Omit any one, and you'll invent doomed-to-fail tricks that try to reconstruct heuristically something you foolishly threw away or haven't explicated.
@JacquesC2 @pigworker @totbwf @AndrasKovacs just because I arrived here via two commuting monoids, doesn't mean I don't deserve to become a commutative monoid.
@JacquesC2 @pigworker @totbwf @AndrasKovacs I learned this lesson, in this context, from @pigworker , with @gallais hammering the lesson often.
@ohad @pigworker @totbwf @AndrasKovacs @gallais The higher lesson is that if you remember the reason for the travel, you know most of the rest already. Amusingly, this lesson is most clearly seen when trying to implement undo/redo.
In other words: transformers are strictly more informative than the sequence of states traveled through.
[Of course I meant intensional representations of transformers, opaque transformers are less useful than knowing all the states.]
@JacquesC2 @totbwf @AndrasKovacs The starting point must be different than 'why can't you do it with the existing ones?'. After twenty years the question is: why didn't **you** do it with the existing ones, or built ones that could do it?
@ohad @totbwf @AndrasKovacs Because I don't know how to build a proof assistant (beyond a toy one). Formalizing this in one is pointless. It's integrating it into its very functioning that is the only remaining, interesting part.
I build stuff akin to this. They worked. But I used the wrong method (meta-programming). Others are still using the wrong method.
This needs programming, not meta-programming.
@JacquesC2 @totbwf @AndrasKovacs sorry, but why do you *need* the proofs to integrate this into the implementation of a proof assistant? With very few exceptions, we don't prove these correct, and even if we do, it's not the canon implementation.
Martin Escardo@ohad @JacquesC2 @totbwf @AndrasKovacs
This discussion is going on several tangents, but if you read any serious mathematical paper, you will see that there is both object-level and meta-level discussion.
At the moment proof assistants are good at object-level discussions, and, although they do support meta-level programming (in a crappy way in my view), they don't support meta-level reasoning (at all).
@MartinEscardo @ohad @totbwf @AndrasKovacs Right!
(You can do it via layers of encoding, but it gets awful really, really quickly.)
@JacquesC2 writes "You can do it via layers of encoding, but it gets awful really, really quickly."
I agree with the "but".
But I disagree with the "You can do it via layers".
Yes, you can in principle, if you take the object-language of your proof assistant as the meta-language, and then encode the object-language within it.
But what if I have already proved something, using the object-language of the proof assistant, and I want to draw a meta-theoretical conclusion?
This happens all the time. In e.g. TypeTopology we have about 260k lines of code (including comments and blank lines).
Do I need to translate this to the encoded language if I want to meta-reason about it? Of course this is a ludicrous requirement.
(Which we often do in papers. I can give explicit examples on demand.)
@MartinEscardo @ohad @totbwf @AndrasKovacs I agree, having both reflection and reification would be extremely useful. Not a la Lisp (or worse) but in a more principled way.
@JacquesC2 @MartinEscardo @ohad @totbwf @AndrasKovacs We are clearly banging our heads off an abstraction ceiling in a dimension wherein we are currently stuck. That provokes.
@MartinEscardo @JacquesC2 @totbwf @AndrasKovacs another tangent: I'm finding 'meta' confusing in these settings, so decided to adopt the antonym 'mesa'. You fix the language, and then it's 'mesa^n-languages' all the way down.
@ohad @totbwf @AndrasKovacs Discussion evolved and veered.
Proofs are only needed to convince oneself that implementing "free substitution machinery" isn't a pile of hacks. Piles of hacks have been done - we know this can work. You've shown there's a strong reason for that. Great.
Now there's no reason not to implement this as a feature.
Zanzi @ Monoidal Cafe@ohad @JacquesC2 @totbwf @AndrasKovacs Implementing a well-typed by construction type theory with type variables inevitably involves a lot of green slime due to needing to do type-substitution in terms. This makes it impractical to build any serious compiler machinery on top of this.
So, personally, I'd like to work in a dependent type theory which has built-in support for equational solving of substitution theories to avoid dealing with this kind of green slime.
Reed Mullanix@ohad @JacquesC2 @AndrasKovacs Because those same grad students who are tired of doing the same bazillion-many cases are *even more* tired of doing those bazillion cases with the mechanical pedant watching
Constantine Theocharis@ohad therapist: strength pentagon isn’t real, it can’t hurt you
strength pentagon:
@constantine The strength pentagon is your friend. Today's 'best practice' is to metaprogram these proofs and then check them.
@ohad That does sound much worse
@ohad gave a very nice talk about this in our Theory Seminar.
@ohad I have pet peeves about commutative diagrams and which of them deserve the name proof.
You have managed to not trigger them. Bravo.
@JacquesC2 details please?
@ohad private message incoming. I don't want to start a flame war.
@MartinEscardo @ohad It'll be fun to watch, given how very little information there is to use to 'flame' on.
@ohad where can I read more about this?