Differences

This shows you the differences between two versions of the page.

--- creating:actions [2025/06/06 18:54] – Parsing & interpreting variable declarations ahelwer
+++ creating:actions [2025/11/03 23:08] (current) – One more instanceof-cast ahelwer
@@ Line 31: / Line 31: @@
 What this means is that we only support certain types of expressions incorporating primed variables, so we restrict ourselves to only model-checking TLA⁺ specs written in a particular idiom.
-====== Variables and Priming ======
 Let's start by supporting a simple operation on primed variables, expressions of the form ''x' = expr''.
 There is a fair bit of groundwork necessary to reach that point.
-===== Variable Declarations =====
+===== Declaring State Variables =====
 First off we have to add support for variable declarations; these are top-level syntactic constructs that look like ''VARIABLES x, y, z''.
 Create a new statement type for them in the ''GenerateAst'' class:
@@ Line 45: / Line 45: @@
     ));
 </code>
 Then use the old ''do''/''while'' trick to parse comma-separated variable names in the ''declaration()'' method of the ''Parser'' class:
 <code java [highlight_lines_extra="4,5,6,7,8,9,10"]>
@@ Line 62: / Line 63: @@
 Before we can define a ''Stmt.VarDecl'' visitor, we need to come up with a way to manage variables & states.
-It's simplest to copy the ''Environment'' approach and record the current state as a field in the ''Interpreter'' class:
+The interpreter must keep track of only two states: the current state, and the next state.
-<code java [highlight_lines_extra="6"]>
+Each state is a mapping from strings - representing variables - to values.
+The interpreter also must keep track of the set of declared variables.
+For this we add three new fields near the top of the ''Interpreter'' class:
+<code java [highlight_lines_extra="6,7,8"]>
 class Interpreter implements Expr.Visitor<Object>,
                              Stmt.Visitor<Void> {
   final Environment globals;
   private Environment environment;
-  private final PrintStream out;
-  private State state = new State();
-</code>
-This requires a new class!
-Create a file called ''State.java''; for now, this just supports the ability to declare variables; it also produces an error if the user attempts to declare the same variable twice:
-<code java>
-package tla;
-import java.util.HashMap;
-import java.util.Map;
-class State {
+  private final Map<String, Token> variables = new HashMap<>();
-  private Map<String, Token> variables = new HashMap<>();
+  private Map<String, Object> current = null;
+  private Map<String, Object> next = new HashMap<>();
+</code>
-  boolean isDeclared(Token name) {
+We choose to initialize the ''current'' state to ''null'' because when the interpreter is created, the system's initial state has not yet been defined.
-    return variables.containsKey(name.lexeme);
+The system's initial state will be built in ''next'', which then eventually becomes ''current''.
-  }
-  void declareVariable(Token name) {
-    if (isDeclared(name)) {
-      throw new RuntimeError(name, "Redeclared state variable.");
-    }
-    variables.put(name.lexeme, name);
-  }
-}
-</code>
-That's enough to implement ''visitVarDeclStmt()'' in the ''Interpreter'' class:
+The new fields are enough to implement ''visitVarDeclStmt()'' in the ''Interpreter'' class:
 <code java>
   @Override
@@ Line 103: / Line 87: @@
     checkNotDefined(stmt.names);
     for (Token name : stmt.names) {
-      state.declareVariable(name);
+      variables.put(name.lexeme, name);
+      next.put(name.lexeme, new UnboundVariable(name));
     }
@@ Line 110: / Line 95: @@
 </code>
-In intepreter mode we continue to support redefining operators, but will produce an error if the user attempts to redefine an operator as a state variable or vice versa.
+This requires a new datatype!
-Add this check to the ''visitOpDefStmt()'' method of the ''Interpreter'' class:
+What is the value of a variable when it is declared but not yet bound to a value?
-<code java [highlight_lines_extra="2,3,4"]>
+It must be a new null type, which we will call ''UnboundVariable''.
+Add ''UnboundVariable'' as a new record type near the top of the ''Interpreter'' class:
+<code java [highlight_lines_extra="4,5,6,7,8,9"]>
+class Interpreter implements Expr.Visitor<Object>,
+                             Stmt.Visitor<Void> {
+  private record UnboundVariable(Token name) {
+    @Override
+    public String toString() {
+      return name.lexeme;
+    }
+  }
+  final Environment globals;
+</code>
+It's important to keep variable declarations & operator definitions disjoint.
+In interpreter mode we continue to support redefining operators, but should produce an error if the user attempts to redefine an operator as a state variable or vice versa.
+Add the highlighted code to ''visitOpDefStmt()'' in the ''Interpreter'' class:
+<code java [highlight_lines_extra="9,10,11"]>
   public Void visitOpDefStmt(Stmt.OpDef stmt) {
-    if (state.isDeclared(stmt.name)) {
+    checkNotDefined(stmt.params);
+    for (Token param : stmt.params) {
+      if (param.lexeme.equals(stmt.name.lexeme)) {
+        throw new RuntimeError(param, "Identifier already in use.");
+      }
+    }
+    if (variables.containsKey(stmt.name.lexeme)) {
       throw new RuntimeError(stmt.name, "State variable redeclared as operator.");
     }
     TlaOperator op = new TlaOperator(stmt);
-    environment.define(stmt.name, op);
 </code>
 Also augment the ''checkNotDefined()'' helper method, so state variables cannot be shadowed by operator parameters:
 <code java [highlight_lines_extra="7,8,9"]>
@@ Line 129: / Line 140: @@
       }
-      if (state.isDeclared(name)) {
+      if (variables.containsKey(name.lexeme)) {
         throw new RuntimeError(name, "Name conflicts with state variable.");
       }
@@ Line 135: / Line 146: @@
 </code>
-===== Variable Values =====
+===== Reading, Priming, & Setting State Variables =====
+To resolve variable values, modify the ever-more-complicated ''visitVariableExpr()'' method of the ''Interpreter'' class to first check whether it's resolving a variable, falling back to an ''environment'' lookup if not:
+<code java [highlight_lines_extra="2,3,4,5"]>
+  public Object visitVariableExpr(Expr.Variable expr) {
+    Object referent =
+      variables.containsKey(expr.name.lexeme)
+      ? (primed ? next : current).get(expr.name.lexeme)
+      : environment.get(expr.name);
+    if (!(referent instanceof TlaCallable)) {
+</code>
+This makes use of yet another field we must add to the ''Interpreter'' class, ''primed'':
+<code java [highlight_lines_extra="2"]>
+  private Map<String, Object> next = new HashMap<>();
+  private boolean primed = true;
+  public Interpreter(boolean replMode) {
+</code>
+The ''primed'' field controls whether variable values are pulled from the ''current'' or ''next'' states.
+When inside a primed expression, variables are pulled from ''next''; when outside of primed expressions, variables are pulled from ''current''.
+The ''primed'' field is initialized to ''true'', since the interpreter builds the system's initial state in the ''next'' field so we want all expressions to be implicitly primed at first.
+We can now finally define the prime operator for real, in ''visitUnaryExpr()'' in the ''Interpreter'' class:
+<code java [highlight_lines_extra="4,5,6,7,8,9,10,11,12,13,14"]>
+  public Object visitUnaryExpr(Expr.Unary expr) {
+    switch (expr.operator.type) {
+      case PRIME: {
+        if (primed) {
+          throw new RuntimeError(expr.operator,
+              current == null
+              ? "Cannot prime expression in initial state."
+              : "Cannot double-prime expression.");
+        } try {
+          primed = true;
+          return evaluate(expr.expr);
+        } finally {
+          primed = false;
+        }
+      } case ENABLED: {
+</code>
+Double-priming an expression or priming an expression in the initial state are both fatal errors in TLA⁺.
+The meaning of priming an expression is that all state variables within that expression are primed, so the way the expression is evaluated is fundamentally changed.
+This is why the prime operator somewhat uniquely modifies the state of the ''Interpreter'' instance itself.
+Similar to in ''executeBlock()'', we wrap this ''Interpreter'' state modification inside a ''try''/''finally'' block to ensure that if the evaluation produces a runtime exception, ''primed'' is reset to ''false'' so the ''Interpreter'' instance is not left in a corrupted state.
+We can retrieve state variable values, but what about assigning them?
+To start, let's handle the simple case of expressions of the form ''x' = expr''.
+This requires modifying the ''EQUAL'' case of ''visitBinaryExpr()'' in the ''Interpreter'' class.
+If the ''left'' operand is an ''UnboundVariable'' instance, then bind the ''left'' state variable to the value of ''right'':
+<code java [highlight_lines_extra="2,3,4,5"]>
+      case EQUAL:
+        if (left instanceof UnboundVariable var) {
+          next.put(var.name().lexeme, right);
+          return true;
+        }
+        return left.equals(right);
+</code>
+We only modify variable values in ''next'', not ''current''; variable values in ''current'' should be considered immutable, and we will never let an ''UnboundVariable'' value into the ''current'' state.
+===== Nondeterminism =====
+In TLA⁺, states generally do not have only one successor state.
+Instead, there are usually multiple possible states to transition to.
+This is called nondeterminism, and is a key TLA⁺ feature enabling modeling of concurrent scheduling & much more.
+Nondeterminism is expressed in TLA⁺ through the use of disjunction; for example:
+<code haskell>
+Action ==
+  \/ x' = 0
+  \/ x' = 1
+</code>
+The ''Action'' predicate matches next states where ''x'' is //either// 0 or 1.
+This means ''Action'' represents a nondeterministic step where the system can arbitrarily move to a state where ''x'' is 0, or a state where ''x'' is 1.
+Currently, we store the next state in a single field in the ''Interpreter'' class.
+How can we represent & compute with multiple possible next states?
+The answer is to add another field to the ''Interpreter'' class, holding the set of identified possible next states:
+<code java [highlight_lines_extra="3"]>
+  private Map<String, Object> current = null;
+  private Map<String, Object> next = new HashMap<>();
+  private Set<Map<String, Object>> possibleNext = new HashSet<>();
+  private boolean primed = true;
+  public Interpreter(boolean replMode) {
+</code>
+When our interpreter finds multiple possible next states, it tosses them into ''possibleNext'' for later consideration and continues evaluating & binding the variables in the next state currently under construction.
+Then some top-level loop churns through the ''possibleNext'' set, either ruling out or accepting each possible next state until none remain.
+We will write this very critical top-level loop now; create a new method ''getNextStates()'' in the ''Interpreter'' class:
+<code java>
+  List<Map<String, Object>> getNextStates(Token location, Expr action) {
+  }
+</code>
+''getNextStates()'' will use the following algorithm:
+  - Clear the ''next'' state and push it onto ''possibleNext''
+  - While states remain in ''possibleNext'', choose one, set it as ''next'', and evaluate ''action''
+  - If ''action'' evaluates to ''true'' and also results in a complete ''next'' state with all variables bound to values, add ''next'' to a set of confirmed next states
+  - Evaluating ''action'' might have pushed more states onto ''possibleNext'', so repeat the process until ''possibleNext'' is empty
+  - Return the set of confirmed next states
+Here's how we set up everything outside of the central loop:
+<code java [highlight_lines_extra="2,3,4,5,6,8,9,10,11,13"]>
+  List<Map<String, Object>> getNextStates(Token location, Expr action) {
+    Set<Map<String, Object>> confirmedNext = new HashSet<>();
+    clearNext();
+    possibleNext.add(new HashMap<>(next));
+    try {
+      while (!possibleNext.isEmpty()) {
+      }
+    } finally {
+      clearNext();
+    }
+    return new ArrayList<>(confirmedNext);
+  }
+</code>
+We use the familiar ''try''/''finally'' approach when evaluating expressions within a modified ''Interpreter'' state to ensure runtime exceptions do not corrupt the ''Interpreter'' instance.
+We also use the ''new HashMap<>(next)'' copy constructor to copy ''next'' before putting it in ''possibleNext'', which avoids a //very// subtle bug: since evaluating the action modifies the values in ''next'', and we put ''next'' into a ''HashMap<>'' which records its position by calculating a hash of the value of ''next'', if we subsequently modify the same object put into the ''HashMap<>'' then that value will get "lost" in the datastructure, because its hash value changed.
+For more on this peculiar issue, consult the Java ''[[https://docs.oracle.com/javase/8/docs/api/java/util/Map.html|Map<>]]'' documentation which warns against using mutable objects as keys.
+This code also requires a new ''clearNext()'' helper method in the ''Interpreter'' class, which does what you might expect from the name; it clears ''possibleNext'' then unbinds all variables in ''next'':
+<code java>
+  private void clearNext() {
+    possibleNext = new HashSet<>();
+    next = new HashMap<>();
+    for (Token variable : variables.values()) {
+      next.put(variable.lexeme, new UnboundVariable(variable));
+    }
+  }
+</code>
+Now we can write the central ''getNextStates()'' loop:
+<code java [highlight_lines_extra="2,3,4,5,6,7"]>
+      while (!possibleNext.isEmpty()) {
+        Map<String, Object> trunk = possibleNext.iterator().next();
+        next = new HashMap<>(trunk);
+        Object satisfied = evaluate(action);
+        checkBooleanOperand(location, satisfied);
+        if ((boolean)satisfied && isComplete()) confirmedNext.add(next);
+        possibleNext.remove(trunk);
+      }
+</code>
+Note again the judicious use of ''HashMap<>'' copy constructors to avoid the mutable ''HashMap<>'' key bug.
+This code requires yet another ''Interpreter'' helper method to check whether a next state candidate is complete (has all variables assigned to concrete values):
+<code java>
+  private boolean isComplete() {
+    return !variables.isEmpty() && next.values().stream()
+        .noneMatch(v -> v instanceof UnboundVariable);
+  }
+</code>
+It's worth spending some time considering the ''getNextStates()'' method.
+From a pure functional perspective the approach is quite displeasing; our interpreter isn't just evaluating expressions anymore, it's also spewing out a bunch of half-baked states on the side.
+This side-effectful method makes it quite a bit harder to reason about the current state of our interpreter, but within the limitations of the Java language the method is appropriate.
+There is also the question of termination.
+What is preventing ''getNextStates()'' from entering an infinite loop?
+The answer is that we only add a state to ''possibleNext'' if either it is //already// in ''possibleNext'' (in which case it is de-duplicated) or after binding the value of at least one more variable than is bound in the ''next'' state under consideration.
+Thus the number of variables bound to concrete values in ''possibleNext'' increases monotonically, eventually encompassing all declared variables and terminating the loop.
+Let's get concrete.
+How do we add states to ''possibleNext'' while evaluating disjunction?
+For each disjunct, we use a fresh copy of the ''next'' state, then evaluate the disjunct and add the resulting modified ''next'' state to ''possibleNext''.
+As described above, this state will either already be in ''possibleNext'' (so be de-duplicated) or have bound the value of at least one more state variable.
+We need to evaluate every disjunct to ensure we find all possible next states, which is why TLA⁺ disjunction does not short-circuit.
+Modify the ''OR'' handling code in ''visitVariadicExpr()'' as highlighted:
+<code java [highlight_lines_extra="3,5,8"]>
+      case OR:
+        boolean result = false;
+        Map<String, Object> trunk = next;
+        for (Expr disjunct : expr.parameters) {
+          next = new HashMap<>(trunk);
+          Object junctResult = evaluate(disjunct);
+          checkBooleanOperand(expr.operator, junctResult);
+          possibleNext.add(new HashMap<>(next));
+          result |= (boolean)junctResult;
+        }
+        return result;
+      default:
+</code>
+There are two other operators to support for binding state variables: the set membership ''\in'' operator, and the ''\E'' existential quantification operator.
+Actions like ''x' \in {0, 1}'' or ''\E v \in {0, 1} : x' = v'' are equivalent to ''x' = 0 \/ x' = 1''.
+Add the following code to the ''IN'' case in ''visitBinaryExpr()'':
+<code java [highlight_lines_extra="3,4,5,6,7,8,9,10,11,12"]>
+      case IN:
+        checkSetOperand(expr.operator, right);
+        if (left instanceof UnboundVariable var) {
+          Map<String, Object> trunk = next;
+          for (Object element : (Set<?>)right) {
+            next = new HashMap<>(trunk);
+            next.put(var.name().lexeme, element);
+            left = element;
+            possibleNext.add(new HashMap<>(next));
+          }
+          return true;
+        }
+        return ((Set<?>)right).contains(left);
+</code>
+Then update the ''EXISTS'' case of ''visitQuantFnExpr()'' as highlighted:
+<code java [highlight_lines_extra="3,5,8"]>
+      } case EXISTS: {
+        boolean result = false;
+        State current = state;
+        Map<String, Object> trunk = next;
+        for (Environment binding : bindings) {
+          next = new HashMap<>(trunk);
+          Object junctResult = executeBlock(expr.body, binding);
+          checkBooleanOperand(expr.op, junctResult);
+          possibleNext.add(new HashMap<>(next));
+          result |= (boolean)junctResult;
+        }
+        return result;
+</code>
+We can now generate all nondeterministic next states by calling ''getNextStates()'' with an appropriate action!
+===== The ENABLED Operator =====
+Now that we've written ''getNextStates()'', we can fully define the ''ENABLED'' prefix operator!
+An expression ''ENABLED Action'' evaluates to ''true'' if ''Action'' produces at least one possible next state.
+So, as simple as a quick call to ''getNextStates()'' to see whether it returns an empty list or not!
+Well, not quite - the ''ENABLED'' operator can possibly be evaluated //inside// an action, so inside a call to ''getNextStates()''!
+This means we need some extra ceremony to stash the current values of ''next'' and ''possibleNext'', then restore them using the standard ''try''/''finally'' block method.
+Add the highlighted code to the ''ENABLED'' case in ''visitUnaryExpr()'':
+<code java [highlight_lines_extra="2,3,4,5,6,7,8,9,10"]>
+      } case ENABLED: {
+        Map<String, Object> oldNext = next;
+        Set<Map<String,Object>> oldPossibleNext = possibleNext;
+        try {
+          clearNext();
+          return !getNextStates(expr.operator, expr.expr).isEmpty();
+        } finally {
+          next = oldNext;
+          possibleNext = oldPossibleNext;
+        }
+      } case NOT: {
+</code>
+This is a big milestone: we now have fully defined //everything// in our minimal TLA⁺ language subset!
+We aren't at the end yet, but it's well within sight.
+===== Error Checking =====
+Our code is nice & simple, but unfortunately it has more holes than Swiss cheese.
+Let's add some error checks!
+Null value types like ''UnboundVariable'' produce a major annoyance: we now need to sprinkle null checks throughout our evaluation code!
+Thankfully many null checks are already handled by our existing stable of ''check-Operand()'' helpers, but some cases still remain.
+Near the bottom of the ''Interpreter'' class, create a new helper method ''checkIsValue()'':
+<code java>
+  private void checkIsValue(Object... operands) {
+    for (Object operand : operands) {
+      if (operand instanceof UnboundVariable var) {
+        throw new RuntimeError(var.name(), "Use of unbound variable.");
+      }
+    }
+  }
+</code>
+In our ''EQUALS'' handling logic, we can only bind the value of ''right'' to a variable if ''right'' has a defined concrete value.
+Also, two values can only be compared for equality if they are both defined:
+<code java [highlight_lines_extra="3,7"]>
+      case EQUAL:
+        if (left instanceof UnboundVariable var) {
+          checkIsValue(right);
+          next.put(var.name().lexeme, right);
+          return true;
+        }
+        checkIsValue(left, right);
+        return left.equals(right);
+</code>
+A null check must also must be added to the ''LEFT_BRACE'' case in ''visitVariadicExpr()'':
+<code java [highlight_lines_extra="5"]>
+      case LEFT_BRACE:
+        Set<Object> set = new HashSet<Object>();
+        for (Expr parameter : expr.parameters) {
+          Object value = evaluate(parameter);
+          checkIsValue(value);
+          set.add(value);
+        }
+</code>
+The ''ALL_MAP_TO'' case in ''visitQuantFnExpr()'':
+<code java [highlight_lines_extra="6"]>
+      case ALL_MAP_TO: {
+        Token param = expr.params.get(0);
+        Map<Object, Object> function = new HashMap<>();
+        for (Environment binding : bindings) {
+          Object value = executeBlock(expr.body, binding);
+          checkIsValue(value);
+          function.put(binding.get(param), value);
+        }
+        return function;
+</code>
+And also the ''visitFnApplyExpr()'' method:
+<code java [highlight_lines_extra="5"]>
+  public Object visitFnApplyExpr(Expr.FnApply expr) {
+    Object callee = evaluate(expr.fn);
+    checkFunctionOperand(expr.bracket, callee);
+    Object argument = evaluate(expr.argument);
+    checkIsValue(argument);
+    Map<?, ?> function = (Map<?, ?>)callee;
+</code>
+===== Hooking Up the Interpreter =====
+It takes a bit of thought to consider how we should expose our new state-stepping capabilities through the REPL.
+One decent approach is to hijack ''Stmt.Print'' statements to trigger steps if they happen to define possible next states.
+For this, add the following code to the bottom of the ''run()'' method in the ''TlaPlus'' class:
+<code java [highlight_lines_extra="4,5,6,7,8,9"]>
+    // Stop if there was a syntax error.
+    if (hadError) return;
+    if (replMode && statements.size() == 1
+        && statements.get(0) instanceof Stmt.Print action) {
+      tryStep(action);
+    } else {
+      interpreter.interpret(statements);
+    }
+  }
+</code>
+This calls a method we'll define in ''TlaPlus'' called ''tryStep()''.
+The ''tryStep()'' method should first speculatively execute ''action'' to see what sort of value it returns; if it doesn't return a ''Boolean'', treat it as an ordinary ''Stmt.Print'' statement.
+However, if ''action'' //does// return a ''Boolean'', it might be a valid action leading to new states, so call ''getNextStates()''.
+If this generates no new states, again treat ''action'' as an ordinary ''Stmt.Print'' statement:
+<code java>
+  private static void tryStep(Stmt.Print action) {
+    Object result = interpreter.executeBlock(action.expression, interpreter.globals);
+    if (!(result instanceof Boolean)) {
+      action.accept(interpreter);
+      return;
+    }
+    List<Map<String, Object>> nextStates =
+      interpreter.getNextStates(action.location, action.expression);
+    if (nextStates.isEmpty()) {
+      action.accept(interpreter);
+      return;
+    }
+  }
+</code>
+The ''java.util.Map'' class must be imported at the top of the file:
+<code java [highlight_lines_extra="2"]>
+import java.util.List;
+import java.util.Map;
+public class TlaPlus {
+</code>
+At this point all that remains is to handle the case of what happens when the ''Stmt.Print'' statement //does// generate possible next states.
+The REPL should choose one next state and make ''interpreter'' step to it; add this to the bottom of ''tryStep()'':
+<code java [highlight_lines_extra="8,9,10,11,12"]>
+    List<Map<String, Object>> nextStates =
+      interpreter.getNextStates(action.location, action.expression);
+    if (nextStates.isEmpty()) {
+      System.out.println(false);
+      return;
+    }
+    Map<String, Object> nextState = pickNext(nextStates);
+    interpreter.goToState(nextState);
+    System.out.println(true);
+    System.out.println(nextState);
+  }
+</code>
+We also print out ''true'' - the value ''Stmt.Print'' would have printed - and display the value of the next state for the user.
+This called two methods; one, ''goToState()'' in ''Interpreter'', sets the ''current'' state to the one given:
+<code java>
+  void goToState(Map<String, Object> state) {
+    current = state;
+    primed = state == null;
+    clearNext();
+  }
+</code>
+The other, in ''TlaPlus'', picks the next state to step to.
+If there are multiple possible next states, the user is prompted to choose one:
+<code java>
+  private static Map<String, Object> pickNext(List<Map<String, Object>> nextStates) {
+    if (nextStates.size() == 1) {
+      return nextStates.get(0);
+    } else {
+      System.out.println("Select next state (enter number): ");
+      for (int i = 0; i < nextStates.size(); i++) {
+        System.out.println(i + ": " + nextStates.get(i));
+      }
+      System.out.print("> ");
+      try (java.util.Scanner in = new java.util.Scanner(System.in)) {
+        return nextStates.get(in.nextInt());
+      }
+    }
+  }
+</code>
+And that's it!
+You can now run the REPL and step through the state space!
+Try entering expressions like the following:
+  - ''VARIABLE x''
+  - ''x = 0''
+  - ''x' \in 0 .. 5''
+This was a pivotal chapter; excellent work making it to the end.
+You can find the expected state of the codebase in [[https://github.com/tlaplus/devkit/tree/main/8-actions|this repository]].
+Now we can put it all together and build a real model checker in [[creating:safety|the next chapter]]!
-Now that we can declare variables, what value are they initialized to?
+[[creating:operators|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:safety|Next Page >]]
-We've successfully dodged this issue for a very long time, but unfortunately the initial value of these variables is undefined.
-That means we will need a null value type.
-We've avoided null types thus far, which means we haven't had to do as many checks before using values in the interpreter - a real luxury!
-Alas we now depart this wonderful land.