Is there a more fluid way to tame scoping of givens?

[liufengyun]

I am writing an interpreter-like program:

enum Expr {
  case Apply(fn: Expr, arg: Expr)
  case Fun(x: String, body: Expr)
  case Var(x: String)
}

import Expr._

type Trace = Vector[Expr]
def trace(using t: Trace): Trace = t

type Env = String => Value
def env(using env: Env): Env = env

case class Closure(fun: Fun, env: Env)
type Value = Closure

type Contextual[T] = (Env, Trace) ?=> T

def eval(e: Expr): Contextual[Value] =
  e match
  case Var(x)         => env(x)
  case fun: Fun       => Closure(fun, env)
  case Apply(fn, arg) =>
    val Closure(fun, env1) = eval(fn)
    val argV = eval(arg)
    given Trace = trace :+ e
    val env2: Env = x => if x == fun.x then argV else env1(x)
    given Env = env2
    eval(fun.body)

In the code above, the following two lines are problematic:

given Trace = trace :+ e
given Env = env2

Two problems:

1. The given is available for its rhs, thus given Trace = trace :+ e will run into cycles
2. The given is available for the previous expression eval(arg) in the same scope, a forward reference again.

As a result, I am forced to break the definition of given Trace = trace :+ e into two lines and using a block:

def eval(e: Expr): Contextual[Value] =
  e match
  case Var(x)         => env(x)
  case fun: Fun       => Closure(fun, env)
  case Apply(fn, arg) =>
    val Closure(fun, env1) = eval(fn)
    val argV = eval(arg)
    val trace2 = trace :+ e
    val env2: Env = x => if x == fun.x then argV else env1(x)
    {
      given Trace = trace2
      given Env = env2
      eval(fun.body)
    }

But what I really want is something like the following:

def eval(e: Expr): Contextual[Value] =
  e match
  case Var(x)         => env(x)
  case fun: Fun       => Closure(fun, env)
  case Apply(fn, arg) =>
    val Closure(fun, env1) = eval(fn)
    val argV = eval(arg)
    val env2 = (x: String) => if x == fun.x then argV else env1(x)
    given Trace = trace :+ e in
      given Env = env2 in
        eval(fun.body)

The hypothetical construct given T = rhs in e is supposed to fix two scoping problem:

• it creates a local scope so that the given not available for statements before or after the given/in in the same block
• the given instance is not available in rhs

[liufengyun]

As a workaround, I ended up with something like the following:

def use[T, R](v: T)(op: T ?=> R): R = op(using v)

def eval(e: Expr): Contextual[Value] =
    ...
    use(trace :+ e) {
      use(env2) {
        eval(fun.body)
      }
    }

With indented-syntax, it looks better:

def use[T, R](v: T)(op: T ?=> R): R = op(using v)

def eval(e: Expr): Contextual[Value] =
    ...
    use(trace :+ e):
      use(env2):
        eval(fun.body)