Clarify evaluation semantics of shared terms

[jfeser]

We've started to think about alternative evaluation strategies (e.g. #594) that take advantage of sharing in terms to avoid redundant work. As part of this work, we should clarify and document the semantics of effectful programs.

We should respect the following equation:

handler(i)(evaluate)(p()) == handler(i)(p)()  # delaying evaluation preserves semantics

Consider a program with two effects f and g:

def p():
  x = f()
  y = g(x, x)
  return y

Our current implementation of evaluate respects this equation only when i is pure, because f is handled twice on the LHS and once on the RHS.

[jfeser]

To follow up on this, actually neither implementation of evaluate fully respects this equation in the presence of handler side effects. There are at least two issues we should consider if we want to give semantic guarantees about side effecting handlers:

• Effect ordering
• Effectful statements

def p():
  x = f(0)
  y = f(1)
  return g(y, x)

def p():
  f()
  return f()

[eb8680]

We should respect the following equation

I doubt this is possible in general without some pretty strong assumptions on p and i. Maybe we can identify some sufficient conditions or find a weaker form of the equation that should hold more broadly.

[jfeser]

Agreed. Here's a weaker version that takes i out of the equation and instead asserts that delayed p and eager p produce the same effect trace:

@contextmanager
def trace():
  ts = []
  def _save(op, *args, **kwargs):
    ts.append((op, *args, **kwargs)
    return fwd()
  with handler({apply: _save}):
    yield ts

e = p()
with trace() as t1:
  evaluate(e)

with trace() as t2:
  p()

assert t1 == t2

I think this version is plausible if p has no native effects (e.g. io, randomness, state). We might need some wrapper like effectful.ops.syntax.trace to scope the effects in p.