Tuples

Tuples are fixed-length ordered collections where each element can have a different type. They are accessed by position using numeric indices like .0, .1, .2. They are useful for small return bundles, but records are clearer when field names carry domain meaning.

Creating Tuples

Create tuples by listing values in parentheses, separated by commas:

tuple-basic.sr9

// Basic tuple creation and access
persistent actor {
  public func example() : async () {
    // Creating tuples
    let pair : (Nat, Text) = (42, "hello");
    let triple = (1, 2, 3);  // Type inferred as (Nat, Nat, Nat)
    let unit : () = ();       // Empty tuple (unit)

    // Accessing elements by position
    assert pair.0 == 42;
    assert pair.1 == "hello";
    assert triple.0 == 1;
    assert triple.1 == 2;
    assert triple.2 == 3;
  };
}

Key points:

• Tuple types are written as (T1, T2, T3, ...) listing each element type
• Type inference works for tuples: let pair = (1, 2) infers (Nat, Nat)
• The empty tuple () is the unit type, representing "no value"
• Access elements with .0, .1, .2, etc. (zero-indexed)

Destructuring with Patterns

Use pattern matching to extract tuple elements into separate variables:

tuple-destructure.sr9

// Tuple destructuring with pattern matching
persistent actor {
  public func example() : async () {
    let pair = (10, 20);

    // Destructure both elements
    let (x, y) = pair;
    assert x == 10;
    assert y == 20;

    // Ignore elements with underscore
    let (first, _) = pair;
    assert first == 10;

    let (_, second) = pair;
    assert second == 20;

    // Destructure triples
    let triple = (1, 2, 3);
    let (a, _, c) = triple;
    assert a == 1;
    assert c == 3;
  };
}

The underscore _ ignores elements you do not need. This keeps code clean when only some elements matter.

Nested Tuples

Tuples can contain other tuples, creating nested structures:

tuple-nested.sr9

// Nested tuples
persistent actor {
  public func example() : async () {
    // Tuple containing a tuple
    let nested : (Nat, (Text, Bool)) = (1, ("hello", true));

    // Access with chained projection
    assert nested.0 == 1;
    assert nested.1.0 == "hello";
    assert nested.1.1 == true;

    // Destructure nested tuples
    let (n, (s, b)) = nested;
    assert n == 1;
    assert s == "hello";
    assert b == true;

    // Multiple nesting levels
    let deep = ((1, 2), (3, 4));
    assert deep.0.0 == 1;
    assert deep.0.1 == 2;
    assert deep.1.0 == 3;
    assert deep.1.1 == 4;
  };
}

Chain projections to access deeply nested elements: outer.1.0 gets the first element of the inner tuple.

Functions with Tuples

Tuples work naturally as function parameters and return types:

tuple-functions.sr9

// Tuples in function parameters and returns
persistent actor {
  // Function returning a tuple
  public func swap(a : Int, b : Int) : async (Int, Int)
    ensures result.0 == b;
    ensures result.1 == a;
  {
    (b, a)
  };

  // Function taking a tuple parameter
  public func sum(pair : (Int, Int)) : async Int
    ensures result == pair.0 + pair.1;
  {
    pair.0 + pair.1
  };

  // Function returning multiple values
  public func minMax(a : Int, b : Int) : async (Int, Int)
    ensures result.0 <= result.1;
    ensures (result.0 == a and result.1 == b) or (result.0 == b and result.1 == a);
  {
    if (a <= b) { (a, b) } else { (b, a) }
  };

  // Using the returned tuple
  public func test() : async () {
    let swapped = await swap(1, 2);
    assert swapped.0 == 2;
    assert swapped.1 == 1;

    let (min, max) = await minMax(5, 3);
    assert min == 3;
    assert max == 5;
  };
}

In postconditions, use result.0, result.1 to specify constraints on each element of a returned tuple.

Pure Functions with Tuples

Pure functions can create, transform, and project tuples. They work well in verification contracts:

tuple-pure.sr9

// Pure functions with tuples
persistent actor {
  // Pure function that creates a tuple
  pure func makePair(a : Int, b : Int) : (Int, Int) {
    (a, b)
  };

  // Pure function that swaps tuple elements
  pure func swapPair(pair : (Int, Int)) : (Int, Int) {
    (pair.1, pair.0)
  };

  // Pure function that extracts first element
  pure func fst(pair : (Int, Int)) : Int {
    pair.0
  };

  // Pure function that extracts second element
  pure func snd(pair : (Int, Int)) : Int {
    pair.1
  };

  // Using pure functions in contracts
  public func example(x : Int, y : Int) : async (Int, Int)
    ensures fst(result) == y;
    ensures snd(result) == x;
    ensures result == swapPair(makePair(x, y));
  {
    swapPair(makePair(x, y))
  };
}

Pure tuple helpers like fst and snd can appear directly in ensures clauses.

Tuple vs Record

Feature	Tuple	Record
Access	By position (.0, .1)	By name (.fieldName)
Type syntax	(Nat, Text)	{ age : Nat; name : Text }
Self-documenting	No	Yes
Best for	Small, temporary groupings	Structured data with meaning

Use tuples for quick groupings like swapping values or returning multiple values. Use records when field names add clarity.

Tuple vs Multiple Parameters

Functions taking multiple parameters differ from functions taking a tuple:

// Two separate parameters
func add(a : Nat, b : Nat) : Nat { a + b };

// One tuple parameter
func addPair(pair : (Nat, Nat)) : Nat { pair.0 + pair.1 };

Calling conventions:

• add(1, 2) passes two arguments
• addPair((1, 2)) passes one tuple
• addPair(1, 2) also works due to implicit tuple construction

Pattern Restrictions in Verification

In verification contexts, tuple patterns in let bindings must be irrefutable (cannot fail to match):

tuple-refutable_reject.sr9

// Refutable tuple patterns are rejected
persistent actor {
  public func example() : async () {
    let pair : (Nat, Nat) = (1, 2);

    // ERROR: Literal patterns are refutable
    let (0, y) = pair;  // Rejected: 0 is a literal pattern

    // The pattern (0, y) could fail if pair.0 != 0
    // Verification requires irrefutable patterns in let bindings
  };
}

Pattern Type	Example	Allowed?
Variable binding	let (x, y) = pair	Yes
Wildcard	let (_, y) = pair	Yes
Nested variable	let ((a, b), c) = nested	Yes
Literal	let (0, y) = pair	No
Option	let (?x, y) = pair	No
Variant	let (#Tag, y) = pair	No

Refutable patterns belong in switch expressions, not plain let bindings during verification.

Tuples in State

Tuples can be stored in actor fields:

persistent actor {
  var coords : (Int, Int) = (0, 0);

  public func getX() : async Int
    reads coords
    ensures result == coords.0;
  {
    coords.0
  };

  public func setCoords(x : Int, y : Int) : async ()
    modifies coords
    ensures coords.0 == x;
    ensures coords.1 == y;
  {
    coords := (x, y);
  };
}

The reads and modifies clauses apply to the entire tuple field, not individual elements.

Tuples with Mutable Records

Tuples can contain mutable records:

type Cell = { var value : Int };

public func example() : async () {
  let pair : (Cell, Int) = ({ var value = 3 }, 9);
  assert pair.0.value == 3;
  assert pair.1 == 9;

  // Mutate the record inside the tuple
  pair.0.value := 10;
  assert pair.0.value == 10;
};

The tuple binding itself is immutable (you cannot assign a new tuple to pair), but mutable record fields inside it can still change. When mutable payloads escape into actor state or collections, the permission model and mutable record rules become the important part of the proof.

Common Mistakes

Projection Out of Bounds

let pair = (1, 2);
pair.2;  // ERROR M0066: tuple projection 2 is out of bounds

Tuple indices are zero-based. A pair has .0 and .1 only.

Projection on Non-Tuple

let x = 42;
x.0;  // ERROR M0067: expected tuple type

Numeric projection only works on tuples.

Wrong Pattern Arity

let pair = (1, 2);
let (a, b, c) = pair;  // ERROR M0118: pattern has 3 components but type has 2

The number of pattern elements must match the tuple size.

Mutable Tuple Bindings

var (a, b) = (1, 2);  // ERROR: patterns not allowed with var

Use separate var declarations instead:

var a = 1;
var b = 2;

Error Codes

Code	Meaning
M0066	Tuple projection index out of bounds
M0067	Projection on non-tuple expression
M0112	Tuple pattern on non-tuple type
M0118	Tuple pattern size mismatch

Summary

• Tuples are fixed-length, ordered collections with positional access
• Create with (a, b, c), access with .0, .1, .2
• Destructure with let (x, y) = tuple
• Use wildcards _ to ignore elements
• In postconditions, access tuple results with result.0, result.1
• Pattern matching in let must use irrefutable patterns (no literals or options)
• Prefer records when field names improve readability
• Tuples are immutable values, but can contain mutable record fields