Jacquard
Core 0.3.0 · research prototype agents → SKILL.md · llms.txt

Tour 2 of 2

One policy, three worlds

The first tour asked what a change can touch. This one asks what it will do in situations you cannot reproduce on your machine. It follows the release-risk case study that ships with Jacquard 0.3.0. Once the release is installed you can run it yourself: 

sh ~/.local/share/jacquard/demos/case-studies/release-risk/run.sh

The review question

Suppose a model hands you a change to a release policy. Before reading any body, you want to know what the change can reach. In most languages the answer lives somewhere in everything the code calls, and nothing checks whichever answer you settle on. In Jacquard it is part of the type.

1. Declare the boundary

The policy depends on three readings from production. Instead of calling a monitoring client, it performs operations of a Telemetry effect. multi allows a handler to resume these operations more than once, which the probability model below relies on. 

multi effect Telemetry where {
  inventory-health : () -> Health
  payments-health : () -> Health
  error-spike? : () -> Bool
}

-- A pure, reviewable release policy.
decide : (Health, Health, Bool) ->{} Decision
decide(inventory, payments, spike) =
  match (inventory, payments, spike) {
    | (_, Down, _) -> Hold("payments-down")
    | (_, Degraded, _) -> Canary(5)
    | (Down, Healthy, _) -> Hold("inventory-down")
    | (Degraded, Healthy, _) -> Canary(10)
    | (Healthy, Healthy, True) -> Canary(5)
    | (Healthy, Healthy, False) -> Ship
  }

release-assessment : () ->{Telemetry} Assessment
release-assessment() = {
  let inventory = inventory-health()
  let payments = payments-health()
  let spike = error-spike?()
  Assessment(inventory, payments, spike, decide(inventory, payments, spike))
}

decide is pure: its row {} is empty. release-assessment may perform Telemetry and nothing else. The checker infers both rows; a signature that left out an effect would be a type error. Here is what it reports for the whole file: 

release-assessment : () ->{Telemetry} Assessment
with-snapshot : forall a | e. (Health, Health, Bool, () ->{Telemetry | e} a) ->{| e} a
with-risk-model : forall a | e. (() ->{Telemetry | e} a) ->{Dist | e} a
conditioned-release-risk : () ->{Dist} Decision

In the handler types, with-snapshot discharges Telemetry and adds nothing, while with-risk-model discharges Telemetry and introduces Dist, the effect of making a weighted choice.

2. Write the worlds as handlers

-- Deterministic interpretation: production snapshot, fixture, or replay.
with-snapshot(inventory, payments, spike, body) =
  handle body() {
    | return value -> value
    | inventory-health() resume continue -> continue(inventory)
    | payments-health() resume continue -> continue(payments)
    | error-spike?() resume continue -> continue(spike)
  }

health-dist(healthy-weight, degraded-weight, down-weight) =
  Categorical([
    MkPair(Healthy, healthy-weight),
    MkPair(Degraded, degraded-weight),
    MkPair(Down, down-weight)
  ])

-- Probabilistic interpretation: uncertain telemetry becomes Dist choices.
with-risk-model(body) =
  handle body() {
    | return value -> value
    | inventory-health() resume continue ->
        continue(`op:sample`(health-dist(0.85, 0.10, 0.05)))
    | payments-health() resume continue ->
        continue(`op:sample`(health-dist(0.90, 0.08, 0.02)))
    | error-spike?() resume continue ->
        continue(`op:sample`(Bernoulli(0.06)))
  }

A handler intercepts each operation and decides how the rest of the program continues. The snapshot handler resumes once with a fixed value, which is ordinary dependency injection. The risk model resumes with a sample from a distribution; under exact enumeration, the rest of the program runs once for each possible value.

That is the difference from dependency injection: an injected dependency is a handler that resumes exactly once. A handler may also abort the rest of the program, or resume it many times to explore every outcome, which is what makes the exact model and the exhaustive check below ordinary library code.

3. Run it against today's readings

Inventory healthy, payments degraded, no error spike:

assessment(healthy, degraded, false, canary(5))

4. Ask what probably happened

A reviewer approving a policy wants to know more than what it decides today: when something goes wrong, which decisions could it have made, and how likely was each? A probability model answers that from the same code.

The model then observes that a checkout failed and asks which release decision the world was most likely in. Enumeration visits every combination of readings, weighs each by its prior and by how likely a failure was there, and normalises: 

0.305077  canary(5)
0.295394  hold("inventory-down")
0.184621  canary(10)
0.155903  hold("payments-down")
0.059005  ship

These are exact probabilities for a finite model, not a sampled estimate. For larger models, jac infer lw runs the same program under seeded likelihood weighting, which gives an approximate answer.

5. Check every world, not a sample

The demo runs the suite with Warp, Jacquard's test framework, twice. First the property “a down service is never approved to ship” is sampled 100 times with a fixed seed: 

PASS release-risk-suite/release risk/the concrete snapshot chooses a five-percent canary (1 check)
PASS release-risk-suite/release risk/the conditioned posterior is normalized with five decisions (2 checks)
PASS release-risk-suite/release risk/a down service is never approved to ship (prop: 100 cases, seed 42)
3 passed, 0 failed, 0 skipped, 0 refused

Because the generators are finite, --exhaustive checks all 18 combinations instead: 

PASS release-risk-suite/release risk/the concrete snapshot chooses a five-percent canary (1 check)
PASS release-risk-suite/release risk/the conditioned posterior is normalized with five decisions (2 checks)
PASS release-risk-suite/release risk/a down service is never approved to ship (verified exhaustively (18 cases))
3 passed, 0 failed, 0 skipped, 0 refused

“Exhaustive” is bounded by the declared generators: three health values for each service and two for the spike. It is a complete check of that space, not a proof about the real world.

What you did not have to write

Next