This seems 'too easy' but to certify things I don't think it needs to be more complex? #6513
Conversation
… be more complex?
ramsay-t
added
No Changelog Required
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
| data UCSE : Relation where | ||
| cse : {X : Set} {x : Maybe X ⊢} {x' e : X ⊢} | ||
| → Translation UCSE (x [ e ]) x' | ||
| → UCSE ((ƛ x) · e) x' |
There was a problem hiding this comment.
Well just like with float-delay, you gotta make sure that e is pure. If the implementation pulls out an effectful e, then this may be a bug in the implementation.
... but unfortunately, it may not be a bug, sometimes it is fine to move impure things around for as long as that doesn't change the semantics of the program (and then there's an entirely separate discussion on whether effect ordering is important or not). For example if you have a bunch of applied lambda and all but one are pure, then it doesn't really matter in which order to execute them, since you're still going to get the single effect that you're ought to get.
So I suggest to reflect what I just said. Require e to be pure and say that this isn't the most general correct CSE, but is sufficient for now. Perhaps also add a link to this discussion.
| isUCSE? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (UCSE {X}) | ||
| isUCSE? ast ast' with (isApp? (isLambda? isTerm?) isTerm?) ast | ||
| ... | no ¬match = no λ { (cse x) → ¬match (isapp (islambda (isterm _)) (isterm _)) } | ||
| ... | yes (isapp (islambda (isterm x)) (isterm e)) with isUntypedCSE? (x [ e ]) ast' |
There was a problem hiding this comment.
I think the whole approach to certification is very suboptimal. I.e. this pass and the others (not sure if all of them). So what you do here is you check that the LHS has the right shape and then you proceed with substitution and recurse. Potentially just to figure out that you didn't need to do all this work, because the terms match exactly and there was no point in all these substitutions and non-deterministic digressing into CSE, float-delay and everything else at every lambda application node.
I guess this is a fine start, but I wouldn't be surprised if it eventually turns out that all the passes need to be rewritten, because they can't handle real-world terms fast enough.
| ``` | ||
| data UCSE : Relation where | ||
| cse : {X : Set} {x : Maybe X ⊢} {x' e : X ⊢} | ||
| → Translation UCSE (x [ e ]) x' |
There was a problem hiding this comment.
I'm perhaps nitpicking, but this isn't sufficient in the general case. CSE promises to pull some common subexpressions out, but it doesn't promise to pull all of them out. I.e. x' may still start with the same lambda and e may be substituted partially in x.
A straightforward Translation Relation for CSE certification. Perhaps there are some more subtle things we want to check?