This paper was converted on www.awesomepapers.org from LaTeX by an anonymous user.
Want to know more? Visit the Converter page.

Free Variable as Effect, in Practice

Oleg Kiselyov 0000-0002-2570-2186 Tohoku UniversityJapan [email protected]
Abstract.

Variable environment is the time-honored way of making sense of free variables, used in programming language theory as well when writing interpreters and some compilers. Algebraic effects give another way, as was pointed already at HOPE 2017. Although a theoretical curiosity, it may have surprising practical benefits: a new way of writing compilers, with the incremental type-checking, with easy variable usage, leaf function analyses. This work-in-progress report prototypes and illustrates the idea.

††copyright: none

1. Introduction

Whenever one writes an interpreter or a compiler, or studies logic, model theory, programming language theory – one soon has to face variables. The well-known way to deal with them is by introducing an environment, or variable assignment in logic. There is, however, another, more general approach, related to algebraic effects. One should not be too surprised. Algebraic effects originate from studying terms with variables, and equations on them: free algebras.

The algebraic effect approach was already described at HOPE 2017 (Kiselyov, 2017) and elaborated at (Kiselyov, 2023). It was explored and scaled up in the study of rigorous, realistic and interesting reasoning with effects (Kiselyov et al., 2021).

Here we look at an unexpected practical side, in interpreting or compiling languages. It has occurred to me as I was teaching compiler class developing the complete compiler to x68-64 assembly feature-by-feature, and in tagless-final style.

The first benefit is the ability to evaluate intermediary expressions and report errors soon, before the whole program is parsed – hence reducing the amount of memory for intermediary data and improving latency. The approach also facilities variable usage and leaf function analyses, indispensable in compilation.

2. Interpreting Languages with Variables

To explain the idea, let’s write an interpreter, which we later turn into a compiler by changing the domain of interpretation.111The complete code accompanying the paper is available at https://okmij.org/ftp/Computation/var-effect/ In rough strokes the development, however simplified, actually follows the compiler class.

We start with the simplest interpreter: the source language has only integers and addition. The language should hopefully be clear from the grammar, in the (ocaml)yacc form. We borrowed this example from the ocamllex/ocamlyacc chapter of the OCaml Reference (Leroy et al., 2022, §15.6).

⬇
exp: INT { int $1 }
∣\mid exp PLUS exp { add $1 $3 }
∣\mid LPAREN exp RPAREN { $2 } ;

The grammar defines the concrete syntax of the language. The semantic actions int and add are arranged in a separate module with the following signature, which in effect, defines the abstract syntax.

⬇
type repr (* representation type *)
val int : int →\rightarrow repr
val add : repr →\rightarrow repr →\rightarrow repr
type obs (* observation type *)
val observe : repr →\rightarrow obs
end

Where repr is the domain of the interpretation.

Here is one implementation of the signature.

⬇
type dom == int
type repr == dom
let int x == x
let add x y == let s == x ++ y in printf ”␣␣␣==>>␣%d\n%!” s; s
type obs == unit
let observe x == string_of_int x |>|\!{>} print_endline
end

The value domain is int (OCaml integers), which is also the domain of interpretation repr. The function observe is invoked after the parsing is finished; it observes the repr value representing the result of the whole program, by printing it. We also made the interpreter to print the (intermediate) results, of each addition expression. As we shall see, it is a good diagnostic for the evaluation order.222as well as memory requirements: deferring a computation needs memory to store what is to compute later.

Let’s add variables. We add the productions

⬇
∣\mid IDENT { var $1 }
∣\mid LET IDENT EQ exp IN exp { let_ ($2,$4) $6 }

to the parser, and likewise extend the abstract syntax. By ‘extending’ we mean creating a new version re-using the old code – in its already compiled form, and without any copy-pasting or editing.

⬇
include LangInt
type name == string
val var : name →\rightarrow repr
val let_ : name * repr →\rightarrow repr →\rightarrow repr
end

Its implementation also re-uses EvalInt, but re-defines all operations:333Here ≫\gg is left-to-right function composition

⬇
type dom == EvalInt.dom
type name == string
type env == (name * dom) list
type repr == env →\rightarrow dom
let ans : dom →\rightarrow repr == fun v →\rightarrow fun _env →\rightarrow v
let lift2 : (dom→\rightarrowdom→\rightarrowdom) →\rightarrow (repr→\rightarrowrepr→\rightarrowrepr) == fun op e1 e2 →\rightarrow
fun env →\rightarrow op (e1 env) (e2 env)
let int == EvalInt.int ≫\gg ans
let add == lift2 EvalInt.add
let var : name →\rightarrow repr == List.assoc
let let_ : name * repr →\rightarrow repr →\rightarrow repr == fun (n,b) body →\rightarrow
fun env →\rightarrow body ((n,b env) :: env)
type obs == unit
let init_env : env == []
let observe x == x init_env |>|\!{>} EvalInt.observe
end

To handle variables, we introduce the variable environment env – here, the associated list of variable names and their meanings – as explained in every textbook about interpreters. The domain of interpretation is now a function from env to the value domain, to which the earlier semantic functions are lifted. Again, the interpretation is completely standard and explained in every textbook on this topic.

What the textbooks rarely point out is an undesirable change. In the original EvalInt, the (intermediate) result of a sub-expression is printed as soon as it is parsed. When we enter ”1++2\n++3\n++4\n” we see the partial sums printed as soon as we hit ‘Enter’. EvalInt indeed works as the familiar desk calculator.444In fact, it makes a simpler and clearer example than the one in the ocamlyacc’s reference manual.

EvalEnv is different: As we enter the same ”1++2\n++3\n++4\n”, nothing is printed. It is only when we terminate the input and tell the parser the whole program is finished that we see the results. Whereas EvalInt interprets as the program is being parsed, EvalEnv does the real work (summation) only after the whole program has been parsed. It is not hard to see why.

The meaning of 1++2 in the EvalInt semantics is 3 (computed compositionally). In the EvalEnv semantics, the same expression has the meaning

⬇
fun env →\rightarrow (fun _ →\rightarrow 1) env ++ (fun _ →\rightarrow 2) env

which is a function. Its body is not evaluated until it receives the env argument – even if the argument is not needed. That argument, the initial environment, is passed by observe only when the entire program is parsed. One may notice that m12_env has the structure of the corresponding source expression 1++2 – obviously, since the meaning assignment is a homomorphism. The meaning is a function (closure) that references the meanings of 1 and 2, which are also closures. In effect, m12_env is a parse tree of the source expression 1++2 – in a form of closures and taking hence more memory compared to a data structure. This parse tree is interpreted upon the final observation.

What EvalEnv gained, however, is handling programs with variables like (1++2)++x – which cannot be evaluated until we receive the environment and look up the value of x. Still, the sub-expression (1++2) could be interpreted on the spot. How to make it happen?

2.1. Variable as an Effect

When dealing with expressions like (1++2)++x, we need to know what value corresponds to x. We can just ask. The meaning of an expression is then either an answer A(v), or a question Q(n,k) about the value of the variable n, to be continued as k, perhaps asking further questions until the final answer. We hence introduce the following variable effect (which is the Free monad implementation of the Reader effect, and entirely standard):

⬇
type name == string
type δ\delta t == A of δ\delta ∣\mid Q of name * (δ\delta →\rightarrow δ\delta t)
let ans : δ\delta →\rightarrow δ\delta t == fun v →\rightarrow A v
let var : name →\rightarrow δ\delta t == fun n →\rightarrow Q(n,ans)
let rec lift2 : (δ\delta→\rightarrowδ\delta→\rightarrowδ\delta) →\rightarrow (δ\delta t →\rightarrow δ\delta t →\rightarrow δ\delta t) == fun op e1 e2 →\rightarrow
match (e1,e2) with
∣\mid (A v1, A v2) →\rightarrow A (op v1 v2)
∣\mid (Q (n,k), e2) →\rightarrow Q (n, (fun v →\rightarrow lift2 op (k v) e2))
∣\mid (e1, Q (n,k)) →\rightarrow Q (n, (fun v →\rightarrow lift2 op e1 (k v)))
let lift : (δ\delta →\rightarrow δ\delta t) →\rightarrow (δ\delta t →\rightarrow δ\delta t) == …
let handle_var : (δ\delta →\rightarrow δ\delta t) →\rightarrow (name →\rightarrow δ\delta option) →\rightarrow δ\delta t →\rightarrow δ\delta t == …
let letv : (name * δ\delta) →\rightarrow δ\delta t →\rightarrow δ\delta t == fun (n,v) →\rightarrow
handle_var ans (function n’ when n’==n →\rightarrow Some v ∣\mid _ →\rightarrow None)
let top_hand : δ\delta t →\rightarrow δ\delta == function A v →\rightarrow v
end

A binary operation on two expressions lift2 op checks to see if both operands have the answer. If so, the operation op can be performed right away. Otherwise, lift2 propagates operand’s questions. Eventually, the questions have to be answered, which is the job of a handler. The handler handle_var is the mapping/fold over the denotation (δ\delta t tree). Its particular instance letv replies to questions only about the given name, propagating all others. The domain of interpretation is now dom VarEff.t, to which the semantic functions are lifted:

⬇
module V == VarEff
type dom == EvalInt.dom
type repr == dom V.t
let int == EvalInt.int ≫\gg V.ans
let add == V.lift2 EvalInt.add
let var == V.var
let let_ : name * repr →\rightarrow repr →\rightarrow repr == fun (n,b) body →\rightarrow
V.lift (fun v →\rightarrow V.letv (n,v) body) b
type obs == unit
let observe x == V.top_hand x |>|\!{>} EvalInt.observe
end

As expected, let_ acts as a handler, answering questions about its bound variable, and propagating all other questions up. One may show, using the technique in (Kiselyov et al., 2021), that EvalEff.repr has the same equational theory as EvalEnv.repr – that is, EvalEff is extensionally equivalent to EvalEnv. Still, ”(1++2)\n++x\n” and ”x++(1++2)\n++3” now print the result of interpreting 1++2 right away, without waiting for the whole program to be parsed. Furthermore, when we enter the program

⬇
in x ++ x ++ 3 in
y ++ 1;;

we not only see 1++2 being evaluated right away, but also x++x++3 being evaluated as soon as it has been parsed, at the end of the second line.555One can see that for themselves by compiling and running the code in the directories step2 and step3 in the accompanying code. The former implements the environment and the latter effect semantics for variables. Questions about local variables can therefore be answered quickly, without waiting for the whole program be parsed.666However, straightened-out let-expressions are right-associated. Therefore, their parsing finishes only at the end of the program.

EvalEff offers further opportunities for optimization: if the body of a let-expression has A v as its interpretation (denotation) – that is, not a question – the body has not needed the value of the bound variable. We have hence come upon an easy way to determine the usage of bound variables, which is valuable in compilation, as we shall see in the next section.

The variable-as-effect approach scales up to functions – as was in effect shown already in (Kiselyov, 2017). Here are two sample programs777see step4 in the accompanying code.

⬇
let fun f(y) == x ++ y in
let x == 2 in f(2)
let x == 1 in
let fun f(y) == x ++ y in
let fun g(x) == f(x) in
g(2)

Since a variable dereference is an effect, to be handled by a dynamically enclosed handler, one may wonder if we are really implementing lexical rather than dynamic binding. As was shown already in (Kiselyov, 2017) and elaborated in (Kiselyov, 2023), variable-dereference-as-effect does support lexical binding, with some work. Generally, a mechanism to capture the current dynamic environment is needed. The current implementation uses a simpler approach: handling the body of a function in the handling environment of its definition rather than of its invocation. Therefore, both sample programs evaluate to 3.

3. Compilation

The ability of EvalEff to evaluate as soon as possible, without waiting for the whole program to be parsed is especially valuable in compilation, where it translates to reporting type and other errors early and reducing memory footprint. There is another benefit, hinted earlier: the ease of variable use analyses, which are needed for memory/register allocation. This section demonstrates both benefits.

First, we turn our interpreter into a compiler, to Wasm. We change the interpretation domain from int to a sequence of Wasm instructions that leave the int result on the stack.

⬇
type dom == Wasm.instr
type repr == dom
let int == Wasm.I32.const
let add x y == Wasm.(exp [x; y; I32.add])
type obs == unit
let observe x ==
let open Wasm in
wasm_module [func ~result:I32 [x]] |>|\!{>} observe
end

We rely on the module Wasm: tagless-final embedding of Wasm.888see the directory wasm in the accompanying code. The new EvalInt_wasm is quite like EvalInt, structurally. It interprets ”1++2++3” as:

Just as we lifted EvalInt to EvalEff in §2.1, we lift Eval_wasm; the result, to be called Eval_var, is EvalEff with EvalInt replaced with Eval_wasm. One may now compile programs with local variables; for example,

produces:

⬇
i32.const 10 i32.const 11 i32.add i32.add i32.const 3 i32.add

The variable x turns out substituted with its bound expression: the let-binding got inlined. One should not be too surprised: after all, variables are like named ‘holes’ in the domain, with let-expressions telling how to fill the holes. Such behavior of let-expressions – effecting sharing in the compiler rather than in the object code – is well-known in code generation (Swadi et al., 2006).

To properly compile let-expressions, allocating storage (Wasm locals) for bound variables, we lift Eval_var one more time.999see step7, in particular, eval.ml in that directory. In other words, we generate Wasm with ‘holes’, to be filled with the names of the allocated Wasm locals. The allocation is performed after a let-expression is compiled and the variable usage in its body is determined. Strictly speaking, the compilation becomes two-pass. However, the first pass generates as much Wasm code as possible. Local let-expressions can even be compiled entirely before the end of parsing of the whole program.

The let-handler is particularly notable:

⬇
let cnt == ref 0 in (* usage count of n *)
let vars == ref [] in (* other variables used *)
let lkup == function
∣\mid n’ when n == n’ →\rightarrow incr cnt; Some (V.var n)
∣\mid n’ →\rightarrow if List.mem n’ !vars then () else vars :=\mathrel{{:}{=}} n’ :: !vars; None
in
let ret res ==
if !cnt == 0 then V.ans res (* no need to allocate anything *)
else if !cnt == 1 then V.ans (Eval_var.let_ (n,v) res) (* inline *)
else
(* request allocation, reporting n and the list of alive,
hence conflicted variables *)
in V.handle ret lkup b

As the handler answers questions about its bound variable, it counts them. At the end, it knows how many times the bound variable has been accessed. If zero, there is no need to allocate storage for the variable. (If the source language has no side effects, as ours currently, we may even skip compiling the bound expression). If the variable was used only once, we substitute it with the bound expression, using Eval_var’s let-machinery to do the substitution. Again, no storage allocation is needed. The letv-handler also watches for other variable requests, and learns of all free variables in its managed expression. Their list is reported to the allocator: these are conflicts, i.e., their storage must be disjoint. We thus obtain all the information (variable usage and conflicts) needed for storage allocation; see the source code for details.

For example, the program

compiles to the following Wasm module

⬇
(module (func (export ”start” ) (result i32 )
(local $t_1 i32) (local $t_2 i32)
(i32.const 1) (i32.const 2) i32.add local.set $t_1 local.get $t_1
(i32.const 1) i32.add local.set $t_2 local.get $t_2 local.get $t_1 i32.add
local.set $t_1 local.get $t_1 local.get $t_1 i32.add local.get $t_2 i32.add))

The variables x and z share the same Wasm local t_1.

Let us add functions – for simplicity, second-class top-level functions whose bodies have no free variables aside from the arguments (since functions are second class, their names are distinct from ordinary variable names).101010Compiling functions with ‘open bodies’ is rather challenging: Wasm intentionally prohibits accessing locals from a different function. To use locals as much as possible we would need an extensive variable use analysis, which should be feasible in our approach. This is the topic for future work. Here is an example:

⬇
let fun g(x,y) == f(y) ++ x in
f(g(1,2))

Since functions may take several arguments, there comes the possibility of applying a function to a wrong number of arguments – which is a type error. We should report it at the compilation time.

The language with top-level second-class functions Lang2Fun is the extension of LangLet with function calls and function declarations:

⬇
include LangLet
val call : name →\rightarrow repr list →\rightarrow repr
type fundecl (* function declaration *)
val defun : name * name list * repr →\rightarrow fundecl
type defns (* a sequence of fundecl *)
val defn_empty : defns
val defn_add : defns →\rightarrow fundecl →\rightarrow defns
type topform
val top_exp : defns →\rightarrow repr →\rightarrow topform
val topf_observe : topform →\rightarrow obs
end

Here, defun interprets a declaration (the function name, the list of argument names and the function body) as fundecl. Since functions may only be declared at top-level and may not refer to outside variables, all function declarations have to appear at the beginning of the program, followed by the top-level expression (main program body) – which is what topform signifies. The compilation for function bindings and function calls is not much different from what we have seen for integer-type let-expressions. A question about a function name is answered with its type (i.e., arity) and the Wasm name111111Function names may be re-defined but Wasm names are unique. (needed to generate the Wasm call instruction). We refer to the accompanying code for details (see the directory step8).

We have claimed that the effect semantics for variable and function names enables incremental type checking and the early reporting of errors. Let us see. First, consider the OCaml code:

⬇
let g(y) == f(y,1) ++ y
f(g(1XXX

with two problems. On line 2 the function f is invoked with a wrong number of arguments. Then there is a parse error on line 3. Although it occurs later in the code, it and only it is reported by the OCaml compiler:

⬇
^^^^
Error: Invalid literal 1XXX

Indeed, an OCaml program must first be completely parsed, and only then type-checked. When writing or refactoring code, however, one would have liked to type check fragments (definitions) as soon as they are finished, before the whole program is completed.

In contrast, if we submit the similar code

⬇
let fun g(y) == f(y,1) ++ y in
f(g(1XXXX

to our compiler, we get the compilation error about the first problem:

⬇
Function f requires 1 arguments but was invoked with 2

In fact, if we feed the code into the compiler line-by-line, we notice that the error is reported right after the second line is entered – before the third, ill-formed, line is even input.

4. Conclusions

In the environment semantics the meaning of an expression is a function from the environment, which is opaque and cannot be examined. We cannot tell which variables in the environment have actually been used, and how many times. Algebraic effects make the denotation more observable: a handler can watch questions and find out which variables have been asked about, and how many times. Thus we obtain the variable usage analysis in the ordinary course of compilation, almost for free, so to speak.

It remains to be seen how this promise holds for a real compiler for a realistic programming language. I intend to find it out by trying this technique out in the new installment of the compiler class (which is underway).

Acknowledgements.
I thank Chung-Chieh Shan for helpful discussions, and the reviewers and participants of the HOPE 2023 workshop for many insightful comments.

References

  • Kiselyov [2017] Oleg Kiselyov. Higher-order programming is an effect, 2017. HOPE Workshop at ICFP 2017.
  • Kiselyov [2023] Oleg Kiselyov. Free variables and free effects: An elementary introduction to algebraic effects and handlers. https://okmij.org/ftp/Computation/variables-effects.html, 2023.
  • Kiselyov et al. [2021] Oleg Kiselyov, Shin-Cheng Mu, and Amr Sabry. Not by equations alone: Reasoning with extensible effects. J. Functional Programming, 31:e2, 2021. doi: 10.1017/S0956796820000271.
  • Leroy et al. [2022] Xavier Leroy, Damien Doligez, Jacques Garrigue Alain Frisch, Didier Rémy, and Jérôme Vouillon. The OCaml system, release 4.14, Documentation and user’s manual, 28 March 2022. http://caml.inria.fr/pub/docs/manual-ocaml/index.html.
  • Swadi et al. [2006] Kedar Swadi, Walid Taha, Oleg Kiselyov, and Emir Pašalić. A monadic approach for avoiding code duplication when staging memoized functions. In PEPM, pages 160–169, 2006.