Anonymous Functions

Anonymous functions (also called lambda expressions or function literals) create inline function values without declaring a named function. They are essential for callbacks, quantifiers, and higher-order programming.

Basic Syntax

Anonymous functions use the same func keyword as named functions but omit the function name:

func (param1 : Type1, param2 : Type2) : ReturnType {
  // body
}

Store anonymous functions in variables to use them:

anon-basic.sr9

// Anonymous function stored in a let binding
persistent actor {
  public func applyAnon(n : Nat) : async Nat
    ensures result == n + 1;
  {
    // Anonymous function with a postcondition
    let anonInc = func (m : Nat) : Nat
      ensures result == m + 1;
    {
      m + 1
    };
    anonInc(n)
  };
}

The anonymous function is assigned to anonInc and then called with anonInc(n).

Expression Body Form

For simple functions, use the expression body form with =:

func (x : Nat) : Nat = x * 2

This is equivalent to:

func (x : Nat) : Nat { x * 2 }

Expression bodies are common in specifications:

anon-expression-body.sr9

// Anonymous functions with expression body syntax
persistent actor {
  public func test() : async () {
    ghost {
      // Expression body uses = instead of { }
      let double = pure func (x : Nat) : Nat = x * 2;
      let isZero = pure func (n : Nat) : Bool = n == 0;

      assert double(5) == 10;
      assert isZero(0);
      assert not isZero(1);
    };
  };
}

Pure Anonymous Functions

Mark anonymous functions with pure when they have no side effects. Pure functions:

• Cannot read or modify state
• Cannot call impure functions
• Cannot use await
• Are safe to use in specifications

anon-pure.sr9

// Pure anonymous functions for use in specifications
persistent actor {
  public func checkArray() : async () {
    ghost {
      let data : [Nat] = [1, 2, 3, 4, 5];

      // Pure anonymous function in a quantifier
      assert forall<Nat>(pure func (i : Nat) : Bool =
        i < data.size() ==> data[i] > 0);
    };
  };
}

The pure modifier is required when:

• Using the function in a forall or exists quantifier
• Passing the function as an argument to an uncontracted higher-order parameter (in verification mode)
• Storing the function in an uncontracted higher-order variable

Contracts on Anonymous Functions

Anonymous functions support verification contracts just like named functions:

let anonInc = func (m : Nat) : Nat
  requires m < 1000;
  ensures result == m + 1;
{
  m + 1
};

The requires clause specifies preconditions and ensures specifies postconditions. The result keyword refers to the return value in postconditions.

Closures

Anonymous functions can capture variables from their enclosing scope. This creates a closure:

anon-closure.sr9

// Anonymous functions capturing variables from enclosing scope
persistent actor {
  public func addN(n : Nat, m : Nat) : async Nat
    ensures result == n + m;
  {
    // This function captures `n` from the enclosing scope
    let addToN = pure func (x : Nat) : Nat {
      x + n
    };
    addToN(m)
  };
}

The function addToN captures the parameter n from the enclosing function. When called, it uses both its own parameter x and the captured n.

Closure Semantics

Captured variables are passed as implicit parameters during verification. The verifier:

• Identifies free variables in the function body
• Adds them as extra parameters in the generated code
• Preserves their values at the point of capture

Mutable Function Variables

Store anonymous functions in var bindings to reassign them:

anon-mutable.sr9

// Mutable function variables with pure anonymous functions
persistent actor {
  type Operation = (m : Nat) -> Nat contract {
    ensures result >= m;
  };

  public func useCurrent(n : Nat) : async Nat
    ensures result == n + 1;
  {
    // Store anonymous function in a contract-typed mutable variable.
    var operation : Operation = pure func (m : Nat) : Nat
      ensures result == m * 2;
    {
      m * 2
    };

    // Reassign the operation to a different pure anonymous function.
    operation := pure func (m : Nat) : Nat
      ensures result == m + 1;
    {
      m + 1
    };

    operation(n)
  };
}

When stored in mutable variables, anonymous functions must be pure unless the variable uses a contract-typed function type. This ensures the verifier can reason about which function is called at each call site.

Higher-Order Function Requirements

In verification mode, function values used as higher-order parameters must be pure or carry type contracts. Uncontracted callback types are treated as pure.

Rejected

anon-impure-reject_reject.sr9

// ERROR: Higher-order function values must be pure in verification mode
module {
  // Impure function - no `pure` modifier
  func addOne(x : Nat) : Nat { x + 1 };

  // Function taking a function parameter
  func apply(f : Nat -> Nat, x : Nat) : Nat {
    f(x)
  };

  public func test(n : Nat) : Nat {
    // REJECT: passing impure function to higher-order parameter
    // Error M0360: higher-order function values must be pure
    apply(addOne, n)
  };
}

Correct

module {
  // Add the pure modifier
  pure func addOne(x : Nat) : Nat { x + 1 };

  func apply(f : Nat -> Nat, x : Nat) : Nat {
    f(x)
  };

  public func test(n : Nat) : Nat {
    apply(addOne, n)  // OK - addOne is pure
  };
}

The error M0360: higher-order function values must be pure occurs when passing an impure function to an uncontracted higher-order parameter. Add the pure modifier or use a contract-typed parameter and a contract-bearing value.

Quantifiers with Anonymous Functions

The forall and exists quantifiers take anonymous functions as their predicate:

// All elements are positive
assert forall<Nat>(pure func (i : Nat) : Bool =
  i < arr.size() ==> arr[i] > 0);

// At least one element is zero
assert exists<Nat>(pure func (i : Nat) : Bool =
  i < arr.size() and arr[i] == 0);

For explicit trigger control, use forallWith:

anon-quantifier-trigger.sr9

// Anonymous functions with explicit triggers in quantifiers
persistent actor {
  public func check() : async () {
    ghost {
      let data : [Bool] = [true, true, true];

      // forallWith uses an explicit trigger function
      assert forallWith<Nat>(
        // The predicate
        pure func (i : Nat) : Bool = i < data.size() ==> data[i] == data[i],
        // The trigger - guides SMT instantiation
        [pure func (i : Nat) : Bool = data[i]]
      );
    };
  };
}

The second argument to forallWith is an array of trigger functions that guide SMT solver instantiation. See quantifier triggers for the solver-facing rules.

Function Types

Anonymous functions have function types written with ->:

// Function from Nat to Nat
let f : Nat -> Nat = pure func (x : Nat) : Nat = x + 1;

// Function from two Ints to Bool
let compare : (Int, Int) -> Bool = pure func (a : Int, b : Int) : Bool = a < b;

// Function returning unit
let log : Text -> () = func (msg : Text) : () { };

Function types are structural. Any function matching the signature is compatible.

Common Patterns

Callback Pattern

Anonymous functions work as callbacks:

func withDefault<T>(opt : ?T, default : () -> T) : T {
  switch (opt) {
    case (?v) { v };
    case (null) { default() };
  }
};

// Usage
let result = withDefault<?Nat>(null, pure func () : Nat = 0);

Predicate Pattern

Define predicates inline:

func findFirst(arr : [Nat], pred : Nat -> Bool) : ?Nat {
  // implementation
};

// Usage
let firstEven = findFirst(arr, pure func (n : Nat) : Bool = n % 2 == 0);

Transformation Pattern

Apply transformations to data:

func mapArray(arr : [Nat], f : Nat -> Nat) : [Nat] {
  // implementation
};

// Usage
let doubled = mapArray(arr, pure func (n : Nat) : Nat = n * 2);

Restrictions

Anonymous functions have these restrictions:

Context	Restriction
Higher-order values	Must be pure or contract-typed in verification mode
Quantifiers	Must use pure func
Array access	Do not close over actor arrays or hidden mutable array state; guarded array predicates are supported in quantifiers
State mutation	Not allowed in pure functions
Recursive pure calls	Rejected; use methods/lemmas or trusted helpers

Common Mistakes

Missing Pure Modifier or Contracts

// WRONG - missing pure/contract for higher-order use
let f = func (x : Nat) : Nat { x + 1 };

// CORRECT
let f = pure func (x : Nat) : Nat { x + 1 };

// CORRECT - or use a contract-typed callback
type Step = (x : Nat) -> Nat contract { ensures result == x + 1; };
let f2 : Step = func (x : Nat) : Nat
  ensures result == x + 1;
{ x + 1 };

Accessing State in Pure Function

persistent actor {
  var counter : Nat = 0;

  public func bad() : async () {
    // WRONG - pure functions cannot access fields
    let f = pure func () : Nat { counter };  // Error M0317
  };
}

Non-Expression Quantifier Predicate

// WRONG - quantifier needs expression body
assert forall<Nat>(pure func (i : Nat) : Bool {
  let x = arr[i];
  x > 0
});

// CORRECT - use expression body for simple predicates
assert forall<Nat>(pure func (i : Nat) : Bool =
  i < arr.size() ==> arr[i] > 0);

Related Topics

• Function Declarations - Named function syntax
• Higher-Order Functions - Functions as parameters
• Pure Functions - The pure modifier
• Quantifiers - forall and exists

Summary

• Anonymous functions use func (params) : Type { body } without a name
• Expression body form = expr is concise for simple functions
• Higher-order use in verification mode requires pure or contract-typed callbacks
• Closures capture variables from the enclosing scope
• Anonymous functions support full verification contracts
• Quantifiers use pure func predicates with expression body syntax
• Function types use arrow notation: Nat -> Bool, (Int, Int) -> Int