diy-marking

A template for you to implement the Marked Lambda Calculus — scaled down into a minimal bidirectional core — on top of a Hazelnut-style structure editor, yourself.

Setup

Installing and Setting Up OCaml

You will need to have the OCaml toolchain installed. If you have not already installed it, I recommend the official Get Up and Running With OCaml tutorial.

Once you do that, I recommend you setup an opam switch just for this project. You can think of a switch like an isolated environment to install opam packages. The packages you install in one switch won't interfere with the packages installed in another switch.

To create the switch:

opam switch create diy-marking 5.2.0

To set this switch as the currently active one:

opam switch set diy-marking

To list all the switches you have:

opam switch list

To learn more about switches:

man opam-switch

Installing Dependencies

If you setup a switch for this project, make sure that it's active:

opam switch set diy-marking

To install the dependencies to the currently active switch:

make deps

Building, Running, etc.

All the build commands are managed by the Makefile. You're free to modify it to your own liking, but as it is provided, here's what the commands do:

To autoformat your code:

make fmt

To build the webapp:

make build

To autoformat and build:

make

To get the URL for the webapp:

make url

To erase the build:

make clean

To test your implementation:

make test

Background

Before writing any code, make sure you've read (at least) these parts of the two papers:

• Hazelnut: A Bidirectionally Typed Structure Editor Calculus — familiarise yourself with the bidirectional type system (Section 3.1) and the action calculus (Section 3.3). In particular, you should understand what a zippered expression is, how type information is threaded through the cursor, and why every edit needs its own rule.

• Total Type Error Localization and Recovery with Holes — focus on Section 2 (the marked lambda calculus) and Section 3.2 (fixing holes in Hazelnut). Sections 1–2.1.5 are the most important; skim the rest as needed. The core idea: marking is a total transformation from unmarked expressions into marked expressions, inserting error marks around ill-typed subterms so that editor services keep working even when the program is locally broken.

The calculus implemented here is deliberately minimal:

• Types — Num, Hole (identified with the unknown type ? in Zhao et al.), and Arrow(τ, τ).

• Unmarked expressions — Var, NumLit, Plus, Lam(x, τ, e) (with type annotation), Ap, Asc(e, τ), EHole.

• Marked expressions — the above plus Mark(e, mark) wrappers, where mark is one of:

  Mark	Paper notation	When it is inserted
  Free	⌊ x ⌋□	the variable x is not in scope (§2.1.3, MKSFree)
  NonArrowAp	⌊ ě ⌋⇒▶̸→	the applicand synthesises a non-arrow type (§2.1.5, MKSAp2)
  LamAscIncon	⌊ λx:τ. ě ⌋:	a λ is analysed against an arrow whose input type is inconsistent with its annotation (§2.1.4, MKALam3)
  Inconsistent	⌊ ě ⌋≁	the synthesised type is inconsistent with the expected type (§2.1.2, MKAInconsistentTypes)

• Actions — Move(Dir), Construct(Shape), Del. Because marking is a separate post-pass (see Zhao et al. §3.2), actions operate on unmarked zippered expressions and never fail: invalid actions simply return the input unchanged.

Implementing diy-marking

All the code you will write lives in hazelnut/hazelnut.re. The starter code is organised to match the structure of the two papers, with rule names in comments mapping each case to the formal system. Modifying any other files (especially hazelnut/hazelnut.rei) isn't recommended, since it might cause unexpected problems.

A typctx is a map from variable names to types. You can insert/update values with TypCtx.add, and read values with TypCtx.find_opt. See the OCaml Map documentation for more details.

Guided Implementation Order

The recommended order follows the dependency chain — each step only requires functions from earlier steps.

Step 1: Type compatibility helpers (Fig. 4 & Fig. 5 of Zhao et al.)

Implement matched_arrow_typ and type_consistent. These are small, self-contained functions that the rest of the system depends on. The helpers test suite verifies them in isolation.

• matched_arrow_typ(τ) — returns Some((τ₁, τ₂)) for any arrow-shaped type (including Hole, which acts like Hole→Hole), and None otherwise. (Zhao et al. Fig. 5: TMAArr, TMAUnknown.)

• type_consistent(τ₁, τ₂) — true when τ₁ ∼ τ₂ (reflexive, symmetric, not transitive). Hole is consistent with everything. (Zhao et al. Fig. 4.)

Step 2: Cursor erasure (Hazelnut 2017, Appendix A.2)

Implement erase_typ and erase_exp. These strip the cursor position from a zipper, recovering the underlying H-type or H-expression. They are needed by the action semantics and by the webapp, which re-marks the entire program after every edit. The erase_exp and helpers test suites cover these.

Step 3: Marking (Zhao et al. 2024, §2.1)

Implement mark_syn and mark_ana, which are mutually recursive. Both are total: they never return None and never raise on a well-formed unmarked input. The recipe from the paper is:

1. For every synthetic rule of the unmarked system, write a case in mark_syn that produces the same term (plus marks on any ill-typed sub-terms).

2. For every analytic rule, write a case in mark_ana. Lambdas are the only non-subsumable form in this minimal calculus, so the analytic rule for Lam has to handle both the "arrow-and-consistent- annotation" (MKALam1) and "arrow-but-inconsistent-annotation" (MKALam3) cases. For every other form, fall back to subsumption.

3. For any rule whose premise in the unmarked system would fail, wrap the result in the appropriate Mark in the marked system. This is what makes marking total.

The syn and ana test suites cover these.

Tip: to test incrementally while your implementation is incomplete, use raise(Unimplemented) to fill the gaps. The webapp will warn you if it reaches an unimplemented part, but it won't crash.

Step 4: Edit actions (Hazelnut 2017 §3.3; Zhao et al. §3.2)

This is the largest step. Because actions operate on unmarked zippered expressions and never fail, every function below returns a plain Zexp.t (or Ztyp.t) and defaults to the input on invalid actions.

Implement these internal helpers first:

1. move_typ — type-zipper movement rules (A.3.2).

2. move_action — expression-zipper movement rules. Handle each Zexp form's Child(One) / Child(Two) / Parent cases, plus zipper recursion (delegating to move_typ for the RAsc and LLam cases).

3. typ_action — type actions: move, delete, construct (Arrow, Num), plus zipper recursion through LArrow and RArrow.

4. syn_action — the main action function:

   • Movement — delegates to move_action.
   • Deletion — replaces the cursor target with EHole.
   • Construction — the bulk of the rules, one case per Shape. Shape constructors for types (Arrow, Num) only fire in type contexts; they are no-ops on expressions at the top level, but should propagate through the zipper to reach any embedded Ztyp.
   • Zipper rules — propagate the action through each non-Cursor Zexp form.

The type_action, syn_action, and properties test suites progressively exercise these.

Step 5: Re-marking a zipper (Zhao et al. §3.2)

Implement fold_zexp_mexp. After each edit, the webapp:

1. Cursor-erases the Zexp.t to get a plain Hexp.t.
2. Runs mark_syn on it to get a marked Hexp.t.
3. Calls fold_zexp_mexp(z, e) to fold the marks from e back onto the zipper z, preserving the cursor position.

fold_zexp_mexp traverses (z, e) in lock-step, copying Mark wrappers from the Hexp side onto matching positions on the Zexp side.

Test Suite

The test suite is organised to mirror both papers. Each test file targets a specific judgement or set of rules, and the test names reference the paper's rule labels.

File	What it tests	Paper reference
Test_helpers.re	type_consistent, matched_arrow_typ, erase_typ	Zhao et al. Figs. 4–5; Hazelnut A.2.1
Test_erase_exp.re	Expression cursor erasure	Hazelnut A.2.2 (extended)
Test_syn.re	mark_syn rules	Zhao et al. §2.1 MKS*
Test_ana.re	mark_ana rules	Zhao et al. §2.1 MKA*
Test_type_action.re	Type-zipper actions	Hazelnut A.3.1
Test_syn_action.re	Expression actions (Move / Del / Construct / zipper recursion)	Hazelnut A.3.3 (decoupled variant)
Test_properties.re	Metatheorem verification (Totality, Well-Formedness, …)	Zhao et al. Thms 2.1–2.4; Hazelnut Thm 2
Test_qcheck.re	Property-based random testing of the metatheorems	Zhao et al. Thms 2.1–2.4; Hazelnut Thm 2

Design principle: tests deliberately use compound, non-value subexpressions (e.g. Plus(Plus(NumLit(2), NumLit(3)), Plus(NumLit(4), NumLit(5))) rather than Plus(NumLit(2), NumLit(2))) to catch the common student mistake of only handling leaf forms like NumLit or Var in recursive positions.

The QCheck property-based tests (Test_qcheck.re) generate random expressions and verify the metatheorems hold on them. These tests pass vacuously on Unimplemented stubs (they try … with Unimplemented -> true), so you can run make test at any stage and only the tests that actually exercise your implemented code will fail.

Using the Webapp

Once you've built the webapp with make build, you can open it in your browser. Run the command make url to get the URL.

The first thing you see will be the Hazelnut expression you're building, with cursor markers and any marks the marker has inserted, followed by the synthesized type. Below that are the buttons that perform actions on the expression. If the button has an input field, you have to fill that in before pressing the button.

If anything unexpected happens, a warning will appear at the bottom:

Warning	Meaning
Unimplemented	You called upon an operation that you haven't implemented yet.

Using the Maybe Monad

Have you ever written code that looks like this?

switch (a) {
| Some(b) =>
  switch (f(b)) {
  | Some(c) =>
    switch (g(c)) {
    | Some(d) => Some(h(d))
    | None => None
    }
  | None => None
  }
| None => None
};

That code is quite messy, even though it's just trying to express some simple logic: if the value is Some(_), do something to it, but if it's None, just return None. Luckily there's a thing called the maybe monad. A category theorist could tell you all kinds of cool properties of monads, but for now, all you need to know is that they make it a lot easier to work with option('a) types.

The following is equivalent to the block of code above, but much cleaner:

let* b = a;
let* c = f(b);
let+ d = g(c);
h(d);

Use let* if the expression below it evaluates to an option('a) type. Use let+ if the expression below it evaluates to a 'a type.

To use this monad syntax, uncomment open Monad_lib.Monad; at the top of the file.

In this project the monad is mostly useful inside matched_arrow_typ (which returns an option) and the various ..._opt lookups on the context, though most of the marking code actually doesn't need it because marking never fails.

Extension Ideas

Once you've completed the core implementation, it's instructive to extend the calculus. Each extension reinforces the recipe of the marked lambda calculus: for every new rule whose premise might fail, add a new mark and a new marking rule.

• Booleans, conditionals, and inconsistent branches (Zhao et al. §2.1.6). Add Bool, tt, ff, and if … then … else …. You will need a BoolLit shape and a new InconsistentBranches mark for the synthesis rule when the two branch types have no meet.

• Products and projections (Zhao et al. §2.1.7). Adds a Prod type, (e, e) pair expressions, π₁/π₂, matched_prod, and two new marks for non-matched products.

• Destructuring let with pattern annotations (Zhao et al. §2.3). The most subtle extension; the "switch type" trick is instructive.

The key insight from both papers is that each extension is guided by the metatheory: the types of the new judgement forms dictate which action rules are needed, and the marking totality theorem tells you exactly where new marks are required.