Evaluation
Free-variable analysis, substitution, and call-by-value function application.
PROGRAMMING LANGUAGES / COURSE PROJECTUCSB CS162 · OCAML
λ⁺ Interpreter &
Type InferenceSmall language. Deep foundations.
From evaluating expressions to reasoning about their types: implementing the core algorithms of a small functional language in OCaml.
Operational semantics. Type systems. Unification.Explore type inference ↓
The project
Turning language rules
into working algorithms.
Across a sequence of assignments, I implemented the core evaluation and type-analysis algorithms for λ⁺. The work progressed from substitution-based evaluation to checking annotated programs and inferring types through constraints.
01 / Implementation scope
My contribution
The course supplied the AST, parser, supporting utilities, and interactive interface. Within that framework, I implemented the following core algorithms.
Additional language constructs
Arithmetic, conditionals, lists, pattern matching, and recursive definitions.
Static analysis
Environment-based type checking and constraint-based type inference.
Constraint solving
Type substitution and unification with an occurs check.
Additional work: simultaneous substitution and alpha-equivalence checking.
02 / Runtime
Building the interpreter
The interpreter recursively evaluates the abstract syntax tree. For function application, it evaluates the function and argument, substitutes the resulting argument value into the function body, and evaluates that body.
Evaluate functionEvaluate argumentSubstitute valueEvaluate body
Respecting variable scope
Free-variable analysis distinguishes references from names introduced by functions, let expressions, and pattern matching. Substitution stops beneath a binding that shadows the variable being replaced.
Extending the language
Lists, conditional execution, and recursion through a fixed-point operator enable recursive computations within the same evaluation model.
03 / Static analysis
From type checking
to type inference.
The type checker translates typing rules into recursive checks. The inference engine introduces fresh type variables for missing annotations, generates equality constraints, and solves them through unification.
Function application
λf. λx. f xInferred type(β → γ) → β → γ
Introduce unknowns
Assign f the fresh type α and x the fresh type β.
Generate a constraint
Give the application f x a fresh result type γ. Applying f to x requires α = β → γ.
Unify and substitute
Solve the equation with the substitution α ↦ β → γ, then apply it to the provisional type α → β → γ.
Construct the function type
The resulting type is (β → γ) → β → γ.
Rejecting infinite types
In λx. x x, the same x acts as both function and argument. With x : α and a fresh result type β, the application requires α = α → β. The occurs check rejects this constraint because α appears within its own replacement, which would require an infinite type.
04 / Reflection
Formal ideas, executable systems.
Evaluation rules became recursive interpreter cases; typing judgments became environment-based checks; and unknown types became constraints that could be solved systematically.
The project deepened my understanding of how bindings determine variable scope, how expressions evaluate at runtime, and how static analysis reasons about a program before execution.