Ship

Book · Control-flow refinement

Control-flow refinement

Draft

Stable checks narrow values to the cases each branch can actually contain.

On this page · 3 sections

Ship carries facts learned from control flow into type inference. A direct tag check narrows an immutable value in the true branch and removes that tag in the false branch.

type Role = [
  | :owner
  | :admin
  | :user
]

Tag Equality

test✓
  let rolerole: Book.ControlFlowRefinement.Role: Role = :admin;
  if rolerole: Book.ControlFlowRefinement.Role == :admin {
    ✓rolerole: [ :admin ]: :admin;
    expect ✓rolerole: [ :admin ] == :admin;
  } else {
    ✓rolerole: [ :owner | :user ]: [ :owner | :user ];
  }

Reversing the comparison reverses the learned facts. The surrounding scope keeps the declared type after the branches join.

Tag Inequality

test✓
  let rolerole: Book.ControlFlowRefinement.Role: Role = :user;
  if rolerole: Book.ControlFlowRefinement.Role != :admin {
    ✓rolerole: [ :owner | :user ]: [ :owner | :user ];
  } else {
    ✓rolerole: [ :admin ]: :admin;
  }
  ✓rolerole: Book.ControlFlowRefinement.Role: Role;

Short-circuit conditions compose the same facts. || joins the successful alternatives; && intersects everything proven before its right side.

Logical Conditions

test✓
  let rolerole: Book.ControlFlowRefinement.Role: Role = :admin;
  if rolerole: Book.ControlFlowRefinement.Role == :owner || rolerole: Book.ControlFlowRefinement.Role == :admin {
    ✓rolerole: [ :admin | :owner ]: [ :owner | :admin ];
  } else {
    ✓rolerole: [ :user ]: :user;
  }
  if rolerole: Book.ControlFlowRefinement.Role != :user && rolerole: Book.ControlFlowRefinement.Role == :admin {
    ✓rolerole: [ :admin ]: :admin;
    expect ✓rolerole: [ :admin ] == :admin;
  }

Refinements follow stable stored fields as well as local names. Inferred constructors can preserve that proof as a whole refined product; this example starts from a broad function parameter so both branches remain possible.

type Session = {
  role: Role;
  user_id: Int;
}

Stable Fields

test✓
  let sessionsession: Book.ControlFlowRefinement.Session: Session = Session { role = :owner; user_id = 77: Int; };
  if sessionsession: Book.ControlFlowRefinement.Session.rolerole: Book.ControlFlowRefinement.Role == :owner {
    ✓sessionsession: Book.ControlFlowRefinement.Session.rolerole: [ :owner ]: :owner;
    expect ✓sessionsession: Book.ControlFlowRefinement.Session.user_iduser_id: Int == 77: Int;
  } else {
    ✓sessionsession: Book.ControlFlowRefinement.Session.rolerole: [ :admin | :user ]: [ :admin | :user ];
  }

Mutable places keep their declared type. A later write could invalidate a branch fact, so the checker never treats the comparison as lasting evidence.

Mutable Values

test✓
  let mut rolerole: Book.ControlFlowRefinement.Role: Role = :admin;
  if rolerole: Book.ControlFlowRefinement.Role == :admin {
    ✓rolerole: Book.ControlFlowRefinement.Role: Role;
    role := :user;
    ✓rolerole: Book.ControlFlowRefinement.Role: Role;
  }
  expect ✓rolerole: Book.ControlFlowRefinement.Role == :user;

Refutable bindings

if let uses the same pattern checker as match. Bindings and refinements exist only in the successful branch.

If Let

test✓
  let rolerole: Book.ControlFlowRefinement.Role: Role = :admin;
  if let :admin = rolerole: Book.ControlFlowRefinement.Role {
    ✓rolerole: [ :admin ]: :admin;
  } else {
    ✓rolerole: [ :owner | :user ]: [ :owner | :user ];
  }

  let possiblepossible: Option(Int) = SomeSome: fn(Int) -> Option(Int)(4242: Int);
  if let Some(valuevalue: Int) = possiblepossible: Option(Int) {
    ✓valuevalue: Int: Int;
    expect ✓valuevalue: Int == 4242: Int;
  }

let ... else keeps the successful bindings in the surrounding block. Its else branch must leave that block, so no unmatched value reaches the code that follows.

Let Else

test✓
  let requirerequire: fn(possible: Option(Int)) -> Int, exn [ :missing ] = fn(possiblepossible: Option(Int): Option(Int)) {
    let Some(valuevalue: Int) = possiblepossible: Option(Int) else {
      error :missing;
    };
    valuevalue: Int
  };
  ✓requirerequire: fn(possible: Option(Int)) -> Int, exn [ :missing ]: fn(Option(Int)) -> Int, exn [ :missing ];

  let requiredrequired: Int = must requirerequire: fn(possible: Option(Int)) -> Int, exn [ :missing ](Some(77: Int));
  expect ✓requiredrequired: Int == 77: Int;

Database scopes

A database declares each scope once. A table opts in with scope Name;; those scope-owned fields materialize on its stored row without being repeated as ordinary fields. Nested scopes compose every parent field.

database ScopedDb(Sqlite) {
  scope Tenant {
    org_id: Int;
  }

  scope Customer {
    scope Tenant;
    customer_id: Int;
  }

  table Tasks {
    scope Customer;
    id: Int #{ primary = True; };
    title: String;
  }
}

A policy maps database action sets to the finite role rows allowed to cross one scope. The complete role type also records denied roles, so changing the role universe remains visible to the checker.

policy CustomerAccess(Role) for ScopedDb.Customer {
  across {
    set(Read, Insert, Update) requires [ :owner | :admin ];
    set(Delete) requires [ :owner ];
  }
}
let current_role_labelcurrent_role_label: fn() -> String, eff CustomerAccess = fn() {
  if CustomerAccess.rolerole: Book.ControlFlowRefinement.Role == :admin {
    | "admin""admin": String
    | "other""other": String
  }
};

Provided Role

test✓
  ✓current_role_labelcurrent_role_label: fn() -> String, eff CustomerAccess: fn() -> String, eff CustomerAccess;
  provide { CustomerAccess = AdminCustomerAccessAdminCustomerAccess: service CustomerAccess; } {
    expect ✓current_role_labelcurrent_role_label: fn() -> String, eff CustomerAccess() == "admin""admin": String;
  };
let tasks_for_tenanttasks_for_tenant: fn(tx: Database.Transaction(ScopedDb), org_id: Int) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ], eff CustomerAccess([ :admin | :owner ]) = query(org_idorg_id: Int: Int) across Customer {
  from task in ScopedDb.Tasks,
  where task.org_id == org_id,
  select task;
};

Scope-owned fields are visible on selected rows. They are absent from generated insert and update inputs because the active scope supplies them and ordinary mutations cannot move a row between scopes.

Scope Shapes

test✓
  let rowrow: ScopedDb.Tasks.Row: ScopedDb.Tasks.Row = { org_id = 11: Int; customer_id = 22: Int; id = 33: Int; title = "ship""ship": String; };
  ✓rowrow: ScopedDb.Tasks.Row: ScopedDb.Tasks.Row;

  let inputinput: ScopedDb.Tasks.Insert: ScopedDb.Tasks.Insert = { id = 33: Int; title = "ship""ship": String; };
  ✓inputinput: ScopedDb.Tasks.Insert: ScopedDb.Tasks.Insert;

  let patchpatch: ScopedDb.Tasks.Update: ScopedDb.Tasks.Update = { title = "refine""refine": String; };
  ✓patchpatch: ScopedDb.Tasks.Update: ScopedDb.Tasks.Update;
  ✓ScopedDb.Tasks.allall: fn(tx: Database.Transaction(ScopedDb)) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ], eff [ ScopedDb.Customer | ScopedDb.Tenant ]: fn(tx: Database.Transaction(ScopedDb)) -> Vector(ScopedDb.Tasks.Row),
    exn! tx [> :db.rejected(String) ],
    eff [ ScopedDb.Customer | ScopedDb.Tenant ];

Queries bind every active layer. Crossing Customer removes only that layer's predicate obligation; the parent Tenant remains mandatory. Reads, inserts, updates, deletes, joins, and generated table operations all pass through the same structural check. A scope field must equal a declared query parameter, and scoped joins must equate that field on every table.

Scope Queries

test✓
  let tasks_for_customertasks_for_customer: fn(tx: Database.Transaction(ScopedDb), org_id: Int, customer_id: Int) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ] = query(org_idorg_id: Int: Int, customer_idcustomer_id: Int: Int) {
    from task in ScopedDb.Tasks,
    where task.org_id == org_id,
    where task.customer_id == customer_id,
    select task;
  };
  ✓tasks_for_customertasks_for_customer: fn(tx: Database.Transaction(ScopedDb), org_id: Int, customer_id: Int) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ]: fn(
    tx: Database.Transaction(ScopedDb),
    org_id: Int,
    customer_id: Int,
  ) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ];

  ✓tasks_for_tenanttasks_for_tenant: fn(tx: Database.Transaction(ScopedDb), org_id: Int) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ], eff CustomerAccess([ :admin | :owner ]): fn(
    tx: Database.Transaction(ScopedDb),
    org_id: Int,
  ) -> Vector(ScopedDb.Tasks.Row),
    exn! tx [> :db.rejected(String) ],
    eff CustomerAccess([ :owner | :admin ]);

  let delete_for_tenantdelete_for_tenant: fn(tx: Database.Transaction(ScopedDb), id: Int, org_id: Int) -> ScopedDb.Tasks.Row, exn! tx [> :db.rejected(String) ], eff CustomerAccess([ :owner ]) = query(idid: Int: Int, org_idorg_id: Int: Int) across Customer {
    delete from ScopedDb.Tasks
    where Tasks.id == id,
    where Tasks.org_id == org_id,
    returning row;
  };
  ✓delete_for_tenantdelete_for_tenant: fn(tx: Database.Transaction(ScopedDb), id: Int, org_id: Int) -> ScopedDb.Tasks.Row, exn! tx [> :db.rejected(String) ], eff CustomerAccess([ :owner ]): fn(
    tx: Database.Transaction(ScopedDb),
    id: Int,
    org_id: Int,
  ) -> ScopedDb.Tasks.Row, exn! tx [> :db.rejected(String) ], eff CustomerAccess(:owner);

Reading the policy's stable role value narrows the ambient policy context. The successful branch discharges the indexed requirement without threading a role argument through the query function.

Policy Narrowing

test✓
  let admin_routeadmin_route: fn(tx: Database.Transaction(ScopedDb), org_id: Int) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ], eff CustomerAccess = fn(txtx: Database.Transaction(ScopedDb), org_idorg_id: Int: Int) {
    if CustomerAccess.rolerole: Book.ControlFlowRefinement.Role == :admin {
      | tasks_for_tenanttasks_for_tenant: fn(tx: Database.Transaction(ScopedDb), org_id: Int) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ], eff CustomerAccess([ :admin | :owner ])(txtx: Database.Transaction(ScopedDb), org_idorg_id: Int)
      | []
    }
  };
  ✓admin_routeadmin_route: fn(tx: Database.Transaction(ScopedDb), org_id: Int) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ], eff CustomerAccess: fn(
    tx: Database.Transaction(ScopedDb),
    org_id: Int,
  ) -> Vector(ScopedDb.Tasks.Row), exn! tx [> :db.rejected(String) ], eff CustomerAccess;

What refinement will not invent

A mutable field, an ordinary Bool helper, and a let ... else branch that can finish normally stay errors.

crates/ship-types/tests/golden/check-control-flow-refinement/run.t

Mutable bindings are not stable refinement places.

✓
type Role = [
  | :owner
  | :admin
  | :user
]

type Session = {
  role: Role;
  user_id: Int;
}

type MutableSession = {
  mut role: Role;
  user_id: Int;
}

let non_variant: Session with { user_id: :owner; } = Session { role = :owner; user_id = 1; };
let mutable_field: MutableSession with { role: :owner; } = MutableSession { role = :owner; user_id = 1; };
let outside_row: Session with { role: :root; } = Session { role = :owner; user_id = 1; };
let admin_only = (role: :admin) => role;

let unsafe = fn(role: Role) {
  let mut current = role;
  if current == :admin {
    ignore(admin_only(current));
  }
};

$ship-types-test mutable-role.shp
error: only open-variant product fields can be refined
  --> mutable-role.shp:17:33
    |
 17 | let non_variant: Session with { user_id: :owner; } = Session { role = :owner; user_id = 1; };
    |                                 ^^^^^^^ field has type Int

error: mutable product fields cannot carry type refinements
  --> mutable-role.shp:18:42
    |
 18 | let mutable_field: MutableSession with { role: :owner; } = MutableSession { role = :owner; user_id = 1; };
    |                                          ^^^^ this field may change after the value is checked

error: product field refinement exceeds its declared row
  --> mutable-role.shp:19:39
    |
 19 | let outside_row: Session with { role: :root; } = Session { role = :owner; user_id = 1; };
    |                                       ^^^^^ [ :root ] is not contained by Role

error: type mismatch
  --> mutable-role.shp:25:23
    |
 25 |     ignore(admin_only(current));
    |                       ^^^^^^^ expected [ :admin ], found Role

Ordinary Boolean helpers carry no refinement proposition.

✓
type Role = [
  | :owner
  | :admin
  | :user
]

type Session = {
  role: Role;
  user_id: Int;
}

let admin_only = (role: :admin) => role;
let is_admin = (role: Role) => role == :admin;
let owner_only = (session: Session with { role: :owner; }) => session.user_id;

let unsafe = fn(role: Role) {
  if is_admin(role) {
    ignore(admin_only(role));
  }
};

let unsafe_session = fn(session: Session) { owner_only(session) };

let dead_code_is_checked = fn() {
  let session = Session { role = :owner; user_id = 1; };
  if session.role == :owner {
    | session.user_id
    | missing_even_when_unreachable
  }
};

$ship-types-test unchecked-predicate.shp
error: type mismatch
  --> unchecked-predicate.shp:18:23
    |
 18 |     ignore(admin_only(role));
    |                       ^^^^ expected [ :admin ], found Role

error: type mismatch
  --> unchecked-predicate.shp:22:56
    |
 22 | let unsafe_session = fn(session: Session) { owner_only(session) };
    |                                                        ^^^^^^^ expected Session with { role: :owner; }, found Session

error: unknown name `missing_even_when_unreachable`
  --> unchecked-predicate.shp:28:7
    |
 28 |     | missing_even_when_unreachable
    |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not found in this scope

The failure branch of let ... else must leave the enclosing block.

✓
let unsafe = fn(possible: Option(Int)) {
  let Some(value) = possible else {
    print("missing");
  };
  value
};

$ship-types-test completing-let-else.shp
error: `let ... else` must leave the enclosing block
  --> completing-let-else.shp:2:35
    |
  2 |   let Some(value) = possible else {
    |                                   ^ this branch can complete normally
help: finish the `else` branch with `return`, `error`, or another diverging expression