(fixing-programmatic-tool-calling-with-types . (blog . (coldboot . org)))

λ-Tool makes these four bugs compile-time type errors; the LLM generates λ-Tool code instead of Python, then a type checker verifies the code before any tool runs. If the code is wrong, the LLM gets a type error, fixes it, and resubmits. Nothing executed, so the retry is free.

Here's the same support agent in λ-Tool:

tool lookup_account: String -{Read}-> {id: String, subscription_tier: String,
                                       email: String, last_charge_cents: Int};
tool issue_refund: {account_id: String, amount: Int} -{Write}-> {tx_id: String};
tool send_reply: {to: String, body: String} -{Write}-> Unit;

match exec tool lookup_account "cust_12345" {
  Ok(account) =>
    match exec tool issue_refund {account_id = account.id,
                                   amount = account.last_charge_cents} {
      Ok(refund) =>
        match exec tool send_reply {to = account.email,
                                     body = refund.tx_id} {
          Ok(u) => "refund processed and customer notified",
          Err(e) => "refund succeeded but notification failed"
        },
      Err(e) => "refund failed, customer not refunded"
    },
  Err(e) => "account lookup failed"
}

Every tool declares its input type, output type, and effects (Read, Write). The types are how the checker knows what fields exist. If the LLM writes account.plan, it gets:

Field 'plan' not found in record type
  {id: String, subscription_tier: String, email: String, last_charge_cents: Int}

Every exec returns a Result. The only way to use it is match ... { Ok(x) => ..., Err(e) => ... }. The type checker rejects any program that uses a Result without matching both branches. send_reply is nested inside Ok(refund), so it only runs if the refund succeeded. In the Err branch, refund doesn't exist as a variable, so the LLM can't reference data from a failed call.

There is no retry mechanism. exec tool issue_refund ... evaluates exactly once, and the language has no try/except, no while, no recursion. You can't write a retry loop because the syntax doesn't allow it.

Iteration is bounded: map, filter, fold over finite lists; these require pure callbacks. Trying to call a tool inside map is a type error:

tool charge: {id: Int, amount: Int} -{Write}-> {tx_id: String};

map (fn o: {id: Int, amount: Int} => exec tool charge o)
    [{id = 1, amount = 100}]
(* Effect violation: allowed {} but got {Write} *)

Effectful iteration uses traverse, which short-circuits on the first error and forces Result handling:

match traverse (fn o: {id: Int, amount: Int} =>
    exec tool charge o
  ) [{id = 1, amount = 100}] {
  Ok(receipts) => "done",
  Err(e) => e
}

Unlike Python-based Programmatic Tool Calling implementations, λ-Tool does not require a sandbox because the restrictiveness is the sandbox.