ALUX Programming Guidelines

How to Read This Book

This book blends theory and practice. You will see each concept from two perspectives:

• Concepts — core ideas expressed clearly and precisely, independent of language or framework.
• Insights — deeper connections between concepts, with examples, design patterns, and transformations.

The examples are often in Rust but the principles are language-agnostic.

Who This Book Is For

• Programmers who want to design for meaning rather than just mechanics.
• Developers seeking to connect category theory, type systems, and program design.
• Readers curious about how ideas like Free Monads, CPS, Defunctionalization, and Dependent Types fit together.

Operational Semantics

Definition

Operational semantics defines the meaning of programs by specifying how they execute step by step. It models program execution as transitions between configurations - abstract states containing program fragments, environments, or memory.

Styles of Operational Semantics

Small-step (Structural Operational Semantics)

Computation is broken into atomic transitions:

(2 + 3) → 5
(2 + 3) * 4 → 5 * 4 → 20

Useful for modeling concurrency, interleaving, and partial execution.

Big-step (Natural Semantics)

Describes evaluation in terms of final results:

(2 + 3) * 4 ⇓ 20

Often clearer for reasoning about terminating programs.

Formal Rules

Operational semantics is typically given with inference rules.
For a simple arithmetic language:

Expr ::= n | Expr + Expr

We can write:

n1 + n2 → n3      (where n3 = n1 + n2)

Evaluation trace:

(1 + 2) + 3 → 3 + 3 → 6

Why It Matters

• Provides a precise machine-like model of execution.
• Foundation for interpreters and virtual machines.
• Supports reasoning about correctness, resource use, and safety.

Relation to Other Concepts

• Free Monad: Encodes operational rules as an AST of instructions.
• CPS: Makes control flow explicit by turning "rest of the program" into a continuation.
• Defunctionalization: Turns continuations into explicit state transitions, directly resembling operational semantics.
• Dependent Types: Can enrich operational rules with proofs (e.g., stack safety, gas bounds).

In Practice

Operational semantics is how interpreters are built:

• The EVM can be viewed as a large-step state transition system.
• Small-step rules directly resemble match arms in a Rust interpreter.

(n1 + n2) → n3

can be read as Rust code:

#![allow(unused)]
fn main() {
match expr {
    Add(Box::new(Num(n1)), Box::new(Num(n2))) => Num(n1 + n2),
    _ => expr,
}
}

To think about

Thinking about programming in operational ways or using an imperative style—even with a proof—does not enable us to gain deep insights

Operational thinking (implementation first) prevent us to express and improve ideas

Expression Problem

Phil Wadler’s expression problem is about simultaneously extending a language in two dimensions without modifying existing code:

• Add new data variants (new expression forms, aka “syntax”).
• Add new operations (new interpretations, aka “semantics”).

The core tension:

• In functional/ADT style, adding new operations is easy, but adding new variants is invasive.
• In object-oriented style, adding new variants is easy, but adding new operations is invasive.

This section shows both sides with small Haskell and Java examples.

Haskell (Functional / ADT)

We start with a classic ADT for expressions and two operations.

data Expr
  = Lit Int
  | Add Expr Expr
  | Mul Expr Expr  -- ✏️ UPDATE: new variant forces edits below

eval :: Expr -> Int
eval (Lit n)     = n
eval (Add a b)   = eval a + eval b

pretty :: Expr -> String
pretty (Lit n)   = show n
pretty (Add a b) = "(" ++ pretty a ++ " + " ++ pretty b ++ ")"

Now adding a new operation is easy:

size :: Expr -> Int
size (Lit _)   = 1
size (Add a b) = 1 + size a + size b

But adding a new variant (e.g. Mul) forces edits in every function:

data Expr
  = Lit Int
  | Add Expr Expr
  | Mul Expr Expr

eval :: Expr -> Int
eval (Lit n)     = n
eval (Add a b)   = eval a + eval b
eval (Mul a b)   = eval a * eval b  -- ✏️ UPDATE: new case

pretty :: Expr -> String
pretty (Lit n)   = show n
pretty (Add a b) = "(" ++ pretty a ++ " + " ++ pretty b ++ ")"
pretty (Mul a b) = "(" ++ pretty a ++ " * " ++ pretty b ++ ")"  -- ✏️ UPDATE: new case

size :: Expr -> Int
size (Lit _)   = 1
size (Add a b) = 1 + size a + size b
size (Mul a b) = 1 + size a + size b  -- ✏️ UPDATE: new case

In Wadler’s terms, data extension is not modular in the ADT approach.

Java (Object-Oriented)

We start with an interface and concrete classes for each variant.

// Expression variants
interface Expr {
    int eval();
    String pretty();
}

final class Lit implements Expr {
    private final int n;

    Lit(int n) {
        this.n = n;
    }

    public int eval() {
        return n;
    }

    public String pretty() {
        return Integer.toString(n);
    }
}

final class Add implements Expr {
    private final Expr a;
    private final Expr b;

    Add(Expr a, Expr b) {
        this.a = a;
        this.b = b;
    }

    public int eval() {
        return a.eval() + b.eval();
    }

    public String pretty() {
        return "(" + a.pretty() + " + " + b.pretty() + ")";
    }
}

Now adding a new variant is easy:

final class Mul implements Expr {
    private final Expr a;
    private final Expr b;

    Mul(Expr a, Expr b) {
        this.a = a;
        this.b = b;
    }

    public int eval() {
        return a.eval() * b.eval();
    }

    public String pretty() {
        return "(" + a.pretty() + " * " + b.pretty() + ")";
    }
}

But adding a new operation (e.g. size) is invasive. You must edit the interface and every class:

interface Expr {
    int eval();
    String pretty();
    int size(); // ✏️ UPDATE: new operation added here
}

final class Lit implements Expr {
    private final int n;

    Lit(int n) { this.n = n; }

    public int eval() { return n; }
    public String pretty() { return Integer.toString(n); }
    public int size() { return 1; } // ✏️ UPDATE: new method in every class
}

final class Add implements Expr {
    private final Expr a;
    private final Expr b;

    Add(Expr a, Expr b) { this.a = a; this.b = b; }

    public int eval() { return a.eval() + b.eval(); }
    public String pretty() { return "(" + a.pretty() + " + " + b.pretty() + ")"; }
    public int size() { return 1 + a.size() + b.size(); } // ✏️ UPDATE: new method in every class
}

final class Mul implements Expr {
    private final Expr a;
    private final Expr b;

    Mul(Expr a, Expr b) { this.a = a; this.b = b; }

    public int eval() { return a.eval() * b.eval(); }
    public String pretty() { return "(" + a.pretty() + " * " + b.pretty() + ")"; }
    public int size() { return 1 + a.size() + b.size(); } // ✏️ UPDATE: new method in every class
}

In Wadler’s terms, operation extension is not modular in the OO approach.

Summary (Wadler’s Point)

• Functional/ADT style favors new operations but resists new variants.
• OO style favors new variants but resists new operations.
• The expression problem asks for a design where both dimensions are extensible without modifying existing code.

Wadler’s Explanation and Solution Landscape (1998)

Wadler frames the problem as: extend a datatype by cases (new variants) and extend functions over that datatype (new operations), without recompiling existing code and while preserving static type safety (no casts).

He uses a “table” metaphor:

• Rows = cases (variants / constructors)
• Columns = functions (operations / interpretations)

In functional/ADT settings, rows are fixed and columns are easy to add.
In OO settings, columns are fixed and rows are easy to add.
The challenge is to make both directions extensible.

Wadler’s Proposed Solution (GJ + Virtual Types)

Wadler presents a solution in GJ (Generic Java) using:

• A This-bounded parameter (This extends LangF<This>) to simulate ThisType.
• Inner classes and interfaces indexed by This (virtual types).
• A visitor-based structure that allows:
  • New cases (e.g., Plus) by subclassing the “language family”
  • New operations (e.g., Show) by adding new visitors

The trick is to refer to This.Exp and This.Visitor so that each extension phase remains type-safe and independently compilable.

Caveat (Java inner interfaces)

Wadler notes that Java treats inner interfaces as static, which breaks the indexing trick.
He suggests that loosening this restriction would make the solution viable; this has still not changed in modern Java (nested interfaces remain implicitly static).

Other Solution Directions Mentioned

1. Corky Cartwright’s approach Requires contravariant extension: allow a base expression type to stand in for an extended one. This explains why fixpoints are used: the extended language family is not a subtype of the original.

2. Kim Bruce’s approach Requires higher‑order type constructors (parameterizing a type over a type constructor). GJ does not support this directly, but Wadler argues virtual types can simulate it.

3. Krishnamurthi et al. (Extended Visitor pattern) Works via an extended visitor design. Not statically typed in their setting (Pizza), so dynamic casts are required.

4. Special‑purpose language extensions Wadler cites two solutions that rely on language features designed specifically for the problem. These are less general than the virtual‑type approach.

Wadler’s Two Points

Wadler’s email makes two points clear:

1. The Expression Problem is a structural tension between data extension and operation extension.
2. Solutions are possible, but they tend to require either:
   • Type system features that simulate virtual types, or
   • Special-purpose language extensions, or
   • A compromise on static type safety or independent compilation.

References

• Wadler, P. (1998). The Expression Problem. Java-Genericity mailing list note.
  https://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt

Referential Transparency

Referential transparency (RT) is the substitution property of expressions: an expression can be replaced by its denotation without changing program meaning.

Today, this is how RT is used in practice: as the basis for equational reasoning, safe refactoring, and law-driven API design.

Core Meaning

RT says:

• if e denotes v
• then using v instead of e preserves meaning

This is a semantic claim, not a coding-style slogan.

Purity

A pure function returns the same output for the same inputs and has no observable side effects. RT is the substitution law for expressions: replacing an expression with its denotation must preserve meaning. So purity is one common way to obtain RT in practice, while RT is the broader semantic criterion. See Referential Transparency Reloaded for the DD purity-vs-RT distinction.

Historical Context

In programming-language semantics, RT is strongly associated with Christopher Strachey's framing. His treatment separates value reasoning from update-heavy behavior:

• R-values: expression values.
• L-values: locations that can be assigned.

The key point is that expression-level substitution is stable when we stay in value reasoning. Assignment introduces updates to locations and makes substitution reasoning harder or invalid in the naive form.

What Assignment And Side Effects Mean Here

In this context:

• assignment is updating a location (for example, x := x + 1)
• side effect is any observable change beyond returning a value

Assignment is a specific kind of side effect.

This is why RT fails in many imperative settings: evaluation can depend on or mutate observable context outside the expression's explicit value interface.

How Modern Languages Present RT

Haskell

RT is taught as default reasoning for pure expressions. Effects are explicit in typed constructions (IO, state threading, and related abstractions), so substitution laws are central in daily use.

Scala (Cats / Cats Effect)

In Scala FP practice, Cats Effect gives the most common RT framing:

• IO[A] is a pure description of effectful work
• composition of IO values is RT
• execution is explicit at runtime boundaries (unsafeRun*)

Cats Effect also contrasts this with eager Future evaluation, which is one reason RT discussions in Scala emphasize laziness and delayed execution.

RT Today

Across modern ecosystems, RT is used as shorthand for substitution-safe behavior. In mixed-paradigm systems, teams usually apply RT claims to specific modules, APIs, or effect-typed regions rather than to all code globally.

For the Denotational Design interpretation of RT, see Referential Transparency Reloaded.

References

• Strachey, C. Fundamental Concepts in Programming Languages (Oxford PRG lecture notes, 1967).
  https://reed.cs.depaul.edu/jriely/447/assets/articles/strachey-fundamental-concepts-in-programming-languages.pdf
• Cats Effect docs: IO data type and RT/lazy evaluation notes.
  https://typelevel.org/cats-effect/docs/datatypes/io
• Typelevel blog: An IO monad for cats (Scala impurity vs RT motivation).
  https://typelevel.org/blog/2017/05/02/io-monad-for-cats.html

Free Monad

What is a Free Monad (Rust version)

A free monad lets you:

• Describe a program as data - not by running it right away.
• Interpret that program later in one or more ways.

Think of it as:

An AST of effectful operations + bind/flat_map to chain them.

You split:

• Syntax → enum of instructions.
• Semantics → interpreter function.

“Free” means you can build a monad from any functor (F) without committing to meaning.

Rust Implementation

Free Monad type

#![allow(unused)]
fn main() {
#[derive(Clone)]
enum Free<F, A> {
    Pure(A),
    Suspend(F),
    FlatMap(Box<Free<F, A>>, Box<dyn Fn(A) -> Free<F, A>>),
}

impl<F: Clone + 'static, A: 'static> Free<F, A> {
    fn pure(a: A) -> Self {
        Free::Pure(a)
    }

    fn flat_map<B: 'static, G>(self, f: G) -> Free<F, B>
    where
        G: Fn(A) -> Free<F, B> + 'static,
        F: 'static,
    {
        match self {
            Free::Pure(a) => f(a),
            Free::Suspend(op) => {
                Free::FlatMap(Box::new(Free::Suspend(op)), Box::new(f))
            }
            Free::FlatMap(inner, g) => {
                Free::FlatMap(inner, Box::new(move |x| g(x).flat_map(f.clone())))
            }
        }
    }
}
}

DSL: Console operations

#![allow(unused)]
fn main() {
#[derive(Clone)]
enum Console<A> {
    Print(String, A),
    ReadLine(fn(String) -> A),
}

// Smart constructors
fn print_line(s: &str) -> Free<Console<()>, ()> {
    Free::Suspend(Console::Print(s.to_string(), ()))
}

fn read_line() -> Free<Console<String>, String> {
    Free::Suspend(Console::ReadLine(|input| Free::Pure(input)))
}
}

Interpreter

#![allow(unused)]
fn main() {
fn run_console<A>(mut prog: Free<Console<A>, A>) -> A {
    loop {
        match prog {
            Free::Pure(a) => return a,
            Free::Suspend(Console::Print(s, next)) => {
                println!("{}", s);
                prog = Free::Pure(next);
            }
            Free::Suspend(Console::ReadLine(f)) => {
                let mut buf = String::new();
                std::io::stdin().read_line(&mut buf).unwrap();
                prog = f(buf.trim().to_string());
            }
            Free::FlatMap(inner, cont) => match *inner {
                Free::Pure(a) => prog = cont(a),
                Free::Suspend(op) => prog = Free::Suspend(op), // minimal handling
                _ => unimplemented!(),
            },
        }
    }
}
}

Usage

fn main() {
    let program =
        print_line("What is your name?")
        .flat_map(|_| read_line())
        .flat_map(|name| print_line(&format!("Hello, {name}!")));

    run_console(program);
}

Takeaway

• Syntax = enum Console (possible instructions)
• Program = Free<Console, A> (data describing steps)
• Semantics = run_console (interpreter)
• Benefit: You can write multiple interpreters for the same program — e.g., run in real IO, log to a file, or compile to another language.

Correlation to Continuations and CPS

Continuation-Passing Style (CPS) is a way of writing programs where functions never return values directly but instead pass results to another function (the continuation) that represents “the rest of the program.”

A free monad is basically a program as a sequence of steps, where each step says:

"Do this, then continue with the rest."

That “rest of the program” is exactly a continuation — a function from the current result to the next step.

• In our Rust free monad:

  #![allow(unused)]
  fn main() {
  Free::FlatMap(Box<Free<F, A>>, Box<dyn Fn(A) -> Free<F, A>>)
  }

  the Box<dyn Fn(A) -> Free<F, A>> is the continuation.

• When you interpret a free monad, you are running in CPS:

  • Instead of returning values directly, you pass them into the next continuation.
  • You end up in a loop of: current_instruction -> feed result into continuation -> next instruction

• CPS relation:

  • Free monads encode CPS in a data structure.
  • CPS is the runtime control flow representation of the same idea.

Quick mapping:

GoF Design Patterns Mapping

Free monads are not in GoF because they’re from functional programming theory, but they subsume or emulate several patterns:

Why Free Monad > These Patterns

• GoF patterns are manual OOP work - you define interfaces, classes, and compose them.

• Free monads are algebraic - you define data for instructions and functions to interpret them.

• You automatically get:

  • Sequencing (flat_map)
  • Composition
  • Multiple interpreters without touching core logic

Summary Table:

Relation to Defunctionalization

Defunctionalization is a program transformation that replaces higher-order functions with a first-order data structure that represents the possible functions, plus an interpreter that applies them.

In CPS, continuations are higher-order functions. Defunctionalizing a CPS program replaces those continuations with an enum of continuation cases and an apply function to run them.

A free monad can be seen as the result of defunctionalizing the continuations inside a CPS-transformed program:

1. Start with a CPS version of your program. The "rest of the program" is carried in continuation functions.
2. Defunctionalize those continuation functions into a finite set of cases in a data type.
3. The resulting data type, together with the initial instruction set, is exactly the AST of a free monad.

Key similarities

• Both free monads and defunctionalization produce a data representation of computation and require an interpreter to give meaning to that data.
• The FlatMap case in a free monad holds the continuation; defunctionalization replaces that closure with a case in a data type.

Key differences

Summary Defunctionalization is a transformation technique. Free monads are a reusable design pattern. The free monad structure is what you get when you defunctionalize the continuations in a CPS program built from a functor F.

Continuation-Passing Style (CPS)

Definition

Continuation-Passing Style (CPS) is a way of writing programs where functions do not return values directly. Instead, they pass their result to another function called a continuation, which represents the rest of the program.

Motivation

• Makes control flow explicit and programmable.
• Enables advanced transformations such as non-blocking IO, early exits, coroutines, backtracking, and concurrency scheduling.
• Used in compiler intermediate representations to simplify optimization and analysis.

Basic Form

In direct style:

fn add_one(x: i32) -> i32 {
    x + 1
}

fn main() {
    let y = add_one(41);
    println!("{}", y);
}

In CPS:

fn add_one_cps(x: i32, k: impl Fn(i32)) {
    k(x + 1)
}

fn main() {
    add_one_cps(41, |y| {
        println!("{}", y);
    });
}

Here, k is the continuation. Instead of returning x + 1, we call k(x + 1).

Key Properties

• All function calls are tail calls to continuations.
• The current computation never "returns" to the caller; instead it jumps into the continuation.
• Control flow becomes explicit in the program.

Relation to Higher-Order Functions

• In CPS, continuations are just higher-order functions.
• Each step of the computation receives a continuation representing what to do next.

Relation to Defunctionalization

• In CPS, the continuation is an actual function value.
• Defunctionalization replaces the continuation function with a data structure (enum) that represents possible next steps, plus an apply function to interpret them.

Relation to Free Monads

• The FlatMap constructor in a free monad is exactly a stored continuation.
• Interpreting a free monad is like executing CPS code where the continuation is part of the program data.
• Free monads can be obtained by taking CPS code and defunctionalizing the continuations.

Advantages

• Flexible control flow representation.
• Easier to reason about evaluation order.
• Powerful for implementing interpreters, debuggers, optimizers, and async runtimes.

Disadvantages

• Verbose compared to direct style.
• Can be harder to read for humans.
• Requires tail call optimization for efficiency in languages without native support for it.

Defunctionalization

Definition

Defunctionalization is a program transformation that replaces higher-order functions with a first-order data structure that represents the possible functions, plus an interpreter function that applies them.

Motivation

Some languages, compilers, or runtimes cannot handle higher-order functions efficiently or at all. By defunctionalizing, you make the program purely first-order, which is easier to compile, analyze, serialize, or run in restricted environments.

The Process

1. Identify all possible higher-order functions that may be created and passed around.
2. Assign each such function a unique tag in an enum or sum type, along with any data it needs to operate.
3. Replace function values with these tags.
4. Define an apply function that takes a tag and the function arguments, then pattern matches on the tag to run the correct code.

Example in Rust

Before: using a closure

#![allow(unused)]
fn main() {
let k: Box<dyn Fn(i32) -> i32> = Box::new(|x| x + 1);
println!("{}", k(41));
}

After: defunctionalized form

#![allow(unused)]
fn main() {
enum Cont {
    Add1
}

fn apply(c: Cont, x: i32) -> i32 {
    match c {
        Cont::Add1 => x + 1,
    }
}

println!("{}", apply(Cont::Add1, 41));
}

Properties

• All functions are now represented by simple data.
• The program becomes purely first-order.
• The apply function replaces direct function calls.

Applications

• Compiler backend simplification: many compilers generate CPS code and then defunctionalize it.
• Serialization of functions: you can send the enum tag over a network or store it in a file.
• Static analysis: first-order code is easier to reason about.
• Derivation of interpreters: defunctionalization naturally leads to an interpreter pattern.

Relation to CPS

In CPS (continuation-passing style), continuations are higher-order functions. Defunctionalizing CPS code turns these continuations into a finite set of cases in an enum plus an apply function.

Relation to Free Monads

A free monad can be seen as the result of defunctionalizing the continuations in a CPS-transformed program. The resulting data structure is the free monad's AST, and the apply function is the interpreter.

References

• Reynolds, J. C. (1972). Definitional Interpreters for Higher-Order Programming Languages.
  https://dl.acm.org/doi/epdf/10.1145/800194.805852
• Yallop, J., and White, L. (2014). Lightweight Higher-Kinded Polymorphism (uses defunctionalization to encode type-level application).
  https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf

Dependent Types

Definition

A type system is called dependent when types can depend on values. This means that the shape, constraints, or meaning of a type may be parameterized by program values. With dependent types, you can express rich invariants and relationships directly in the type system.

Examples

• Vec<n, T> - a vector type indexed by its length n
• Matrix<rows, cols, T> - dimensions encoded in the type
• Proof<p> - a type representing a proof of a proposition p

For instance, in a language with dependent types:

append : Vec<n, T> -> Vec<m, T> -> Vec<n + m, T>

The type says that appending two vectors produces a vector whose length is the sum of the lengths.

Purpose

• Capture invariants in the type system so they are checked at compile time
• Reduce or eliminate certain classes of runtime errors
• Allow programs to carry proofs of their own correctness
• Enable more expressive APIs where type signatures encode precise behavior

Key Characteristics

• Types are computed: Types can be expressions evaluated from program values
• Terms appear in types: No strict separation between values and types
• Type checking may evaluate code: The compiler may need to run computations to verify type constraints
• Expressiveness: Can model proofs, exact sizes, state transitions, or logical conditions

Dependent Function Types

A dependent function type is written (in type theory notation) as:

Π x : A. B(x)

This means: for each value x of type A, the result type is B(x) which may depend on the value of x.

In programming terms:

• Non-dependent function:

  f : A -> B
  

  The output type B is fixed regardless of the input value.

• Dependent function:

  f : (x : A) -> B(x)
  

  The output type varies based on the actual input x.

In Practice

• Fully supported in Agda, Idris, Coq, Lean

• Rust supports restricted forms via const generics and trait bounds

• Commonly used for:

  • Exact-size arrays and matrices
  • State machines with type-level states
  • Encoding logical proofs alongside code

Branching and Confluence

We encounter branching constantly in everyday life. Imagine:

• You wake up and decide: ☕ coffee or 🍵 tea.
• If coffee: sugar or no sugar?
• If tea: green or black?

Each decision branches into alternatives, like a little decision tree. But in the end, you don’t live in two universes — you end up with one drink in your hand. That’s confluence: although choices branch, they merge back into one reality.

Branching in Rust Programs

The same pattern appears in programs. A sequential program may branch internally, but execution always continues as a single flow.

if

#![allow(unused)]
fn main() {
fn sign(x: i32) -> i32 {
    if x > 0 {
        1
    } else if x < 0 {
        -1
    } else {
        0
    }
}
}

• Branching: program splits into one of three paths.
• Confluence: for a given input value, the same branch condition will always be chosen. Each input deterministically follows exactly one path, and evaluation of conditions happens in a fixed order (first check x > 0, then x < 0, else default). Regardless of which path is taken, the result is always determined from the input, and execution continues in a single, unified flow.

match

#![allow(unused)]
fn main() {
fn day_type(day: &str) -> &str {
    match day {
        "Saturday" | "Sunday" => "Weekend",
        "Monday" | "Tuesday" | "Wednesday" | "Thursday" | "Friday" => "Weekday",
        _ => "Unknown",
    }
}
}

• Branching: many alternatives.
• Confluence: for a given input value, the program deterministically selects exactly one matching branch. The essential property is that the trace of evaluation is deterministic: the same input always leads down the same path. In this simple example each branch yields the same type (&str), but even in settings with dependent types—where result types vary with input—the execution remains confluent because identical inputs always produce the same path and outcome.

Loops with Early Exit

#![allow(unused)]
fn main() {
fn find_even(nums: &[i32]) -> Option<i32> {
    for &n in nums {
        if n % 2 == 0 {
            return Some(n); // branch: exit early
        }
    }
    None // confluence: reached if loop completes
}
}

• Branching: may exit during iteration.
• Confluence: one thread of control — either returns early or finishes and continues.

Sequential Confluence Illustrated

Start
 ├─ branch A → ...
 └─ branch B → ...
           ↘
            Confluence → continues as one flow

Just like your morning drink decision, a program doesn’t split into parallel worlds. Branches are local alternatives, but sequential confluence ensures only one actual path is taken, and execution rejoins into one future.

⚡ Key idea: Branching explores alternatives, confluence merges them back. In sequential programs, confluence is guaranteed: there’s always one final thread of execution.

Confluence Beyond Determinism

Confluence is often explained as the guarantee that the same input always produces the same output. But its essence is deeper: the trace of evaluation itself is deterministic. This means the path through the program is uniquely determined by the input, independent of external factors. In Rust, both if and match enforce deterministic traces. More broadly, confluence is what allows reasoning about programs algebraically, since the same input always reduces in a predictable way.

Trace Equivalence

Trace equivalence means that two programs, given the same input, follow evaluation paths that yield the same observable behavior: the same result and the same observable effects. In pure code (no effects), this reduces to producing the same result for all inputs. With side effects, equivalence also requires that the same conditions are evaluated in the same order.

Example of not trace‑equivalent (side effect changes trace):

#![allow(unused)]
fn main() {
fn is_admin() -> bool {
    println!("checked admin"); // side effect
    true
}
fn is_user() -> bool {
    println!("checked user"); // side effect
    true
}

fn classify_role(x: i32) -> &'static str {
    if is_admin() {
        "admin"
    } else if is_user() {
        "user"
    } else {
        "other"
    }
}
}

Here both is_admin and is_user return true, so the result is always "admin". But the trace differs: if is_admin is checked first, only that prints; if conditions are reordered, is_user prints instead. The outcome is the same, but the traces differ, so the programs are not trace‑equivalent.

Trace‑equivalent reorder (pure, disjoint, total):

#![allow(unused)]
fn main() {
fn classify_a(x: i32) -> &'static str {
    if x < 0 { "neg" } else if x == 0 { "zero" } else { "pos" }
}
fn classify_b(x: i32) -> &'static str {
    if x == 0 { "zero" } else if x < 0 { "neg" } else { "pos" }
}
}

The predicates are disjoint and cover all integers; both versions return the same label for every input. With no side effects, these are trace‑equivalent.

Bridge to Trees

Branching in programs naturally connects to tree structures. A sequence of decisions can be visualized as a decision tree: each internal node is a branching point, and each leaf is a possible outcome. Restricting to two alternatives at each branch gives binary trees, which are a cornerstone of computer science. This perspective shifts branching from a control-flow mechanism into a structural representation of possibilities.

Conal Elliott has described memory addressing as a kind of perfect binary leaf trees, where each memory cell corresponds to a leaf reached by a sequence of left/right choices. This view links the abstract branching structure of programs to the very way data is organized and accessed.

Bridge to Semantics

Confluence is also a fundamental property in programming language semantics. In lambda calculus, for example, the Church–Rosser theorem states that if an expression can be reduced in different ways, all reduction paths will converge to a common result. This reflects the same guarantee as sequential confluence in Rust: different branches don’t lead to diverging realities but ultimately rejoin into one meaning. This bridge from everyday branching to formal semantics helps build intuition for deeper topics in programming theory.

Bridge to Bisimulation

Another important concept related to branching is bisimulation, used in process calculi and concurrency theory. Two systems are bisimilar if they can simulate each other’s steps: whenever one makes a move, the other can make a corresponding move, and the resulting states remain related. Unlike simple trace equivalence, bisimulation is sensitive to the structure of branching, not just final results. It ensures that two programs behave the same way under every possible interaction, making it a powerful tool for reasoning about equivalence in concurrent and interactive systems.

There are different flavors of bisimulation:

• Strong bisimulation – requires that every single step of one process can be matched by an identical step in the other, including internal or invisible actions.
• Weak bisimulation – abstracts away from internal or silent actions (often denoted τ). Two systems can be weakly bisimilar if they match on observable behavior, even if one performs extra internal steps.
• Branching bisimulation – a refinement of weak bisimulation that preserves the branching structure more carefully: even when ignoring internal actions, the branching points must align so that the choice structure is respected.

These distinctions are crucial in concurrency theory: strong bisimulation is very strict, weak bisimulation allows flexibility with internal computation, and branching bisimulation balances the two by maintaining the essential shape of choices while abstracting from unobservable details.

Confluence and Bisimulation Compared

Although confluence and bisimulation both deal with branching and outcomes, they apply in different contexts:

• Confluence is about deterministic evaluation: for the same input, all reduction paths lead to the same result. It is mainly used in sequential semantics (e.g., lambda calculus) to prove consistency and simplify reasoning.
• Bisimulation is about behavioral equivalence between two possibly concurrent systems: whenever one system can make a step, the other can match it. It is mainly used in process calculi and concurrency theory to establish that two processes behave the same under all possible interactions.

In short:

• Confluence → guarantees one meaning for each program.
• Bisimulation → guarantees two programs mean the same in terms of behavior.

These notions complement each other: confluence helps ensure determinism in sequential computation, while bisimulation provides a robust notion of equivalence in concurrent or interactive computation.

Operational Semantics in Context

Why Operational Semantics Matters

Operational semantics gives us the step-by-step execution model of a language.
In ALUX, this plays a central role: it is the bridge between abstract meaning and concrete mechanics.

Connection to Free Monads

A free monad describes a program as an AST of instructions.
Interpreting this AST is essentially applying operational semantics:

• Free monad: syntax of instructions + sequencing
• Operational semantics: rules that define how each instruction steps

Thus, an interpreter for a free monad is exactly an operational semantics defined as code.

Connection to CPS

Continuation-Passing Style (CPS) makes the rest of the computation explicit.
Operational semantics can be expressed in CPS:

• Small-step rules correspond to continuations being applied after each instruction.
• The operational machine is just a CPS interpreter in which the continuation is made first-class.

This shows how CPS makes operational semantics executable.

Connection to Defunctionalization

Defunctionalization takes CPS continuations and replaces them with explicit state transitions.
This is precisely what operational semantics rules are:

• Continuation-as-function → State-transition-as-data
• Apply function → Pattern match on instruction + next state

The result is a transition system that matches the structure of operational semantics directly.

Real Example: The EVM

The Ethereum Virtual Machine (EVM) can be understood operationally:

• State: program counter, stack, memory, storage, gas
• Transition rules: one for each opcode (ADD, PUSH, SSTORE, etc.)
• Execution: repeatedly apply small-step rules until halting

In ALUX terms:

• The EVM bytecode is a defunctionalized free monad program.
• The EVM interpreter is its operational semantics.

Dependent Types as Enriched Semantics

Dependent types can enrich operational semantics with proofs:

• Stack safety: pop only valid if stack depth > 0
• Gas constraints: program type encodes available gas and its consumption
• Resource invariants: state transitions guaranteed by types

This turns operational semantics from rules for execution into proofs of correctness.

Summary

• Operational semantics is the execution model of programs.
• Free monads encode the same idea as syntax + sequencing.
• CPS and defunctionalization provide mechanical ways to express operational semantics.
• Real systems like the EVM are defunctionalized operational semantics in practice.
• Dependent types elevate semantics into proof-carrying computations.

Expression Problem Reloaded

This page presents a practical trait-based solution to the Expression Problem: how to add new expression forms and new operations without repeatedly rewriting existing code. The solution is Conal-style in design and tagless-final/object-algebra in encoding. Concretely: we specify compositional meaning first (small capability interfaces and extension-level program specs), and only then provide concrete interpreters. The concrete encoding is in the same family as Oleg Kiselyov’s tagless-final style and Object Algebras: constructor interfaces (LitAlg, AddAlg, MulAlg) define the language signature, programs are written polymorphically against those interfaces, and concrete implementations (like Eval or Pretty) provide interpretations. This avoids committing to one closed AST while preserving static typing and extensibility in both dimensions.

Oleg’s approach is explicitly denotational: assign compositional meaning first, then realize effects/interpreters as modular semantic layers. For the Expression Problem, this is exactly why the alignment with Denotational Design is expected rather than accidental. Conal’s Denotational Design formulation states the same priority directly: specify meaning compositionally first, and treat concrete execution strategies as secondary and replaceable.

For the expression problem, this design means:

• Syntax is modeled as tiny, independent capability traits.
• Semantics are implementations of those traits.
• New syntax adds a new trait, leaving old code untouched.
• New semantics adds a new interpreter type, leaving old code untouched.

Specify Tiny Syntax Capabilities

Each constructor becomes a small trait. This is the specification (spec).

#![allow(unused)]
fn main() {
trait LitAlg {
    type Expr;

    fn lit(&self, n: i64) -> Self::Expr;
}

trait AddAlg {
    type Expr;

    fn add(&self, a: Self::Expr, b: Self::Expr) -> Self::Expr;
}
}

Programs are written as extensions over the alg traits; these extensions are also part of the specification and serve to compose smaller specs into reusable program-level specs:

#![allow(unused)]
fn main() {
#[ext(name = ExprPrograms)]
impl<This> This
where
    This: LitAlg + AddAlg,
{
    fn expr_basic(&self) -> This::Expr {
        self.add(self.lit(2), self.lit(3))
    }
}
}

#[ext(...)] is a macro from the extend crate used to reduce boilerplate by generating extension methods from an impl block; it is not a new Rust language feature.

Add New Semantics (New Interpreter)

Interpreters implement the spec. No syntax changes needed.

#![allow(unused)]
fn main() {
struct Eval;

impl LitAlg for Eval {
    type Expr = i64;

    fn lit(&self, n: i64) -> i64 { n }
}

impl AddAlg for Eval {
    type Expr = i64;

    fn add(&self, a: i64, b: i64) -> i64 { a + b }
}

struct Pretty;

impl LitAlg for Pretty {
    type Expr = String;

    fn lit(&self, n: i64) -> String { n.to_string() }
}

impl AddAlg for Pretty {
    type Expr = String;

    fn add(&self, a: String, b: String) -> String {
        format!("({a} + {b})")
    }
}
}

Now the same expression can be interpreted differently:

#![allow(unused)]
fn main() {
let eval = Eval;
let pretty = Pretty;

let v: i64 = eval.expr_basic();        // 5
let s: String = pretty.expr_basic();   // "(2 + 3)"
}

Add New Syntax (New Capability Trait)

To add Mul, define a new trait. Existing code stays untouched.

#![allow(unused)]
fn main() {
trait MulAlg {
    type Expr;

    fn mul(&self, a: Self::Expr, b: Self::Expr) -> Self::Expr;
}

#[ext(name = ExprProgramsMul)]
impl<This> This
where
    This: LitAlg + AddAlg + MulAlg,
{
    fn expr_with_mul(&self) -> This::Expr {
        self.mul(self.add(self.lit(2), self.lit(3)), self.lit(4))
    }
}
}

Existing interpreters still work for old expressions.
If they want the new syntax, they implement the new trait:

#![allow(unused)]
fn main() {
impl MulAlg for Eval {
    type Expr = i64;

    fn mul(&self, a: i64, b: i64) -> i64 { a * b }
}

impl MulAlg for Pretty {
    type Expr = String;

    fn mul(&self, a: String, b: String) -> String {
        format!("({a} * {b})")
    }
}
}

Why This Solves the Expression Problem

• Add new operations: define a new interpreter type implementing the same specs.
• Add new variants: define a new capability trait and use it only where needed.
• No edits to existing expressions or interpreters unless they opt into new syntax.

This keeps the design modular: simple specs, extension by composition, and thin concrete implementations.

Final Insight: Wadler vs Denotational Design

Wadler diagnosed the Expression Problem correctly at the level of language mechanisms: rows vs columns under static typing and modular extension. But that framing starts after the key mistake is already made: treating concrete representation as the model.

Denotational Design moves the diagnosis upstream. The core failure is representation-first programming: encoding machine structure (ADT, class graph, memory layout) before specifying meaning. Once that commitment is made, extensibility tradeoffs appear as “deep problems.”

From a meaning-first view, many of these tensions are self-inflicted. Define compositional meaning first, then choose encodings. The Expression Problem becomes an engineering choice among encodings, not a conceptual deadlock.

Meaning of a language should be independent of the idea of a machine.

References

• Elliott, C. Denotational design with type class morphisms.
  http://conal.net/papers/type-class-morphisms/

• Elliott, C. Compiling to categories.
  http://conal.net/papers/compiling-to-categories/

• Kiselyov, O. Tagless-final style (overview, tutorials, and papers on final encodings and extensible typed interpreters).
  https://okmij.org/ftp/tagless-final/

• Kiselyov, O. Having an Effect (definitional/denotational framing of effects and extensible interpreters).
  https://okmij.org/ftp/Computation/having-effect.html#defint

• Oliveira, B. C. d. S., and Cook, W. R. (2012). Extensibility for the Masses: Practical Extensibility with Object Algebras.
  https://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf

Referential Transparency Reloaded

This page gives the Denotational Design interpretation of referential transparency. The concept page covers history and mainstream language usage. Here we focus on what RT means as a design constraint.

In DD, RT is not a purity label. It is a law on denotations: substitution must preserve specified meaning.

Denotational Design Restatement of RT

Denotational Design restates RT as a requirement on specifications, not on implementation style. The specification must define compositional meaning first; execution strategy is chosen later.

So RT is checked at the semantic boundary:

• same inputs
• same declared context
• same denotation

If these hold, substitution is valid and equational reasoning is available. This remains true even when concrete interpreters perform I/O, concurrency, retries, or state transitions, because those details are delegated behind the specified capabilities.

In other words, DD does not ask "is this implementation pure?" DD asks "are the denotational equalities explicit, and are interpreters preserving them?"

Purity And RT

RT and purity are related, but not identical.

• RT is a substitution law on meaning.
• purity is an operational constraint: no hidden observable effects.

Purity is a common way to obtain RT for expression-level code. But RT remains the semantic criterion: substitution must preserve specified denotation.

So DD avoids turning RT into a style label like "pure code only". The requirement is explicit semantic equalities, with effects isolated behind capability boundaries.

One minimal semantic reading is:

#![allow(unused)]
fn main() {
fn f(a: A, io: Io) -> (Result<B, E>, Io)
}

For the same a and same io input, f yields the same (result, io'). This is the DD-style, context-indexed form of substitution reasoning.

Why This Clarifies RT

Many RT debates blur a useful distinction:

• semantic transparency
• operational side effects

DD separates these layers:

• semantic core states meaning
• interpreters realize execution strategy

This separation allows practical effects without losing law-based reasoning.

Representation-First Failure Mode

If you commit early to concrete representation, RT discussion drifts into style arguments:

• "this style is pure"
• "that style is impure"
• "IO wrappers fix it"

These are mostly encoding debates. DD asks a simpler question: what equalities are valid in your specification?

Practical DD Pattern

Define tiny capability traits and write program behavior as extensions over them. Then provide thin concrete interpreters.

#![allow(unused)]
fn main() {
trait FileSystem {
    type Error;

    fn file_read(&self, name: &str) -> Result<String, Self::Error>;
}

trait GithubPublish {
    type Error;

    fn github_publish(&self, repo: &str, files: Vec<String>) -> Result<(), Self::Error>;
}

trait Concurrent {
    fn map_concurrent<A, B, E, F>(&self, xs: &[A], f: F) -> Result<Vec<B>, E>
    where
        A: Clone,
        F: Fn(&A) -> Result<B, E>;
}

#[ext(name = PublishProjectExt)]
impl<This> This
where
    This: FileSystem<Error = String> + GithubPublish<Error = String> + Concurrent,
{
    fn publish_project(&self, files: &[&str], repo: &str) -> Result<(), String> {
        let files = self.map_concurrent(files, |name| self.file_read(*name))?;
        self.github_publish(repo, files)
    }
}
}

#[ext(...)] is a macro from the extend crate used to reduce boilerplate by generating extension methods from an impl block; it is not a new Rust language feature.

In Scala FP, RT is often presented through values of type F[A] (for example IO[A], or F[Either[E, A]]). Here, RT is expressed one level up: as capability-bounded program meaning. So this Rust method is not an RT value container in the same encoding sense as F[A]; it is RT behavior specified over explicit capabilities, with concrete effects delegated to implementations.

The extension states semantic behavior against capabilities. Concrete implementations decide execution strategy: batching, retries, transport, parallelism, and storage details.

Final Insight

In Denotational Design, RT is a property of semantic specifications. Implementation choices are secondary as long as they preserve the stated denotational laws.

Keep the law. Do not get stuck on the label.

EVM as a Virtual Machine

The Ethereum Virtual Machine (EVM) is a stack-based virtual CPU that executes Ethereum bytecode. This bytecode is the compiled form of Ethereum smart contracts, usually written in Solidity, Vyper, or another EVM-compatible language.

At the lowest level:

• The EVM processes opcodes (ADD, PUSH, JUMP, SSTORE, etc.).

• Execution state includes:

  • Stack: LIFO data stack for operand storage.
  • Memory: transient byte array for temporary values.
  • Storage: persistent key-value store for each contract.
  • Program counter: points to the next opcode.
  • Gas: metering system that charges for execution steps.

EVM as an Interpreter Pattern

From the free monad and GoF design patterns perspective:

• Instruction Set = EVM opcodes (similar to your enum Console).
• Program AST = Actually, EVM code is already compiled, so it’s a flat sequence of instructions, not a rich high-level AST. High-level languages like Solidity first have a compiler that builds an AST, optimizes it, and then emits EVM bytecode.
• Interpreter = The EVM specification defines how each opcode changes the machine state.
• Multiple interpreters = While the EVM spec is fixed, different clients (Geth, Nethermind, Besu, Erigon) are alternative implementations of the same interpreter.

In GoF terms:

• The EVM is an Interpreter over an instruction language (bytecode).
• Opcodes are Command objects executed in sequence.
• The program state (stack, memory, storage) acts like the context in Interpreter pattern.

EVM and Free Monad Analogy

If we model the EVM in a free monad style:

1. Syntax: Enum of opcodes with parameters, e.g.

   #![allow(unused)]
   fn main() {
   enum EvmInstr<A> {
       Add(A),
       Push(U256, A),
       SStore(U256, U256, A),
       // ...
   }
   }

2. Program: Free<EvmInstr, ()> would represent an abstract Ethereum program before compilation.

3. Semantics: Interpreter function that executes these instructions against the EVM state.

The difference:

• The real EVM executes a linear bytecode sequence (already defunctionalized into an array of low-level instructions).
• A free monad version would allow you to build programs algebraically, chain them with flat_map, and then interpret or compile them into EVM bytecode.

EVM and CPS / Defunctionalization

The EVM’s real execution loop is very similar to a defunctionalized CPS interpreter:

• In CPS: “do instruction, then call continuation”.
• In EVM: “execute opcode, then increment program counter” is equivalent to applying the continuation for that instruction.
• Defunctionalization: The “continuations” are already turned into a position in bytecode (program counter). This is the tag identifying the next action.
• The interpreter (switch or match on opcode) is the apply function of the defunctionalized continuations.

So:

• CPS form: Smart contract execution as “do opcode → continuation”.
• Defunctionalized form: Replace continuations with pc + bytecode array.
• Free monad form: Build higher-level EVM programs before compiling them into the defunctionalized form.

Key Insight

EVM execution = defunctionalized CPS interpreter for Ethereum bytecode.

Mini EVM

Here’s a mini-EVM in Rust using the same free monad style from the Console example, so you can clearly see the mapping to Ethereum’s real EVM execution model.

Instruction Set (EVM subset)

#![allow(unused)]
fn main() {
#[derive(Clone)]
enum EvmInstr<A> {
    Push(u64, A),              // Push constant to stack
    Add(A),                    // Pop two, push sum
    SStore(u64, u64, A),       // Store key-value
    SLoad(u64, fn(u64) -> A),  // Load value from storage
}
}

Free Monad Core

#![allow(unused)]
fn main() {
#[derive(Clone)]
enum Free<F, A> {
    Pure(A),
    Suspend(F),
    FlatMap(Box<Free<F, A>>, Box<dyn Fn(A) -> Free<F, A>>),
}

impl<F: Clone + 'static, A: 'static> Free<F, A> {
    fn pure(a: A) -> Self {
        Free::Pure(a)
    }
    fn flat_map<B: 'static, G>(self, f: G) -> Free<F, B>
    where
        G: Fn(A) -> Free<F, B> + 'static,
    {
        match self {
            Free::Pure(a) => f(a),
            other => Free::FlatMap(Box::new(other), Box::new(f)),
        }
    }
}
}

Smart Constructors

#![allow(unused)]
fn main() {
fn push(val: u64) -> Free<EvmInstr<()>, ()> {
    Free::Suspend(EvmInstr::Push(val, ()))
}

fn add() -> Free<EvmInstr<()>, ()> {
    Free::Suspend(EvmInstr::Add(()))
}

fn sstore(key: u64, value: u64) -> Free<EvmInstr<()>, ()> {
    Free::Suspend(EvmInstr::SStore(key, value, ()))
}

fn sload(key: u64) -> Free<EvmInstr<u64>, u64> {
    Free::Suspend(EvmInstr::SLoad(key, Free::pure))
}
}

EVM State

#![allow(unused)]
fn main() {
use std::collections::HashMap;

struct EvmState {
    stack: Vec<u64>,
    storage: HashMap<u64, u64>,
}
}

Interpreter

#![allow(unused)]
fn main() {
fn run_evm<A>(mut prog: Free<EvmInstr<A>, A>, state: &mut EvmState) -> A {
    loop {
        match prog {
            Free::Pure(a) => return a,
            Free::Suspend(EvmInstr::Push(v, next)) => {
                state.stack.push(v);
                prog = Free::Pure(next);
            }
            Free::Suspend(EvmInstr::Add(next)) => {
                let b = state.stack.pop().unwrap();
                let a = state.stack.pop().unwrap();
                state.stack.push(a + b);
                prog = Free::Pure(next);
            }
            Free::Suspend(EvmInstr::SStore(k, v, next)) => {
                state.storage.insert(k, v);
                prog = Free::Pure(next);
            }
            Free::Suspend(EvmInstr::SLoad(k, cont)) => {
                let val = *state.storage.get(&k).unwrap_or(&0);
                prog = cont(val);
            }
            Free::FlatMap(inner, cont) => match *inner {
                Free::Pure(a) => prog = cont(a),
                Free::Suspend(op) => prog = Free::Suspend(op),
                _ => unreachable!(),
            },
        }
    }
}
}

Example Program

fn main() {
    let program = push(2)
        .flat_map(|_| push(3))
        .flat_map(|_| add())
        .flat_map(|_| sstore(1, 5))
        .flat_map(|_| sload(1))
        .flat_map(|val| push(val));

    let mut state = EvmState {
        stack: vec![],
        storage: HashMap::new(),
    };

    run_evm(program, &mut state);

    println!("Final stack: {:?}", state.stack);
    println!("Storage: {:?}", state.storage);
}

How This Maps to the Real EVM

• EvmInstr enum = EVM opcode set (syntax).
• Free<EvmInstr, A> = Abstract EVM program before compilation.
• run_evm = Interpreter (like Geth, Besu, Nethermind).
• EvmState = EVM stack, memory, and storage.
• The FlatMap continuations here are exactly what the real EVM defunctionalizes into a program counter and bytecode array.

Here is the defunctionalized mini-EVM: continuations are replaced by a program counter.

Core idea

• Continuation in Free FlatMap becomes an integer pc.
• Program is a flat Vec<Op>.
• The interpreter is a loop that reads code[pc], mutates state, then updates pc.

Rust code

use std::collections::HashMap

#[derive(Clone, Debug)]
enum Op {
    Push(u64),
    Add,
    SStore(u64, u64),
    SLoad(u64),       // pushes value at key
    Halt,
}

#[derive(Default)]
struct VM {
    pc: usize,
    stack: Vec<u64>,
    storage: HashMap<u64, u64>,
    code: Vec<Op>,
}

impl VM {
    fn new(code: Vec<Op>) -> Self {
        VM { code, ..Default::default() }
    }

    fn step(&mut self) -> bool {
        match self.code.get(self.pc).cloned().unwrap_or(Op::Halt) {
            Op::Push(v) => {
                self.stack.push(v);
                self.pc += 1;
            }
            Op::Add => {
                let b = self.stack.pop().expect("stack underflow")
                let a = self.stack.pop().expect("stack underflow")
                self.stack.push(a + b);
                self.pc += 1;
            }
            Op::SStore(k, v) => {
                self.storage.insert(k, v);
                self.pc += 1;
            }
            Op::SLoad(k) => {
                let v = *self.storage.get(&k).unwrap_or(&0);
                self.stack.push(v);
                self.pc += 1;
            }
            Op::Halt => return false,
        }
        true
    }

    fn run(&mut self) {
        while self.step() {}
    }
}

fn main() {
    // Program: push 2; push 3; add; sstore 1,5; sload 1; halt
    let code = vec![
        Op::Push(2),
        Op::Push(3),
        Op::Add,
        Op::SStore(1, 5),
        Op::SLoad(1),
        Op::Halt,
    ]

    let mut vm = VM::new(code)
    vm.run()

    println!("Final stack: {:?}", vm.stack)
    println!("Storage: {:?}", vm.storage)
}

Mapping to Free and CPS

• Free continuation Fn(A) -> Free is now the integer pc.
• match on Op is the defunctionalized apply function.
• Vec<Op> is the defunctionalized program - a linear bytecode.
• The loop while self.step() is the CPS trampoline without closures.

Free Monads with Dependent Types

Dependent Types as a Natural Fit

Free monads describe computations as data. Dependent types allow us to express properties of these computations in their types. By combining the two, we can write programs that are:

• Easier to compose because type constraints guide construction
• Safer because invalid programs cannot type-check
• Self-documenting because the type itself encodes a specification
• Proof-carrying because the type may serve as a logical statement and the program as its proof

Making Composition Easier

In a non-dependent setting, a free monad type might look like:

Free<F, A>

where F is the instruction set and A is the return value type.

With dependent types, we can enrich this to:

Free<F, A, P>

where P is a predicate or property about the program. The type system can ensure that when two programs are composed with flat_map, the resulting program's property is automatically derived from the inputs.

Example:

Free<EvmInstr, A, GasUsed <= Limit>

The type carries a proof that the program's gas usage is below the limit.

Turning Programs into Proofs

In dependent type theory, a type can represent a proposition and a term of that type is a proof. A free monad program can be viewed as a construction of a proof about the sequence of instructions.

Example in a dependently typed language:

-- In Idris/Agda style
data Program : GasLimit -> GasLimit -> Type -> Type where
  Pure   : A -> Program g g A
  Instr  : F X -> Program g1 g2 X -> Program g1 g2 A

Here:

• The type Program g_in g_out A says that running the program transforms the available gas from g_in to g_out and produces an A.
• Writing a program of this type is a proof that the gas accounting is correct.

Benefits Over Plain Free Monads

Without dependent types:

• Safety relies on runtime checks or careful manual construction.
• Properties like "stack never underflows" or "resource usage within bounds" require testing or external proofs.

With dependent types:

• The type system enforces these properties during program construction.
• A well-typed program is already a certificate that it satisfies the desired property.

Example: Safe Stack Operations

Plain free monad:

push : Val -> Free<StackInstr, ()>
pop  : Free<StackInstr, Val> -- may fail at runtime if empty

Dependent free monad:

push : Val -> Program<Depth, Depth + 1, ()>
pop  : Program<Suc Depth, Depth, Val> -- only type-checks if Depth > 0

Here, the type encodes the stack depth before and after the operation. An attempt to pop from an empty stack is a type error, not a runtime failure.

Summary

• Dependent types turn free monads into proof-carrying programs.
• They make composition easier by tracking and combining properties automatically.
• They can statically guarantee safety and correctness without runtime checks.
• The type of a free monad program can be the proposition it proves.

About

This book distills a way of thinking about software inspired by Conal Elliott’s Denotational Design. The core idea is simple yet profound:

In this view, computation is not an opaque sequence of steps but a transparent mathematical object. We begin with specifications as pure, compositional descriptions of what a program means. These are expressed as algebraic structures, often in the form of traits or type signatures. The implementation, how those meanings are realized, is a separate, interchangeable layer.

By separating meaning from mechanics, we gain:

• Clarity - programs read like precise definitions.
• Composability - parts fit together algebraically.
• Refactorability - meaning stays fixed while implementation evolves.
• Correctness - reasoning about programs becomes equational, not operational.

These guidelines aim to provide practical techniques for applying this style in modern programming languages, especially Rust, without losing the elegance and rigor of its mathematical roots.

Reference of mdbook

mdBook documentation

Reference of admonish mdbook plugin (tooltip boxes)

admonish documentation