Variants

Variants are tagged unions that represent values from a fixed set of alternatives. Each alternative has a unique tag (starting with #) and can optionally carry a payload. Variants are the standard way to model enumerations, result types, and state machines in Sector9.

Creating Variants

Define variant types by listing tags with optional payload types:

variant-basic.sr9

// Basic variant types and construction
persistent actor {
  // Define a variant type with three cases
  type Status = { #pending; #approved; #rejected };

  // Variant with payloads of different types
  type Result = { #ok : Nat; #err : Text };

  // Variant with tuple payload
  type Color = { #red; #blue : Nat; #green : (Nat, Nat) };

  var status : Status = #pending;

  // Construct variants with their tag
  public func setPending() : async ()
    modifies status
    ensures status == #pending;
  {
    status := #pending
  };

  public func setApproved() : async ()
    modifies status
    ensures status == #approved;
  {
    status := #approved
  };

  // Construct payloaded variant
  public func makeOk(n : Nat) : async Result
    ensures result == #ok(n);
  {
    #ok(n)
  };

  public func makeErr(msg : Text) : async Result
    ensures result == #err(msg);
  {
    #err(msg)
  };
}

Key points:

• Tags start with # followed by an identifier: #pending, #approved, #rejected
• Tags without payloads: #pending (just the tag itself)
• Tags with payloads: #ok : Nat (tag carries a value)
• Tuple payloads: #green : (Nat, Nat) (tag carries multiple values)
• Construct variants by writing the tag with its payload: #ok(42), #err("failed")

Pattern Matching with switch

Use switch expressions to match on variant tags and extract payloads:

variant-switch.sr9

// Pattern matching on variants with switch
persistent actor {
  type Status = { #pending; #approved; #rejected };
  type Result = { #ok : Nat; #err : Text };

  // Switch on simple variant
  public func statusCode(s : Status) : async Nat
    ensures switch (s) {
      case (#pending) result == 0;
      case (#approved) result == 1;
      case (#rejected) result == 2;
    };
  {
    switch (s) {
      case (#pending) 0;
      case (#approved) 1;
      case (#rejected) 2;
    }
  };

  // Extract payload with pattern binding
  public func getValue(r : Result) : async Nat
    ensures switch (r) {
      case (#ok n) result == n;
      case (#err _) result == 0;
    };
  {
    switch (r) {
      case (#ok n) n;
      case (#err _) 0;
    }
  };

  // Wildcard matches remaining cases
  public func isApproved(s : Status) : async Bool
    ensures s == #approved ==> result == true;
    ensures s != #approved ==> result == false;
  {
    switch (s) {
      case (#approved) true;
      case (_) false;
    }
  };
}

Pattern matching rules:

• Each case matches a tag: case (#pending) ...
• Bind payload to a variable: case (#ok n) ... binds n to the payload
• Use _ to ignore a payload: case (#err _) ...
• Wildcard case (_) matches all remaining cases
• All cases must be covered (exhaustiveness is checked at compile time)

Payloads

Variants can carry different types of data:

variant-payload.sr9

// Variants with different payload types
persistent actor {
  // No payload
  type Empty = { #none };

  // Single value payload
  type MaybeInt = { #nothing; #just : Int };

  // Tuple payload
  type Point = { #origin; #coords : (Int, Int) };

  // Multiple variants with different payloads
  type Shape = { #circle : Nat; #rect : (Nat, Nat); #point };

  // Pattern match to extract tuple payload
  public func area(s : Shape) : async Nat
    ensures switch (s) {
      case (#circle r) result == r * r;
      case (#rect (w, h)) result == w * h;
      case (#point) result == 0;
    };
  {
    switch (s) {
      case (#circle r) r * r;
      case (#rect (w, h)) w * h;
      case (#point) 0;
    }
  };

  // Extract single payload
  public func getInt(m : MaybeInt) : async Int
    ensures switch (m) {
      case (#nothing) result == 0;
      case (#just n) result == n;
    };
  {
    switch (m) {
      case (#nothing) 0;
      case (#just n) n;
    }
  };
}

Payload types:

Pattern	Syntax	Example
No payload	#tag	#pending, #rejected
Single value	#tag : Type	#ok : Nat, #err : Text
Tuple	#tag : (T1, T2)	#coords : (Int, Int)

When matching tuple payloads, destructure directly: case (#coords (x, y)).

Pure Functions with Variants

Pure functions work naturally with variants for reusable predicates:

variant-pure.sr9

// Pure functions with variants
persistent actor {
  type Result = { #ok : Nat; #err : Text };
  type Status = { #pending; #approved : Nat; #rejected };

  // Pure function to check variant case
  pure func isOk(r : Result) : Bool {
    switch (r) {
      case (#ok _) true;
      case (#err _) false;
    }
  };

  // Pure function to extract payload with default
  pure func getOrDefault(r : Result, default : Nat) : Nat {
    switch (r) {
      case (#ok n) n;
      case (#err _) default;
    }
  };

  // Pure function to check specific case
  pure func isPending(s : Status) : Bool {
    switch (s) {
      case (#pending) true;
      case (_) false;
    }
  };

  // Use pure functions in postconditions
  public func checkResult(r : Result) : async Bool
    ensures result == isOk(r);
  {
    isOk(r)
  };

  public func unwrapOr(r : Result, default : Nat) : async Nat
    ensures result == getOrDefault(r, default);
  {
    getOrDefault(r, default)
  };
}

Pure variant helpers like isOk and getOrDefault can appear directly in ensures clauses, making contracts more readable.

Variants as State

Variants are ideal for modeling state machines:

variant-state.sr9

// Variants as actor state
persistent actor {
  type Status = { #pending; #approved : Nat; #rejected };

  var status : Status = #pending;

  // State transitions with preconditions
  public func approve(id : Nat) : async ()
    modifies status
    entry_requires status == #pending;
    requires status == #pending;
    ensures status == #approved(id);
  {
    status := #approved(id)
  };

  public func reject() : async ()
    modifies status
    entry_requires status == #pending;
    requires status == #pending;
    ensures status == #rejected;
  {
    status := #rejected
  };

  public func reset() : async ()
    modifies status
    ensures status == #pending;
  {
    status := #pending
  };

  // Query current state
  public func getStatus() : async Status
    reads status
    ensures result == status;
  {
    status
  };

  // Check specific state
  public func isPending() : async Bool
    reads status
    ensures result == (status == #pending);
  {
    switch (status) {
      case (#pending) true;
      case (_) false;
    }
  };
}

State machine patterns:

• Store variant in actor field: var status : Status = #pending
• Use entry_requires and requires to enforce valid public transitions: entry_requires status == #pending
• Use ensures to specify the new state: ensures status == #approved(id)
• Payload captures transition data: #approved(id) remembers the approval ID

Contracts with Variants

Specify behavior per variant case using switch in postconditions:

public func describe(s : Status) : async Text
  ensures switch (s) {
    case (#pending) result == "waiting";
    case (#approved n) result == "approved";
    case (#rejected) result == "denied";
  };
{
  switch (s) {
    case (#pending) "waiting";
    case (#approved _) "approved";
    case (#rejected) "denied";
  }
}

For result-style variants, use implication (==>) for cleaner contracts:

public func divide(a : Nat, b : Nat) : async Result
  ensures b == 0 ==> result == #err("division by zero");
  ensures b != 0 ==> result == #ok(a / b);

Verification Behavior

The verifier handles variants by generating:

1. Discriminator functions: Check which tag a value has (isResult$ok(r))
2. Getter functions: Extract payloads (getResult$ok$0(r))
3. Exhaustiveness axioms: Ensure exactly one tag is active
4. Exclusivity axioms: Tags are mutually exclusive

This means postconditions like switch (r) { case (#ok n) ... } work correctly: the verifier knows that if isResult$ok(r) is true, then isResult$err(r) is false.

Common Patterns

Result Type

Model success/failure with payloads:

type Result<T, E> = { #ok : T; #err : E };

public func safeDivide(a : Nat, b : Nat) : async Result<Nat, Text>
  ensures b == 0 ==> switch (result) { case (#err _) true; case _ false }
  ensures b != 0 ==> result == #ok(a / b);
{
  if (b == 0) { #err("division by zero") } else { #ok(a / b) }
};

Option Alternative

While ?T is the idiomatic option type, variants offer explicit naming:

type MaybeInt = { #nothing; #just : Int };

State Machines

Model protocols with restricted transitions:

type Loan = { #applied : Nat; #approved : (Nat, Nat); #denied };

public func approve(rate : Nat) : async ()
  modifies loan
  entry_requires switch (loan) { case (#applied _) true; case _ false };
  requires switch (loan) { case (#applied _) true; case _ false };
  ensures switch (old(loan)) {
    case (#applied amt) loan == #approved(amt, rate);
    case _ false
  };
{
  switch (loan) {
    case (#applied amt) { loan := #approved(amt, rate) };
    case _ { assert false }
  }
}

Restrictions

Exhaustiveness Required

All variant cases must be covered. Missing cases cause a compile error. See pattern matching for the general exhaustiveness rules:

switch (status) {
  case (#pending) 0;
  case (#approved) 1;
  // ERROR M0145: pattern does not cover value #rejected
}

No Or-Patterns

Combining cases with or is not supported:

// NOT SUPPORTED
case (#pending or #rejected) 0;

Use wildcards or list cases separately:

case (#pending) 0;
case (#rejected) 0;
case (#approved) 1;

Function Payloads

Function types in variant payloads must be pure or contract-typed in verification mode:

type Callback = { #none; #some : (Nat -> Nat) };  // Function must be pure or contract-typed

Mutable Records in Payloads

Mutable records can appear in variant payloads, but have ownership implications:

type Cell = { var x : Int };
type MaybeCell = { #none; #some : Cell };

switch (v) {
  case (#some c) {
    c.x := 10;  // Mutation allowed after pattern match
  };
  case (#none) {};
};

The pattern match introduces a local alias to the mutable record. Ownership and aliasing are still checked by the verifier; avoid keeping multiple mutable aliases live when you need to write through one of them.

Error Detection

The verifier catches incorrect postconditions:

variant-wrong_unsat.sr9

// Wrong postcondition: verifier will reject
// Expected: verification failure (_unsat suffix)
persistent actor {
  type Color = { #red; #blue : Nat };

  public func colorCode(c : Color) : async Nat
    ensures switch (c) {
      case (#red) result == 5;  // WRONG: actual returns 4
      case (#blue x) result == x;
    };
  {
    switch (c) {
      case (#red) 4;  // Returns 4, not 5
      case (#blue x) x;
    }
  };
}

The verifier rejects this because #red returns 4, not 5. Verification failures appear as unsat results.

Variant vs Option

Feature	Variant	Option (?T)
Syntax	{ #none; #some : T }	?T
Construction	#some(value)	?value
Empty	#none	null
Custom names	Yes	No
Multiple empties	Yes	No

Use ?T for simple nullable values. Use variants when you need custom tag names or multiple "empty" states.

Variant vs Record

Feature	Variant	Record
Purpose	One of several alternatives	Collection of named fields
Contains	One tag with optional payload	All fields simultaneously
Access	Pattern matching	Dot notation
Example	#ok(42) or #err("fail")	{ x = 1; y = 2 }

Variants model "or" (alternatives). Records model "and" (all fields together).

Error Codes

Code	Meaning
M0116	Variant pattern cannot consume expected type
M0145	Pattern does not cover all variant cases
M0146	Pattern is never matched (unreachable)
M0360	Higher-order function in variant must be pure or contract-typed

Summary

• Variants represent one of several tagged alternatives
• Tags start with #: #pending, #ok : Nat, #coords : (Int, Int)
• Use switch to pattern match and extract payloads
• Bind payloads to variables: case (#ok n) ...
• All cases must be covered (exhaustiveness checked at compile time)
• Pure functions with variants work in postconditions
• Variants model state machines with requires/ensures on transitions
• Use implication (==>) for result-style contracts
• The verifier generates discriminator and getter functions automatically
• Prefer ?T for simple nullability, variants for richer alternatives