Translation relation and decision procedure for the Float-Delay

[ramsay-t]

Translation relation and decision procedure for the Float-Delay phase of the UPLC certifying compiler.

This typechecks and follows the description of the phase, but it hasn't been tested against many real examples.

Fixes #6371

[effectfully]

So I've only attempted to make this thing type check without trying to think about its semantics, but now that I review the PR, this isn't a semantics-preserving transformation, is it?

If I'm reading it correctly, it'll transform (\x z -> x) (delay y) into (\x z -> delay x) y, but these are very different terms: the former doesn't necessarily force y while the latter does always force it.

I don't know what the pass does in Haskell, but what's written here doesn't look correct to me. I may be missing something though.

[ramsay-t]

I - perhaps naively - assumed the value was the interactions with the Force-Delay rule? If we have force x we can now cancel that out. Of course, force x seems ... unlikely?

[effectfully]

Well, each pass needs to make sense on its own, so there should either be an explicit dependency of the force-delay one or something else that constraints this pass to only work over appropriate terms... except that wouldn't help either, because even if it was force x, you'd still evaluate y with the second term without necessarily evaluating it with the first one.

[ramsay-t]

I was also assuming that converting (\x -> blah x blah x blah) . (delay y) into (\x -> blah (delay x) blah (delay x) blah) . y provides more "opportunities for laziness", since the long term with lots of xs might realise that it doesn't need to evaluate all of them? That is more likely if they are at multiple places in a larger expression? Doing the y once, even if you always do it, then seems cheaper? Whether this is actually a correct impression of how the evaluation will proceed, though, I don't know?

[effectfully]

Doing the y once, even if you always do it, then seems cheaper?

That's just not how things work, at all. y can be a loop or an error crashing the program, you can't change the semantics of a completely arbitrary term.

(\x -> blah (delay x) blah (delay x) blah) . y provides more "opportunities for laziness", since the long term with lots of xs might realise that it doesn't need to evaluate all of them?

x is already evaluated within that term, since it's bound by a lambda. So evaluating force (delay x) amount to simply discharging the force-delay pair and looking x up in the current environment.

[ramsay-t]

I'm just playing "Devil's Advocate" :) This phase was created for some purpose, we ought to find out what and document it...

[ana-pantilie]

I think when we spoke about this transformation I glossed over some details, sorry. I've looked at the docs again, and it's necessary that every occurrence of the variable is immediately under a force, and that the argument is "work-free".

So, let's take a look at some examples. Let x, y, z ... be variables and arg be some term; we assume that there aren't any occurrences of x in the body other than the ones explicitly mentioned:

1. (\x -> ... force x ... force x ... x ... force x) (delay arg) here we cannot apply the transformation, because the third x in the body is not under a force.
2. (\x -> ... force x ... force x ... force x ... force x) (delay y), although all x's are under force, we still can't apply the transformation because y is not "work-free".
3. (\x -> ... force x ... force x ... force x ... force x ...) (delay (\y -> ...)) in this case we can apply the transformation and the term becomes (\x -> ... force (delay x) ... force (delay x) ... force (delay x) ... force (delay x) ...) (\y -> ...)

I think you asked me what happens in the following case: (\x -> (\y -> blah y blah) . x) . (delay z). Given the restrictions above, the transformation wouldn't apply, but if we had instead (\x -> (\y -> blah y blah) . (force x)) . (delay arg) where arg is "work-free", then the result would be (\x -> (\y -> blah y blah) . (force (delay x))) . arg.

Regarding its relation to the force-delay transformation, it looks like float-delay provides more opportunities for force-delay to fire, and force-delay provides more opportunities for float-delay to fire as well. If you consider a term like (\x -> ... (force ... (force x)) ...) (delay ... (delay arg)) where arg is "work-free", and the number of forces over x and delays over arg is equal, one application of float-delay would "push" a single delay under the force. It's necessary to then run force-delay to simplify the force (delay x) pair to x, and then you can apply float-delay again. So depending on the number of simplifier iterations, a number of these force-delay pairs can get simplified away. In practice, I think the simplifier iterates about 3 times which seems to be enough for real-life programs.

If you ignore the restrictions, you get an unsound transformation. For example, if you apply it even if not every x is under a force:

(\x -> (\y -> x) . (force x)) . (delay arg)
--float-delay-->
(\x -> (\y -> x) . (force (delay x)) . arg
--beta-reduction-->
(\x -> x) . arg
--beta-reduction-->
arg

(\x -> (\y -> x) . (force x)) . (delay arg)
--beta-reduction-->
(\x -> x) . (delay arg)
--beta-reduction-->
delay arg

arg =/= delay arg

I am not entirely sure, however, if the "work-free" requirement is mostly to do with optimisation or if it also protects against modifying the semantics of impure terms. I'll have to look into that.

[effectfully]

I'm not really confident that we need that DecEq X here or that we need it all, maybe there's some way to avoid adding it that I failed to find.

[effectfully]

maybe there's some way to avoid adding it that I failed to find

Actually, we can probably just compute X from n : Nat and that's it. I.e. do this (I didn't try type checking it, not sure if the last line is gonna work for example):

NatToSet : ℕ → Set
NatToSet zero    = ⊥
NatToSet (suc n) = Maybe (NatToSet n)

Relation = ∀ n → NatToSet n ⊢ → NatToSet n ⊢ → Set₁

data Translation (R : Relation) : Relation

I'm not sure if it's more pain or less than the current solution though, could be either way.

[ramsay-t]

I think, at best, this is adding a layer of indirect to the current complexity, without actually removing it... You will have to start littering the code with explicit ns because I suspect Agda won't figure them out for itself. At worst, you will lose the quite elegant typechecking of scopes that James has made with the Maybes (even if they are annoying). What you suggestion does achieve though is making it explicit that everything in the stack is either Maybe or ⊥, and that should make the DecEq problem go away?

[effectfully]

explicit ns because I suspect Agda won't figure them out for itself

I made it explicit, but now that I look at that definition, I think Agda should be able to figure it out, because NatToSet is constructor-headed and ⊢ is injective as well (from the unifier's POV, not theory).

At worst, you will lose the quite elegant typechecking of scopes that James has made with the Maybes (even if they are annoying).

Not sure what you mean.

What you suggestion does achieve though is making it explicit that everything in the stack is either Maybe or ⊥, and that should make the DecEq problem go away?

Yup, you won't need DecEq if you can simply match on n and tell if it's another Maybe inside or the final ⊥.

It may be easier in the sense that you won't need to deal with instance arguments, which were always a pain for me, although it's been a while since I last used them, so maybe they're fine these days.