G02: Language semantics, scope, and type safety

Prerequisites and observable goals#

The central question: what does an expression mean?#

A string of characters is syntax. A parsed tree identifies structure. A semantics specifies what that structure does. A type system rejects selected structural mistakes before evaluation. These are separate layers: a parser can accept True+2 syntactically even when the language’s type rules reject it.

We use a deliberately small, pure expression language. Its values are mathematical integers and Booleans. Its constructs are addition, multiplication, integer comparison, conditional expressions, variables, and a local binding. There are no loops, recursion, mutable references, division, I/O, or host-language calls. These restrictions make some proofs and optimizations possible that would be wrong in a larger language.

The symbol $::=$ defines grammatical alternatives; the vertical bars mean “or.” A grammar is not yet an execution rule. Parentheses or the abstract syntax tree remove ambiguity about grouping.

Environments turn names into values#

An environment $\rho$ maps variable names to values. The judgment $\rho\vdash e\Downarrow v$ reads “under environment $\rho$, expression $e$ evaluates to value $v$.” This is a big-step description: it relates a whole expression to its result.

For a variable, evaluate by lookup: $\rho\vdash x\Downarrow\rho(x)$ when $x$ is bound. For addition, evaluate each operand under the same environment, obtain integers $a,b$, and return $a+b$. For a conditional, first evaluate its condition to a Boolean, then evaluate only the selected branch. For a binding, evaluate its right side in the outer environment, create an environment extended by the new name, and evaluate the body there:

A rule has premises above the line and a conclusion below it. It is a logical inference, not division. The updated environment shadows an older binding in that scope without mutating its caller’s environment.

Worked trace with shadowing#

Evaluate $\mathsf{let}\ x=2\ \mathsf{in}\ (\mathsf{let}\ x=x+1\ \mathsf{in}\ x)+x$. The outer right side is 2, producing $\rho_1=\{x\mapsto2\}$. The inner right side $x+1$ is evaluated in $\rho_1$, so it is 3. The inner body uses $\rho_2=\rho_1[x\mapsto3]$ and returns 3. The right operand of the outer addition still uses $\rho_1$ and returns 2. The answer is 5.

The figure is a scope diagram, not a required memory layout. An implementation can use parent-linked environments, a stack of frames, or compiled local slots. Correctness requires the same lookup behavior, not the same physical diagram.

Typing judgments and rules#

A type environment $\Gamma$ maps names to types rather than values. Write $\Gamma\vdash e:\tau$ for “$e$ has type $\tau$ under $\Gamma$.” Here $\tau$ is either $\mathsf{Int}$ or $\mathsf{Bool}$. The addition rule is

Comparison has the same operand requirements but returns $\mathsf{Bool}$. A conditional requires a Boolean condition and the same type in both branches. A local binding infers the right-side type under the outer environment and extends the type environment for the body.

Both branches are checked even though only one is evaluated. Thus $\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ 7\ \mathsf{else}\ \mathsf{false}$ is rejected by this type system. Another language could admit union types, but adding them would require new typing and runtime rules. Do not assume our simplification is a universal language law.

Python itself permits some operations between Booleans and integers. Our language intentionally does not. The reference uses exact runtime type comparisons so a Boolean literal is not accidentally classified as an integer. An interpreter written in a host language must implement the guest language’s rules rather than silently inheriting every host behavior.

Why type checking helps, and what it cannot prove#

A small-step relation $e\to e'$ describes one evaluation step. Two central proof ideas are progress and preservation. Progress says a well-typed closed expression is a value or has an allowed next step. Preservation says an allowed step of a well-typed expression preserves its type. Together they exclude a particular kind of stuck state, such as trying to add a Boolean and an integer. Their precise forms depend on the language and evaluation rules. [G-TYPES]

For addition, progress follows by cases: if the left operand can step, step it; if it is an integer value and the right can step, step the right; if both are integer values, add them. The typing rule excludes a Boolean operand. For a variable, closedness matters: an unbound name has no value lookup. For let, the corresponding substitution or environment-consistency lemma connects a value of the inferred type to its binding in the body.

An approachable big-step argument fits our implementation directly. Assume every name’s runtime value has the type recorded in $\Gamma$. Prove by structural induction on $e$ that successful evaluation of a well-typed expression produces a value of its inferred type. Literals and variables follow immediately. Arithmetic/comparison use the induction hypothesis for operands. For a conditional, its condition is Boolean and the selected branch has the common branch type. For let, the right side has its inferred type, so extending both environments consistently lets the induction hypothesis apply to the body.

Our finite AST and absence of recursive calls also yield termination in the ideal unbounded-resource model: evaluation descends into proper subtrees. This is not a consequence of type safety alone. A typed language can have nonterminating recursion. Nor does type safety prove that an integer expression computes the business quantity you intended, that a model’s prediction is fair, or that physical memory cannot be exhausted.

Method selection and debugging#

When a program is rejected, ask which layer rejects it. A missing parenthesis is parsing. An unknown name is binding/scope. Boolean addition is typing. A wrong but well-typed arithmetic formula is a specification or implementation error. Reproducing the failure at the smallest AST separates these categories.

For example, an interpreter that mutates scope[name] in place may return the right answer for non-shadowing examples yet fail nested binding. A checker that only inspects the selected constant branch may hide an invalid unchosen branch, changing the language’s acceptance rules. A checker that uses isinstance(True,int) inherits a host quirk. Each bug needs a test drawn from the appropriate rule, not only more random arithmetic inputs.

Independent practice#

F foundation C standard course work T transfer S optional stretch L runnable lab or project. Attempt the complete set before opening its solutions.

Smallest useful hints#

For .04, evaluate the right side before extending the environment. For .05, distinguish “same returned value” from “same observable behavior.” For .06, write separate environments for types and values; infer before executing the selected branch.

Complete solutions: G02#

Compare the first step where your work differs. A corrected answer is not yet an independent success.

Open every solution

"""G02: typed, pure, finite expressions. No eval or host-language calls.
AST: int, bool, variable str, ('+',a,b), ('*',a,b), ('<',a,b),
('if',condition,then,otherwise), ('let',name,value,body).
"""


def infer(expr, env=None, depth=0):
    env = {} if env is None else env
    if depth > 48:
        raise ValueError("expression depth exceeds 48")
    if type(expr) is bool:
        return "bool"
    if type(expr) is int:
        return "int"
    if type(expr) is str:
        if expr not in env:
            raise ValueError("unbound name: " + expr)
        return env[expr]
    if type(expr) is not tuple or not expr:
        raise ValueError("malformed expression")
    tag = expr[0]
    if tag in ("+", "*", "<") and len(expr) == 3:
        if any(infer(x, env, depth + 1) != "int" for x in expr[1:]):
            raise TypeError("arithmetic/comparison requires integers")
        return "bool" if tag == "<" else "int"
    if tag == "if" and len(expr) == 4:
        if infer(expr[1], env, depth + 1) != "bool":
            raise TypeError("condition must be Boolean")
        left = infer(expr[2], env, depth + 1)
        right = infer(expr[3], env, depth + 1)
        if left != right:
            raise TypeError("branches must have identical types")
        return left
    if tag == "let" and len(expr) == 4 and type(expr[1]) is str:
        typ = infer(expr[2], env, depth + 1)
        child = dict(env)
        child[expr[1]] = typ
        return infer(expr[3], child, depth + 1)
    raise ValueError("unknown node or wrong arity")


def evaluate(expr, env=None):
    values = {} if env is None else dict(env)
    if any(type(x) not in (int, bool) for x in values.values()):
        raise TypeError("environment values must be integers or Booleans")
    infer(expr, {k: "bool" if type(v) is bool else "int"
                 for k, v in values.items()})

    def go(e, scope):
        if type(e) in (int, bool):
            return e
        if type(e) is str:
            return scope[e]
        tag = e[0]
        if tag == "let":
            value = go(e[2], scope)  # value uses the outer scope
            return go(e[3], {**scope, e[1]: value})
        if tag == "if":
            return go(e[2] if go(e[1], scope) else e[3], scope)
        a, b = go(e[1], scope), go(e[2], scope)
        if tag == "+":
            return a + b
        if tag == "*":
            return a * b
        return a < b

    return go(expr, values)


if __name__ == "__main__":
    e = ("let", "x", 3, ("if", ("<", "x", 4), ("*", "x", 2), 0))
    print(infer(e), evaluate(e))

Retention and continuation#

From memory, distinguish a string, an AST, a type, an environment, and a value. Demonstrate a scope bug with a minimal shadowing program. You are ready for GP1 after you can explain how a conditional may have one runtime branch but two checked branches. Continue by adding functions and closures with an explicit environment-capture rule; that is an unassigned extension requiring new type and evaluation tests, not a capability claimed for this reference. [G-TYPES]