Where do we go from here?

The goal of the next chapters is to operationalize our understanding of OCaml functions by tracing their calls and returns, i.e., to visualize them with

• the name of the function being called, its arguments, and ->, and
• the name of the function returning a result, its arguments, <-, and the result.

This way we can build a mental picture of the operations being carried out in a certain order, and that is useful when the functions being called are recursive, i.e., call themselves.

For example, an arithmetic expression, which is constructed inductively as an abstract-syntax tree (i.e., with a base case (an integer is an arithmetic expression) and with an induction step (given two arithmetic expressions, here is a new arithmetic expression to add them)) is evaluated recursively as the evaluator traverses this tree:

• to evaluate e1 + e2 in an environment, we first evaluate e1 in this environment (which gives the result n1, assuming this evaluation terminates and doesn’t raise an error);
• then we evaluate e2 in this environment (which gives the result n2, assuming this evaluation terminates and doesn’t raise an error); and
• then we add n1 and n2, which gives the result n3, which is the result of evaluating e1 + e2.

See how evaluation is recursive, i.e., defined in terms of itself as it traverses the abstract-syntax tree?

Tracing the evaluation function:

eval "e1 + e2" ->
  eval "e1" ->
  ...
  eval "e1" <- n1
  eval "e2" ->
  ...
  eval "e2" <- n2
eval "e1 + e2" <- n3

Here is a concrete example, "0 + (1 + 10) + (100 + 1000) + 10000", or, making OCaml’s left associativity explicit, "((0 + (1 + 10)) + (100 + 1000)) + 10000". This arithmetic expression was constructed inductively then and it is evaluated recursively now:

eval "(((0 + (1 + 10)) + (100 + 1000)) + 10000)" ->
  eval "((0 + (1 + 10)) + (100 + 1000))" ->
    eval "(0 + (1 + 10))" ->
      eval "0" ->
      eval "0" <- 0
      eval "(1 + 10)" ->
        eval "1" ->
        eval "1" <- 1
        eval "10" ->
        eval "10" <- 10
      eval "(1 + 10)" <- 11
    eval "(0 + (1 + 10))" <- 11
    eval "(100 + 1000)" ->
      eval "100" ->
      eval "100" <- 100
      eval "1000" ->
      eval "1000" <- 1000
    eval "(100 + 1000)" <- 1100
  eval "((0 + (1 + 10)) + (100 + 1000))" <- 1111
  eval "10000" ->
  eval "10000" <- 10000
eval "(((0 + (1 + 10)) + (100 + 1000)) + 10000)" <- 11111

The next chapters describe how to make OCaml functions emit such traces as they are called and as they return, to visualize their computation.

Food for thought

All the syntactic constructs of OCaml introduced so far were introduced with a similar recursive description of how they are evaluated:

• evaluating an integer in an environment yields this integer;

• evaluating a Boolean in an environment yields this Boolean;

• evaluating a character in an environment yields this character;

• evaluating a string in an environment yields this string;

• to evaluate a name in an environment, we look it up in this environment;

• to evaluate if e1 then e2 else e3 in an environment, we first evaluate e1 in this environment;
  • if evaluating e1 does not terminate, then evaluating if e1 then e2 else e3 does not terminate either;
  • if evaluating e1 raises an error, then evaluating if e1 then e2 else e3 also raises this error;
  • if evaluating e1 yields a Boolean, then
    • if this Boolean is true, then evaluating if e1 then e2 else e3 in an environment reduces to evaluating e2 in this environment, and
    • if this Boolean is false, then evaluating if e1 then e2 else e3 in an environment reduces to evaluating e3 in this environment;

• to evaluate (e1, e2) in an environment, we first evaluate e1 and e2 in this environment:
  • if either of these first evaluations does not terminate, then evaluating (e1, e2) does not terminate either;
  • if either of these first evaluations raises an error, then evaluating (e1, e2) also raises this error;
  • if e1 and e2 evaluate to v1 and v2, then evaluating (e1, e2) yields a pair that holds v1 and v2;

• to evaluate (e1, ..., eN) in an environment, we first evaluate e1, ..., and eN in this environment:
  • if either of these first evaluations does not terminate, then evaluating (e1, ..., eN) does not terminate either;
  • if either of these first evaluations raises an error, then evaluating (e1, ..., eN) also raises this error;
  • if e1, ..., and eN respectively evaluate to v1, ... and vN, then evaluating (e1, ..., eN) yields a tuple that holds v1, and vN;

• evaluating () yields ();

• evaluating fun x1 -> e2 in an environment yields a function;

• to evaluate e0 e1 in an environment, we first evaluate e0 and e1 in this environment:
  • if either of these first evaluations does not terminate, then evaluating e0 e1 does not terminate;
  • if either of these first evaluations raises an error, then evaluating e0 e1 also raises this error; and
  • if e0 and e1 evaluate to v0 and v1, then since OCaml is statically typed, v0 denotes a function; evaluating e0 e1 reduces to applying this function to v1;
    • if this function resulted from evaluating fun x1 -> e2 in an environment, applying it to v1 reduces to evaluating e2 in an extension of this environment where x1 denotes v1; the binding of x1 is local: it vanishes once e2 is evaluated;
    • if this function resulted from evaluating, e.g., fun (x3, x4) -> e2 in an environment, i.e., a function abstraction where the formal parameter is compound, then for typing reasons v1 must be a pair; writing this pair as (v3, v4), applying this function to (v3, v4) reduces to evaluating e2 in an extension of this environment where x3 denotes v3 and x4 denotes v4; the bindings of x3 and x4 are local: they vanish once e2 is evaluated;
    • if this function was predefined, applying it to v1 triggers its computation:
      • if this computation does not terminate, then evaluating e0 e1 does not terminate either;
      • if this computation raises an error (e.g., a division by 0), then evaluating e0 e1 also raises this error; and
      • if this computation yields a value, then evaluating e0 e1 also yields this value;

• to evaluate let x1 = e1 in e2 in an environment, we first evaluate the definiens, i.e., e1 in this environment:
  • if this first evaluation does not terminate, then evaluating let x1 = e1 in e2 does not terminate;
  • if this first evaluation raises an error, then evaluating let x1 = e1 in e2 also raises this error;
  • if e1 evaluates to v1, then evaluating let x1 = e1 in e2 in an environment reduces to evaluating e2 in an extension of this environment where x1 denotes v1; the binding of x1 is local: it vanishes once e2 is evaluated;

• likewise, to evaluate, e.g., let (x1, x2) = e12 in e0 in an environment, i.e., a let-expression where the formal parameter is compound, we first evaluate the definiens, i.e., e12 in this environment:
  • if this first evaluation does not terminate, then evaluating let (x1, x2) = e12 in e0 does not terminate;
  • if this first evaluation raises an error, then evaluating let (x1, x2) = e12 in e0 also raises this error;
  • if e12 evaluates to (v1, v2) (which it must, for typing reasons), then evaluating let (x1, x2) = e12 in e0 in an environment reduces to evaluating e0 in an extension of this environment where x1 denotes v1 and x2 denotes v2; the bindings of x1 and x2 are local: they vanish once e0 is evaluated;

• to evaluate let x1 = e1 and ... xN = eN in e0 in an environment, we first evaluate the definienses, i.e., e1, ..., and eN in this environment:
  • if either of these first evaluations does not terminate, then evaluating let x1 = e1 and ... xN = eN in e0 does not terminate;
  • if either of these first evaluations raises an error, then evaluating let x1 = e1 and ... xN = eN in e0 also raises this error;
  • if e1, ..., and eN respectively evaluate to v1, ... and vN, then evaluating let x1 = e1 and ... xN = eN in e0 in an environment reduces to evaluating e0 in an extension of this environment where x1 denotes v1, ..., and xN denotes vN; the bindings of x1, ..., and xN are local: they vanish once e0 is evaluated;

More food for thought

The lecture notes for this week introduce how to declare recursive functions. To make the present chapter self-contained, here is the recursive description of how these declarations are evaluated, and how recursive functions are applied:

• to evaluate let rec f = fun x1 -> e2 in e0 in an environment,
  • we first evaluate the definiens, i.e., fun x1 -> e2, in an extension of this environment where f denotes the result of evaluating fun x1 -> e2 in this extended environment; it is this self-reference that enables the recursive definition of f;
  • evaluating let rec f = fun x1 -> e2 in e0 in an environment then reduces to evaluating e0 in this extended environment; the binding of f is local: it vanishes once e0 is evaluated;

• to evaluate let rec f1 = fun x1 -> e1 and ... and fN = fun xN -> eN in e0 in an environment,
  • we first evaluate the definienses, i.e., fun x1 -> e1, ..., and fun xN -> eN, in an extension of this environment where f1 denotes the result of evaluating fun x1 -> e1, ..., and fN denotes the result of evaluating fun xN -> eN in this extended environment; it is this self-reference that enables the recursive definitions of f1, ..., and fN;
  • evaluating let rec f1 = fun x1 -> e1 and ... and fN = fun xN -> eN in e0 in an environment then reduces to evaluating e0 in this extended environment; the binding of f1, ..., and fN are local: they vanish once e0 is evaluated.

Version

Updated [02 Feb 2023]

Created [09 Sep 2022]