Typed holes

A typed hole is a placeholder for code you have not written yet. In Sakura Lang it is written ?name: a ? immediately followed by an identifier, with no space. A hole is an expression of a fresh type, so a program with holes can be checked before it is finished.

Holes turn "write the whole function and hope it compiles" into small steps, each with precise feedback.

Writing a holeCopy Anchor Link

fn clamp(x: Int, lo: Int, hi: Int) -> Int
  requires ordered: lo <= hi
  ensures bounded: lo <= result && result <= hi
{
  ?body
}

sakura check accepts this program and reports one hole record. sakura build and sakura run reject it with V2050, so a hole cannot reach a build by accident.

The name is for you and for tooling. Use one that says what belongs there: ?body, ?user, ?retry_policy.

? also appears as postfix raise on a Result (r?). The two never clash: ?name with no space before the identifier is always a hole, and ? after an operand is always raise.

What a hole reportsCopy Anchor Link

After solving the enclosing body, sakura check --json emits one hole record per hole, on its own line. The record is exactly this shape (design §12.2):

For the clamp program above, saved as src/main.sakura, the record looks like this, pretty-printed, with hashes shortened:

{
  "schema_version": "1.0",
  "kind": "hole",
  "id": "h:5d0c8e2b1a7f4396",
  "name": "body",
  "snapshot": "sha256:…",
  "span": { "uri": "file:///…/src/main.sakura", "content_hash": "sha256:…",
            "start_byte": 123, "end_byte": 128, "role": "primary" },
  "expected_type": { "render": "Int", "structured": null },
  "allowed_effects": { "render": "{}", "row": { "labels": [], "tail": null } },
  "locals": [
    { "name": "x", "type": { "render": "Int" } },
    { "name": "lo", "type": { "render": "Int" } },
    { "name": "hi", "type": { "render": "Int" } }
  ],
  "candidates": [
    { "expr": "x", "fit": "exact_local" },
    { "expr": "lo", "fit": "exact_local" },
    { "expr": "hi", "fit": "exact_local" },
    { "expr": "Int.min(?a, ?b)", "fit": "function" },
    { "expr": "Int.max(?a, ?b)", "fit": "function" }
  ],
  "contracts_in_scope": ["requires ordered: lo <= hi"]
}

A function candidate carries holes for its own arguments, named after its parameters, so filling the hole with it leaves smaller holes to fill next.

How candidates are rankedCopy Anchor Link

• Exact fits from locals come first.
• Then constructors and functions whose result type unifies with the expected type, such as Int.min or Int.max here. Each is tried in a rollback snapshot, so trying a candidate never changes the inference state.
• Candidates that would need an effect outside the allowed row are filtered out.
• At most 10 candidates are reported.

A hole never affects inference of other bindings beyond its own fresh type variable. The rest of the body, including effects and contracts, is checked normally around it.

Filling a holeCopy Anchor Link

Following the report, an agent fills the hole:

fn clamp(x: Int, lo: Int, hi: Int) -> Int
  requires ordered: lo <= hi
  ensures bounded: lo <= result && result <= hi
{
  if x < lo { lo } else if x > hi { hi } else { x }
}

The ensures clause is checked at runtime on every normal return, in every build mode, including --release. A wrong fill is a D021 defect blamed on clamp, not a silent wrong answer.

Narrower holesCopy Anchor Link

A hole takes its expected type from context. An annotation gives a hole a type when the context does not:

fn greet(name: String) -> Unit ! {Console, Clock} {
  let now: Instant = ?now
  Console.print("hello, {name}; it is {Instant.format_iso(now)}")
}

Here the report expects Instant, and allowed_effects is {Console, Clock}. A function such as Clock.now fits on both counts.

Holes in the MCP serverCopy Anchor Link

The MCP server has a hole_context(snapshot, hole_id) tool. It returns the same record for one hole, which is cheaper than re-checking the project. The M3 acceptance tests in design §14.3 require the language server, after replaying the same edits, to match hole_context byte for byte.

Recommended agent workflowCopy Anchor Link

1. Write every signature the task needs: types, effect rows, Fail<...> unions, and contracts. Bodies are holes.
2. Run sakura check --json. Fix signature-level errors first; these are what a human reviews.
3. Write tests for the behavior the task asks for.
4. Fill holes one at a time, using candidates, locals, and contracts_in_scope. Re-check after each.
5. When no hole records remain, run sakura test --json, then summarize any signature changes for review.

The design does not yet say whether sakura test runs a program that still contains holes. Assume it does not.

NextCopy Anchor Link

Back to the For Agents overview, or see the standard library.