Higher-Order Functions

Higher-order functions take other functions as parameters or return functions as results. They enable abstractions like map, filter, and fold patterns, but in verification mode every function value must be pure or have a contract type.

Function Types

Function types use arrow notation (->) to describe the parameter and return types:

// Single parameter: ParamType -> ReturnType
let f : Int -> Int = pure func (x : Int) : Int { x + 1 };

// Multiple parameters: (Type1, Type2) -> ReturnType
let compare : (Int, Int) -> Bool = pure func (a : Int, b : Int) : Bool { a < b };

// No parameters: () -> ReturnType
let getZero : () -> Nat = pure func () : Nat { 0 };

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

Type Aliases

Create type aliases for common function signatures:

type UnaryOp = Int -> Int;
type Predicate = Nat -> Bool;
type BinaryOp = (Int, Int) -> Int;

Type aliases make higher-order function signatures more readable:

func apply(f : UnaryOp, x : Int) : Int { f(x) }

Passing Functions as Arguments

Functions can be passed as arguments to other functions. The receiving function specifies the expected function type:

higher-order-basic.sr9

// Higher-order function that takes a function parameter
module MathOps {
  public pure func double(x : Int) : Int { x * 2 };
  public pure func triple(x : Int) : Int { x * 3 };
};

persistent actor {
  // Higher-order function: takes a function as parameter
  func applyOp(f : Int -> Int, x : Int) : Int {
    f(x)
  };

  public func testDouble() : async Int
    ensures result == 10;
  {
    applyOp(MathOps.double, 5)
  };

  public func testTriple() : async Int
    ensures result == 15;
  {
    applyOp(MathOps.triple, 5)
  };
}

The applyOp function takes any Int -> Int function and applies it to a value. The verifier proves that calling with double returns 10 and calling with triple returns 15.

Function Composition

Higher-order functions enable composition patterns where functions combine to form new behaviors:

higher-order-compose.sr9

// Function composition and apply-twice patterns
persistent actor {
  type UnaryOp = Int -> Int;

  // Compose two functions: f(g(x))
  pure func compose(f : UnaryOp, g : UnaryOp, x : Int) : Int {
    f(g(x))
  };

  // Apply a function twice: f(f(x))
  pure func applyTwice(f : UnaryOp, x : Int) : Int {
    f(f(x))
  };

  pure func addOne(x : Int) : Int { x + 1 };
  pure func double(x : Int) : Int { x * 2 };

  public func testCompose() : async Int
    ensures result == 12;
  {
    // double(addOne(5)) = double(6) = 12
    compose(double, addOne, 5)
  };

  public func testApplyTwice() : async Int
    ensures result == 2;
  {
    // addOne(addOne(0)) = 2
    applyTwice(addOne, 0)
  };
}

The compose function chains two functions: f(g(x)). The applyTwice function applies the same function twice: f(f(x)).

Storing Functions in Variables

Functions can be stored in variables and called later:

higher-order-alias.sr9

// Storing functions in variables
module Math {
  public pure func increment(x : Nat) : Nat
    ensures result == x + 1;
  { x + 1 };
};

module {
  public func useAlias(n : Nat) : Nat
    ensures result == n + 1;
  {
    // Store module function in a local variable.
    let inc = Math.increment;
    inc(n)
  };
}

When storing a function in a variable, the function's contracts are preserved. Calling inc(n) verifies against the original increment postcondition.

Conditional Function Selection

Select between functions at runtime based on conditions:

higher-order-conditional.sr9

// Conditional function selection
module A {
  public func getValue() : Int { 10 }
};

module B {
  public func getValue() : Int { 20 }
};

persistent actor {
  var useA : Bool = true;

  public func selectAndCall() : async Int
    modifies useA
    ensures useA ==> result == 10;
    ensures not useA ==> result == 20;
  {
    // Select function based on condition
    let f = if (useA) A.getValue else B.getValue;
    f()
  }
}

The verifier reasons about both branches. If useA is true, f is A.getValue which returns 10. Otherwise, f is B.getValue which returns 20. The postconditions capture this conditional relationship.

Anonymous Functions as Arguments

Pass anonymous functions directly without naming them:

higher-order-anon.sr9

// Passing anonymous functions as arguments
persistent actor {
  pure func applyTwice(f : Int -> Int, x : Int) : Int {
    f(f(x))
  };

  public func testAnonymous() : async Int
    ensures result == 9;
  {
    // Pass an anonymous pure function
    applyTwice(pure func (x : Int) : Int { x + 2 }, 5)
  };
}

Anonymous functions must be pure or flow through a contract-typed parameter in verification mode. See Anonymous Functions for more on lambda syntax.

Callback Requirements

In verification mode, functions passed as higher-order values must be pure or carry a type contract. If the parameter type has no contract, the verifier treats it as pure, so the passed value must be pure (or have an effect-free contract).

Rejected

higher-order-impure_reject.sr9

// REJECT: Higher-order function values must be pure
module {
  // Impure function - missing `pure` modifier
  func addOne(x : Nat) : Nat { x + 1 };

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

  public func test(n : Nat) : Nat {
    // 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 callback. Add pure, or use a contract-typed parameter and a contract-bearing value.

Why Purity Matters

The verifier can inline local pure function bodies to reason about their behavior. When you write applyOp(double, 5) in the same verified unit, the verifier can use the function definition. Across source imports, runtime pure/spec helpers are contract-only by default unless they are explicitly written as inline pure func. For contract-typed callbacks, the verifier uses the contract instead of the body.

Verification Contracts

Higher-order functions support full verification contracts. The verifier tracks function behavior through the abstraction:

module MathOps {
  public pure func square(x : Int) : Int
    ensures result == x * x;
  { x * x };
};

persistent actor {
  func applyAndDouble(f : Int -> Int, x : Int) : Int
    ensures result == 2 * f(x);
  {
    2 * f(x)
  };

  public func test() : async Int
    ensures result == 50;
  {
    // applyAndDouble(square, 5) = 2 * square(5) = 2 * 25 = 50
    applyAndDouble(MathOps.square, 5)
  }
}

The verifier chains the contracts: applyAndDouble guarantees 2 * f(x), and square guarantees x * x, so the result is 2 * 5 * 5 = 50.

Common Patterns

Apply Pattern

Apply a function to a value:

pure func apply<T, U>(f : T -> U, x : T) : U { f(x) }

Map Pattern

Transform each element of a collection:

func mapArray(arr : [Nat], f : Nat -> Nat) : [Nat] {
  // apply f to each element
}

Filter Pattern

Select elements matching a predicate:

func filterArray(arr : [Nat], pred : Nat -> Bool) : [Nat] {
  // keep elements where pred returns true
}

Fold Pattern

Reduce a collection to a single value:

func foldArray(arr : [Nat], init : Nat, combine : (Nat, Nat) -> Nat) : Nat {
  // combine elements starting from init
}

Factory Pattern

Return a function configured with captured values:

module {
  public func makeAdder(n : Int) : Int -> Int {
    pure func (x : Int) : Int { x + n }
  }
}

Restrictions

Higher-order functions have these restrictions in verification mode:

Restriction	Error Code	Description
Must be pure or contracted	M0360	Function values must be pure or carry type contracts (requires/ensures, and reads/modifies if they touch state). Uncontracted callback types are treated as pure.
No recursion in pure	-	Pure functions used as values cannot be recursive
No state access	M0317	Pure functions cannot access actor/module fields
Escaping $Self closures	M0360	Functions that may touch actor state must have full contracts before they can escape
No collections	M0242	Function types cannot be elements of Set, Map, Seq, Multiset

Functions in Collections

Function types cannot be stored in specification collections:

// WRONG - function types not allowed in Set
ghost let funcs : Set<Nat -> Nat> = Set.empty();  // Error M0242

// Use a wrapper or alternative design

Common Mistakes

Missing Pure Modifier or Contracts

// WRONG - missing pure/contract
func double(x : Int) : Int { x * 2 };
apply(double, 5);  // Error M0360

// CORRECT - mark pure
pure func double(x : Int) : Int { x * 2 };
apply(double, 5);  // OK

// CORRECT - or use a contract type (both sides need contracts)
type Step = (x : Int) -> Int contract { ensures result == x * 2; };
func doubleC(x : Int) : Int
  ensures result == x * 2;
{ x * 2 };
let f : Step = doubleC;
apply(f, 5);  // OK

Calling Parameter in Pure Context

// OK - allowed when the parameter is pure or lemma
pure func applyPure(f : Int -> Int, x : Int) : Int {
  f(x)
}

// WRONG - passing an impure function value
func double(x : Int) : Int { x * 2 };
applyPure(double, 5);  // Error M0360

// CORRECT
pure func doublePure(x : Int) : Int { x * 2 };
applyPure(doublePure, 5);  // OK

State Access in Passed Function

persistent actor {
  var counter : Nat = 0;

  // WRONG - captures state
  let f = pure func () : Nat { counter };  // Error M0317

  // CORRECT - pass state as parameter
  let f = pure func (c : Nat) : Nat { c + 1 };
}

Related Topics

• Function Declarations - Named function syntax
• Anonymous Functions - Lambda expressions
• Pure Functions - The pure modifier
• Generic Functions - Type parameters
• First-Class Modules - Modules as values

Summary

• Function types use arrow notation: Nat -> Bool, (Int, Int) -> Int
• Type aliases improve readability: type UnaryOp = Int -> Int
• Functions can be passed as arguments to higher-order functions
• Functions can be stored in variables and selected conditionally
• Functions passed as values must be pure or carry type contracts in verification mode
• The verifier preserves function contracts through higher-order abstractions
• Composition patterns like compose and applyTwice enable powerful abstractions