Interpreter can't reduce top-level definitions

[dhess]

Code of conduct

• I've read the project's code of conduct, and agree to follow it.

Don't report security issues here

• I've read the project's security policy, and I do not believe this bug is a security issue.

Is there an existing issue?

• I've searched GitHub Issues, and I believe this is a new issue

What happened?

While adding the interpreter to the various Primer APIs, I discovered that the interpreter can't reduce top-level definitions. This test demonstrates that the interpreter can't evaluate the even 3? top-level definition in our example even3Prog:

• https://buildkite.com/hackworthltd/primer-ci/builds/82#018efd83-e413-494c-a428-ee50fd50beda/16-32

What should have happened?

The interpreter should be able to reduce a top-level definition whose root node is an App.

Which package(s) or aspect(s) of the project are the source of the issue?

primer

Developers, please provide the output of the bug report script

No response

Do you have a reproducer?

Yes, see above.

Any additional information?

We can't use the interpreter in the frontend until this issue is resolved. See hackworthltd/primer-app#1169

[georgefst]

I can see the problem here, and a potential solution.

The definition of EnvTm/EnvTy says "Invariant: the values in the env will be in normal form.". Yet when creating these with mkGlobalEnv we don't check this. The body of even 3? is even (succ (succ (succ zero))), which is of course not a normal form ("normal form" in this context means "fix point of interp'"). So we instantly hit the Var _ (GlobalVarRef v) branch of interp' which inserts the definition itself, which is then never reduced further.

If we try to reduce these up front by inserting some extra interp' calls in the definition of mkGlobalEnv, we find that those calls need the definition map itself as an argument, and in the mutual recursion case I don't see any simple way to resolve this. Besides, we shouldn't be calling interp' without the timeout logic from interp.

Instead, I've tried starting with an empty context, and converting all top-level defs to a recursive let, using the encoding from #114 (comment). This should be sound, but appears to reveal a separate bug: the perfectly-valid expression which results does not reduce as expected, and instead grows infinitely large.

There is a comment in the source saying "this interpretation af letrec can easily cause deadlocked or infinite-size programs". I'm not sure I'm parsing this correctly (I should have probably asked for clarification in review, but that was a little rushed in the case of #1187 for obvious reasons), and it doesn't seem to be covered explicitly in #1194, but this seems to suggest that maybe this is a known limitation? I haven't yet examined the resulting infinite expression to see exactly what keeps getting expanded.

(This problem has been nagging at me since our discussion on Monday, so I had to have a look. I suppose I got nerd sniped!)

[dhess]

@georgefst Thanks!

The first thing that pops into my head is, what is the fundamental difference between the step evaluator and the interpreter such that the step evaluator isn't caught by this?

[dhess]

Despite my preference to treat top-level definitions as simply module-scoped letrecs, they keep resisting that. So rather than trying to convert them to letrecs during interpretation, should we instead treat them specially in EnvTm/mkGlobalEnv/interp ? I can vaguely imagine an implementation where, when a top-level definition is encountered during a particular interpretation sequence, we force its evaluation.