Refined products

Draft

Immutable open-variant fields stay precise without losing their nominal product.

On this page · 4 sections

A product constructor already proves which open-variant tag it stores. Without an expected type, Ship preserves that proof while keeping the product's nominal identity.

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

type AccountState = [
  | :active
  | :invited
  | :suspended
]

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

let known_ownerknown_owner: Book.RefinedProducts.Session with { role: :owner; state: :active; } = Session { role = :owner; state = :active; user_id = 77: Int; };

Inferred Refinements

test✓

  ✓known_ownerknown_owner: Book.RefinedProducts.Session with { role: :owner; state: :active; }: Session with { role: :owner; state: :active; };

  let sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; } = Session { role = :owner; state = :active; user_id = 77: Int; };
  ✓sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; }: Session with { role: :owner; state: :active; };
  ✓sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; }.rolerole: [ :owner ]: :owner;
  ✓sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; }.user_iduser_id: Int: Int;
  expect ✓sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; }.user_iduser_id: Int == 77: Int;

  let aliasalias: Book.RefinedProducts.Session with { role: :owner; state: :active; } = sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; };
  ✓aliasalias: Book.RefinedProducts.Session with { role: :owner; state: :active; }: Session with { role: :owner; state: :active; };

Payload tags retain their payload type as part of the field refinement.

type WorkState = [
  | :waiting
  | :done(String)
]

type Work = {
  state: WorkState;
}

Payload Refinements

test✓

  let workwork: Book.RefinedProducts.Work with { state: :done(String); } = Work { state = :done("shipped""shipped": String); };
  ✓workwork: Book.RefinedProducts.Work with { state: :done(String); }: Work with { state: :done(String); };
  expect ✓workwork: Book.RefinedProducts.Work with { state: :done(String); }.statestate: [ :done(String) ] == :done("shipped""shipped": String);

Precision boundaries

An explicit expected type deliberately widens the value. This applies to bindings, function results, collection elements, and every other expected type boundary.

Explicit Widening

test✓

  let sessionsession: Book.RefinedProducts.Session: Session = Session { role = :owner; state = :active; user_id = 77: Int; };
  ✓sessionsession: Book.RefinedProducts.Session: Session;
  ✓sessionsession: Book.RefinedProducts.Session.rolerole: Book.RefinedProducts.Role: Role;

  let widenedwidened: Book.RefinedProducts.Session = known_ownerknown_owner: Book.RefinedProducts.Session with { role: :owner; state: :active; } :> Session;
  ✓widenedwidened: Book.RefinedProducts.Session: Session;

let broad_sessionbroad_session: fn() -> Book.RefinedProducts.Session = fn() -> Session {
  Session { role = :owner; state = :active; user_id = 77: Int; }
};

Expected Results

test✓

  ✓broad_sessionbroad_session: fn() -> Book.RefinedProducts.Session: fn() -> Session;

  let sessionssessions: Vector(Book.RefinedProducts.Session): Vector(Session) = [Session { role = :owner; state = :active; user_id = 77: Int; }];
  ✓sessionssessions: Vector(Book.RefinedProducts.Session): Vector(Session);

Encoding uses the nominal product's generated behavior and keeps the same runtime representation. Decoding returns the broad boundary type; ordinary control flow establishes any narrower proof afterward.

Boundary Behavior

test✓

  let encodedencoded: Bytes = must Json.encodeencode: pure fn('a: Encode)(value: Book.RefinedProducts.Session with { role: :owner; state: :active; }) -> Bytes, exn [ :encode(Wire.EncodeError) ](known_ownerknown_owner: Book.RefinedProducts.Session with { role: :owner; state: :active; });
  ✓encodedencoded: Bytes: Bytes;

  let decodeddecoded: Book.RefinedProducts.Session = must Json.decodedecode: pure fn('target: Decode)(body: Bytes, target: Struct(Book.RefinedProducts.Session), ~max_depth: Int = 128) -> Book.RefinedProducts.Session, exn [ :decode(Wire.DecodeError) ](encodedencoded: Bytes, Session);
  ✓decodeddecoded: Book.RefinedProducts.Session: Session;

Refined contracts

A refined product can cross a function boundary when the signature asks for that proof. A broad Session must establish it through control flow.

let owner_user_idowner_user_id: fn(session: Book.RefinedProducts.Session with { role: :owner; }) -> Int = fn(sessionsession: Book.RefinedProducts.Session with { role: :owner; }: Session with { role: :owner; }) {
  sessionsession: Book.RefinedProducts.Session with { role: :owner; }.user_iduser_id: Int
};

Refined Parameters

test✓

  let ownerowner: Book.RefinedProducts.Session with { role: :owner; state: :active; } = Session { role = :owner; state = :active; user_id = 77: Int; };
  expect ✓owner_user_idowner_user_id: fn(session: Book.RefinedProducts.Session with { role: :owner; }) -> Int(ownerowner: Book.RefinedProducts.Session with { role: :owner; state: :active; }) == 77: Int;

  let from_sessionfrom_session: fn(session: Book.RefinedProducts.Session) -> Int = fn(sessionsession: Book.RefinedProducts.Session: Session) {
    if sessionsession: Book.RefinedProducts.Session.rolerole: Book.RefinedProducts.Role == :owner {
      | owner_user_idowner_user_id: fn(session: Book.RefinedProducts.Session with { role: :owner; }) -> Int(sessionsession: Book.RefinedProducts.Session with { role: :owner; })
      | 00: Int
    }
  };
  ✓from_sessionfrom_session: fn(session: Book.RefinedProducts.Session) -> Int: fn(Session) -> Int;
  expect ✓from_sessionfrom_session: fn(session: Book.RefinedProducts.Session) -> Int(ownerowner: Book.RefinedProducts.Session with { role: :owner; state: :active; }) == 77: Int;

The whole value receives the branch refinement, not only its projected field. The opposite branch carries the complementary finite row.

Whole Value Narrowing

test✓

  let sessionsession: Book.RefinedProducts.Session: Session = Session { role = :owner; state = :active; user_id = 77: Int; };
  if sessionsession: Book.RefinedProducts.Session.rolerole: Book.RefinedProducts.Role == :owner {
    ✓sessionsession: Book.RefinedProducts.Session with { role: :owner; }: Session with { role: :owner; };
    expect ✓owner_user_idowner_user_id: fn(session: Book.RefinedProducts.Session with { role: :owner; }) -> Int(sessionsession: Book.RefinedProducts.Session with { role: :owner; }) == 77: Int;
  } else {
    ✓sessionsession: Book.RefinedProducts.Session with { role: [ :admin | :user ]; }: Session with { role: [ :admin | :user ]; };
  }

Updates and joins

Immutable record updates replace the proof for an updated field and retain independent field refinements.

Updated Refinements

test✓

  let ownerowner: Book.RefinedProducts.Session with { role: :owner; state: :active; } = Session { role = :owner; state = :active; user_id = 77: Int; };
  let adminadmin: Book.RefinedProducts.Session with { role: :admin; state: :active; } = { ownerowner: Book.RefinedProducts.Session with { role: :owner; state: :active; } with role = :admin; };
  ✓adminadmin: Book.RefinedProducts.Session with { role: :admin; state: :active; }: Session with { role: :admin; state: :active; };
  expect ✓adminadmin: Book.RefinedProducts.Session with { role: :admin; state: :active; }.rolerole: [ :admin ] == :admin;

Joining two precise branches unions their open rows. If either branch is a broad Session, the join is broad.

Branch Joins

test✓

  let choosechoose: fn(owner: Bool) -> Book.RefinedProducts.Session with { role: [ :admin | :owner ]; state: :active; } = fn(ownerowner: Bool: Bool) {
    if ownerowner: Bool {
      | Session { role = :owner; state = :active; user_id = 77: Int; }
      | Session { role = :admin; state = :active; user_id = 88: Int; }
    }
  };
  ✓choosechoose: fn(owner: Bool) -> Book.RefinedProducts.Session with { role: [ :admin | :owner ]; state: :active; }: fn(Bool) -> Session with { role: [ :owner | :admin ]; state: :active; };

  let choose_broadchoose_broad: fn(owner: Bool, other: Book.RefinedProducts.Session) -> Book.RefinedProducts.Session = fn(ownerowner: Bool: Bool, otherother: Book.RefinedProducts.Session: Session) {
    if ownerowner: Bool {
      | Session { role = :owner; state = :active; user_id = 77: Int; }
      | otherother: Book.RefinedProducts.Session
    }
  };
  ✓choose_broadchoose_broad: fn(owner: Bool, other: Book.RefinedProducts.Session) -> Book.RefinedProducts.Session: fn(Bool, Session) -> Session;

  let sessionssessions: Vector(Book.RefinedProducts.Session with { role: [ :admin | :owner ]; state: :active; }) = [
    Session { role = :owner; state = :active; user_id = 77: Int; },
    Session { role = :admin; state = :active; user_id = 88: Int; },
  ];
  ✓sessionssessions: Vector(Book.RefinedProducts.Session with { role: [ :admin | :owner ]; state: :active; }): Vector(Session with { role: [ :owner | :admin ]; state: :active; });

Unreachable branches

A known refinement makes the contradictory branch unreachable. Ship still checks that source for ordinary mistakes, but its errors and effects do not widen the reachable function.

effect service UnreachableEffect {
  touch: pure fn!() -> Unit;
}

let exact_controlexact_control: pure fn!() -> Unit: pure fn!() -> Unit = fn() {
  let sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; } = Session { role = :owner; state = :active; user_id = 77: Int; };
  if sessionsession: Book.RefinedProducts.Session with { role: :owner; state: :active; }.rolerole: [ :owner ] == :owner {
    | ()(): Unit
    | UnreachableEffect.touchtouch: fn!() -> Unit, eff UnreachableEffect()
  }
};

Unreachable Effects

test✓

  exact_controlexact_control: pure fn!() -> Unit();