Functional Programming

We say that an identifier with a matching binder is bound. If there is no matching binder, then we say that the identifier is free. For example, x is bound and y is free in (fun x -> x) y. A term with no free identifiers is called a closed term; a term with some free identifiers is called open.

The free variables of a term can be computed from the syntax of the term as follows. Note that the free variables of a lambda abstraction are the free variables of the body minus the argument name.

def free(expr : Expr) -> set[str]:
    match expr:
	case Lam(var, body):
	    return free(body) - set([var])
	case Var(v):
	    return set([v])
	case App(lhs, rhs):
	    return free(lhs) | free(rhs)
	case Prim(_, args):
	    return set([v for a in args for v in free(a)])
	case If(cond, then, else_):
	    return free(cond) | free(then) | free(else_)
	case (Num() | Bool()):
	    return set([])
	case _:
	    raise RuntimeError("Unexpected expr", expr)

We can check that free is doing what we expect:

In the term fun x -> x (fun x -> x), we say that the inner lambda shadows the outer lambda. Shadowing a variable means that it can no longer be referenced.

In FL, identifiers refer to the most enclosing binder with the same identifier. Binders create a scope, which is the region of the program where the variable can be referred to. We can draw a Stoy diagram for the term (fun a -> a a) (fun a b c -> c a) to make it easier to see the binding structure: (Source: Design Concepts in Programming Languages)

In the diagram, identifiers are replaced with wires that connect them to their binder. This makes it clear that there are two different variables that are referred to as a.

We usually want to ignore the particular variable names used in a term, and instead only consider the binding structure. We say that two terms \(t\) and \(t'\) that have the same Stoy diagram are alpha-equivalent; in other words, \(t\) and \(t'\) differ only in their bound variable names. We'll write this as \(t =_\alpha t'\).

A renaming of the bound variables in a lambda term that preserves the term's α-equivalence class is called an α-renaming. This seemingly simple operation has a number of subtleties, however.

Consider the following lambda term: fun a -> b (fun c -> a). If we naively rename a to b, we get fun b -> b (fun c -> b). Notice that b, which was previously free, is now bound, so the new term is not α-equivalent. We say that b was captured. In this example, b was free, but free variables are not required for capture to occur. If we rename a to c, then we get fun c -> b (fun c -> c). This term is also not α-equivalent, because it changes where c is bound.

These problems mean that not all renamings are acceptable, and we need to be careful to choose a renaming that does not cause a variable to be captured.

We introduce renaming because it is a great way to illustrate capture, but the operation we are really interested in is substitution (and in fact renaming a free variable is a special case of substitution). Substitution replaces all occurrences of a free variable \(I\) in an expression \(E\) with another expression \(E'\). We write this as \([E'/I]E\), which you can read as "substitute \(E'\) for \(I\) in \(E\)." For example, \([(\texttt{fun}\ b \rightarrow b)/a](\texttt{fun}\ c \rightarrow a\ c)\) produces \(\texttt{fun}\ c \rightarrow (\texttt{fun}\ b \rightarrow b)\ c\).

Substitution has the same issues with variable capture that we saw in renaming. Modifying the previous example slightly shows how capture can occur in substitution. Substituting \([(\texttt{fun}\ b \rightarrow c)/a](\texttt{fun}\ c \rightarrow a\ c)\) naively will result in the capture of the free variable c.

Issues with capture arise when substituting into the body of binding constructs. In FL, this means lambdas: \([E/I](\texttt{fun} I' \rightarrow E')\). There are two cases we need to handle:

• If \(I = I'\), then \(I\) is not free in \(E'\), so we perform no substitution.
• Otherwise, we need to substitute inside \(E'\). The question then is what to do if \(I'\) occurs free in \(E\), as in \([b/a](\texttt{fun}\ b \rightarrow b\ a)\). Naive substitution will produce \(\texttt{fun}\ b \rightarrow b\ b\), which captures \(b\) and changes the meaning of the term. We avoid this issue by first renaming \(I'\) in the lambda to a fresh identifier that is not free in either \(E\) or \(E'\). For example, we could rename \(b\) to \(c\) to produce \([b/a](\texttt{fun}\ c \rightarrow c\ a)\). Substitution will then produce \(\texttt{fun}\ c \rightarrow c\ b\).

Why do we need to rename \(I'\) in \(E'\)? What would happen if instead we renamed \(I'\) in \(E\)?

The interesting case is implemented in Python as follows:

case Lam(var, body):
    # If the lambda binds 'v', then it can't be free in 'body'
    if var == v:
	return Lam(var, body)

    # Check if we will capture a variable in 'e1'
    if var in free(e1):
	# If so, rename the lambda parameter before substituting
	fresh_var = fresh(free(e1) | free(body) | set([var]))
	renamed_body = subst(Var(fresh_var), var, body)
	return Lam(fresh_var, subst(e1, v, renamed_body))
    else:
	return Lam(var, subst(e1, v, body))

We can see from the following examples that subst behaves as we expect. If there is no possibility of capture, it does not rename the lambda parameter. If the lambda captures a variable, then the parameter is given a fresh name before substitution proceeds.

We can use the substitution operation to sketch out a big-step operational semantics for FL. We'll call our evaluation relation \(\Downarrow_s\) because it uses substitution.

(There are also rules for reducing primitive operators, but they are exactly what you'd expect, so we omit them.) The first rule just says that lambdas are values. The last two describe how the if-then-else construct works. Note that only one arm of the if-then-else is evaluated.

The most interesting rule here is the application of a lambda to an argument, which we reduce by simply substituting the argument expression into the lambda. This needs to be the capture-avoiding substitution that we discussed earlier.

This kind of evaluation strategy (where the argument expression is substituted without being evaluated first) is also called call-by-name, and it is similar to the strategy used in lazy functional languages like Haskell.

We can implement our semantics in Python as follows. (Again, we've elided eval_prim.)

We're using a little trick here called open recursion (you may have heard of it in the context of object-oriented programming). In this case, we're passing eval_subst as an argument to eval_subst_open instead of making a recursive call. This lets us define a new function eval_subst_print, that prints out each expression before evaluating it, without modifying eval_subst_open.

def eval_subst_open(eval_subst, e : Expr) -> Expr:
    def fail(e) -> NoReturn:
	raise (RuntimeError(f'Evaluation of {e} is stuck.'))

    match e:
	case (Bool() | Num() | Lam()) as val:
	    return val

	case App(lhs, rhs):
	    match eval_subst(lhs):
		case Lam(var, body):
		    return eval_subst(subst(rhs, var, body))
		case v:
		    fail(v)

	case If(cond, then, else_):
	    match eval_subst(cond):
		case Bool(True):
		    return eval_subst(then)
		case Bool(False):
		    return eval_subst(else_)
		case v:
		    fail(v)

	case Prim(op, args):
	    return eval_prim(op, [eval_subst(a) for a in args])

	case e:
	    fail(e)

def eval_subst(expr):
    return eval_subst_open(eval_subst, expr)

def eval_subst_print(expr, indent=0):
    import functools

    print('| ' * indent + f'Eval: {expr}')
    result = eval_subst_open(functools.partial(eval_subst_print, indent = indent + 1), expr)
    print('| ' * indent + f'+---> {result}')
    return result

We can check that our evaluator works as expected by running it on a program that computes \(2 + 1 + 1\) by composing an increment function and a double application function.

We can also give a semantics for FL that doesn't involve substitution. Substitution is a fairly expensive way to evaluate programs, so in practice implementers use closures. A closure is a pair \((E, \sigma)\) of an expression and an environment (a mapping from name to value). You can think of a closure as a kind of delayed substitution. Instead of performing the substitutions up front, we remember the substitutions that we should have made in \(\sigma\) and look them up as needed. We track the current binding environment in \(\sigma\), and when we encounter a lambda, we capture that environment.

Rules for if-then-else are left as an exercise for the reader :).

We can implement these rules in Python as follows:

def update(env, var, value):
    env = env.copy()
    env[var] = value
    return env

def env_to_string(env):
    return '{%s}' % (', '.join(f'{k}: {v}' for (k, v) in env.items()))

@dataclass
class Closure(Expr):
    body: Expr
    env: dict[str, Expr]

    def __str__(self):
	return f'({self.body}, {env_to_string(self.env)})'

def eval_closures_open(
    eval_closures: Callable[[Expr, dict[str, Expr]], Expr],
    e: Expr,
    env: dict[str, Expr],
) -> Expr:
    def fail(e, env):
	raise (RuntimeError(f"Evaluation of {e} in {env} is stuck."))

    match e:
	case Bool() | Num():
	    return e

	case Var(v):
	    if v in env:
		match env[v]:
		    case (Bool() | Num()) as x:
			return x
		    case Closure(body, cenv):
			return eval_closures(body, cenv)
	    fail(e, env)

	case Lam():
	    return Closure(e, env)

	case App(lhs, rhs):
	    match eval_closures(lhs, env):
		case Closure(Lam(var, body), closure_env):
		    closure_env = update(closure_env, var, Closure(rhs, env))
		    return eval_closures(body, closure_env)
		case e:
		    fail(e, env)

	case If(cond, then, else_):
	    match eval_closures(cond, env):
		case Bool(True):
		    return eval_closures(then, env)
		case Bool(False):
		    return eval_closures(else_, env)
		case e:
		    fail(e, env)

	case Prim(op, args):
	    return eval_prim(op, [eval_closures(a, env) for a in args])

	case e:
	    fail(e, env)

def eval_closures_print(expr, env, indent=0):
    import functools

    print('| ' * indent + f'Eval: {expr} in {env_to_string(env)}')
    result = eval_closures_open(functools.partial(eval_closures_print, indent = indent + 1),
				expr, env)
    print('| ' * indent + f'+---> {result}')
    return result

def eval_closures(e : Expr, env : dict[str, Expr]) -> Expr:
    return eval_closures_open(eval_closures, e, env)

Applying our new interpreter to the example that we used above, we see that it computes the same result.