Generic Functions

Generic functions use type parameters to write code that works with any type. Instead of writing separate functions for Int, Bool, and Nat, you write one function parameterized by <T>. The verifier specializes each used instantiation, so contracts stay attached to the concrete version that is called.

Basic Syntax

Type parameters appear in angle brackets after the function name:

func identity<T>(x : T) : T { x }

The <T> declares a type parameter named T. Inside the function, T acts as a placeholder for any concrete type. When called, the type parameter is replaced with an actual type.

Multiple Type Parameters

Functions can have multiple type parameters separated by commas:

func swap<A, B>(a : A, b : B) : (B, A) { (b, a) }
func fst<X, Y>(pair : (X, Y)) : X { pair.0 }

Use descriptive names when the meaning is clear: <Key, Value> for maps, <Input, Output> for transformations.

Generic Functions with Contracts

Generic functions support full verification contracts. The type parameters can appear in the function signature and contracts:

generic-basic.sr9

// Generic functions with type parameters

module GenericBasic {
  // Generic identity function
  public pure func identity<T>(x : T) : T
    ensures result == x;
  {
    x
  };

  // Generic swap function with two type parameters
  public pure func swap<A, B>(a : A, b : B) : (B, A)
    ensures result.0 == b;
    ensures result.1 == a;
  {
    (b, a)
  };

  // Generic first projection
  public pure func fst<X, Y>(pair : (X, Y)) : X
    ensures result == pair.0;
  {
    pair.0
  };

  // Generic second projection
  public pure func snd<X, Y>(pair : (X, Y)) : Y
    ensures result == pair.1;
  {
    pair.1
  };
}

The verifier checks each concrete instantiation that appears in the verified program. When you call identity<Int>(42), the Int specialization carries the same contract, so the verifier knows result == x for that call. See function contracts for contract-bearing function types.

Calling Generic Functions

Explicit Type Arguments

Provide type arguments in angle brackets at the call site:

generic-instantiation.sr9

// Calling generic functions with explicit type arguments

module GenericInstantiation {
  public pure func identity<T>(x : T) : T { x };
  public pure func fst<A, B>(pair : (A, B)) : A { pair.0 };
  public pure func snd<A, B>(pair : (A, B)) : B { pair.1 };
};

persistent actor {
  // Explicit type argument: identity<Int>
  public func testIdentityInt() : async Int
    ensures result == 42;
  {
    GenericInstantiation.identity<Int>(42)
  };

  // Explicit type argument: identity<Bool>
  public func testIdentityBool() : async Bool
    ensures result == true;
  {
    GenericInstantiation.identity<Bool>(true)
  };

  // Multiple type arguments: fst<Int, Bool>
  public func testFst() : async Int
    ensures result == 1;
  {
    GenericInstantiation.fst<Int, Bool>((1, true))
  };

  // Nested generic calls
  public func testNested() : async Int
    ensures result == 99;
  {
    GenericInstantiation.identity<Int>(
      GenericInstantiation.fst<Int, Int>((99, 0))
    )
  };
}

Explicit type arguments are required when:

• The type cannot be inferred from the arguments
• You want to be explicit about the intended type
• Multiple valid types could apply

Type Inference

The compiler can often infer type arguments from the context:

let x : Int = identity(42);        // T inferred as Int
let pair = swap(1, true);          // A inferred as Nat, B as Bool
let first : Bool = fst((true, 5)); // X inferred as Bool, Y as Nat

When inference succeeds, explicit type arguments are optional. The compiler warns about redundant type instantiation (M0223) when types could be inferred.

Nested Generic Calls

Generic functions can be nested and composed:

// Compose two generic calls
identity<Int>(fst<Int, Bool>((42, true)))

// Chain operations
snd<Bool, Int>(swap<Int, Bool>(1, true))

Each call is independently instantiated with its own type arguments.

Generic Higher-Order Functions

Generic functions combine naturally with higher-order patterns:

generic-higher-order.sr9

// Generic higher-order functions

module GenericHigherOrder {
  // Apply a function to a value
  public func apply<T, U>(f : T -> U, x : T) : U
    ensures result == f(x);
  {
    f(x)
  };
};

persistent actor {
  pure func double(n : Nat) : Nat
    ensures result == n * 2;
  {
    n * 2
  };

  public func testApply() : async Nat
    ensures result == 10;
  {
    GenericHigherOrder.apply<Nat, Nat>(double, 5)
  };

  public func testApplyTwice(n : Nat) : async Nat
    ensures result == n + 2;
  {
    GenericHigherOrder.apply<Nat, Nat>(
      pure func (m : Nat) : Nat
        ensures result == m + 1;
      {
        m + 1
      },
      GenericHigherOrder.apply<Nat, Nat>(
        pure func (m : Nat) : Nat
          ensures result == m + 1;
        {
          m + 1
        },
        n
      )
    )
  };
}

The apply<T, U> function works with any function type T -> U. When called with apply<Nat, Nat>(double, 5), the type parameters become concrete: T = Nat, U = Nat.

Common Higher-Order Patterns

// Map: transform each element
func map<A, B>(f : A -> B, xs : [A]) : [B] { ... }

// Filter: keep matching elements
func filter<T>(pred : T -> Bool, xs : [T]) : [T] { ... }

// Fold: reduce to single value
func fold<T, R>(f : (R, T) -> R, init : R, xs : [T]) : R { ... }

These patterns require the function argument to be pure or contract-typed in verification mode. See Higher-Order Functions for callback requirements.

Generic Type Definitions

Define generic types with type parameters:

generic-type-def.sr9

// Generic type definitions

module GenericTypeDef {
  // Generic option type
  public type Maybe<T> = { #none; #just : T };

  // Create a Maybe with a value
  public func just<T>(x : T) : Maybe<T> {
    #just(x)
  };

  // Check if Maybe is none
  public pure func isNone<T>(m : Maybe<T>) : Bool {
    switch (m) {
      case (#none) true;
      case (#just(_)) false;
    }
  };

  // Get value or default
  public func getOrElse<T>(m : Maybe<T>, default : T) : T {
    switch (m) {
      case (#none) default;
      case (#just(v)) v;
    }
  };
};

persistent actor {
  public func testMaybe() : async Nat {
    let m1 : GenericTypeDef.Maybe<Nat> = GenericTypeDef.just<Nat>(42);
    let m2 : GenericTypeDef.Maybe<Nat> = #none;
    let v1 = GenericTypeDef.getOrElse<Nat>(m1, 0);
    let v2 = GenericTypeDef.getOrElse<Nat>(m2, 99);
    v1 + v2
  };

  public func testIsNone() : async Bool {
    let m : GenericTypeDef.Maybe<Int> = #none;
    GenericTypeDef.isNone<Int>(m)
  };
}

Generic types follow the same syntax: type Name<T> = .... Functions operating on generic types use the same type parameters.

Common Generic Type Patterns

// Optional value
type Option<T> = ?T;

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

// Pair/Tuple alias
type Pair<A, B> = (A, B);

// Wrapper
type Box<T> = { value : T };

Verification and Monomorphization

Sector9 uses monomorphization for verification: each generic call with different type arguments creates a specialized version. This is why generic proofs are precise but can increase verifier work if a helper is instantiated at many unrelated types. When you call:

identity<Int>(42);
identity<Bool>(true);

The verifier creates two separate functions internally: one for Int, one for Bool. Each is verified independently with its concrete types.

How Contracts Work

1. Type parameters in contracts are replaced with concrete types
2. Each used instantiation is verified as a separate function
3. The verifier proves properties for each concrete type combination that appears in the program

This means ensures result == x is checked on the Int specialization used by identity<Int>(42).

Verification Output

In Viper output (--viper), generic functions appear as specialized versions:

$spec$identity$Int(...)
$spec$identity$Bool(...)
$spec$fst$Int$Bool(...)

The type arguments are encoded in the function name for the verification backend.

Restrictions

Generic functions have several restrictions in Sector9.

No Generic Actor Classes

Actor classes cannot have type parameters:

Rejected

generic-actor-class_reject.sr9

// Generic actor classes are not supported

// This is rejected with error M0140:
// "actor classes with type parameters are not supported yet"

actor class Container<T>() {
  var item : ?T = null;

  public func set(x : T) : async () {
    item := ?x;
  };

  public func get() : async ?T {
    item
  };
}

Workaround

// Use a concrete actor with generic helper module
module Container {
  public type Box<T> = { var value : ?T };

  public func make<T>() : Box<T> { { var value = null } };
  public func set<T>(box : Box<T>, x : T) { box.value := ?x };
  public func get<T>(box : Box<T>) : ?T { box.value };
}

Error M0140: "actor classes with type parameters are not supported yet"

No Generic Shared Functions

Public actor methods cannot have user-defined type parameters:

Rejected

generic-shared_reject.sr9

// Generic shared functions are not supported

// These are rejected with error M0180:
// "shared function has unexpected type parameters"

persistent actor {
  // WRONG - generic shared function
  public func badShared<T>(x : T) : async T {
    x
  };
}

Workaround

persistent actor {
  // Use private generic helper
  private func helper<T>(x : T) : T { x };

  // Public methods with concrete types
  public func processInt(x : Int) : async Int {
    helper<Int>(x)
  };

  public func processBool(x : Bool) : async Bool {
    helper<Bool>(x)
  };
}

Error M0180: "shared function has unexpected type parameters"

Only the implicit system capability parameter is allowed on shared functions.

Other Restrictions

Restriction	Error	Description
Duplicate type parameters	M0044	func f<T, T>() - same name twice
Wrong number of type arguments	M0045	List<Int, Bool> when List<T> expects one
Type argument violates bound	M0046	When type doesn't satisfy constraint
Cyclic type bounds	M0043	<T <: U, U <: T> - circular bounds
Outer scope reference	M0137	Inner type referencing outer type parameter

Type Parameter Bounds

Type parameters can have bounds constraining what types are valid:

// T must be a subtype of Comparable
func sort<T <: Comparable>(items : [T]) : [T] { ... }

Bounds ensure the type has required operations. Without a bound, the type parameter accepts any type.

Bound Inference Issues

When bounds involve other type parameters, explicit instantiation may be required:

// Error: bound involves unresolved type parameter
func f<T <: U, U>(x : T) : U { ... }

// Fix: provide explicit type arguments
f<Int, Int>(42)

Error: "type parameter has a bound involving another type parameter. Please provide an explicit instantiation."

Common Mistakes

Missing Type Arguments When Required

// WRONG - type cannot be inferred
let result = identity(someUnknownValue);  // Error

// CORRECT - provide explicit type
let result = identity<Int>(42);

Generic Recursion

Polymorphic recursion through generic functions is not supported:

// WRONG - recursive call with different type arguments
func bad<T>(x : T) : T {
  bad<(T, T)>((x, x)).0  // Not supported
}

Functions in Generic Collections

Function types cannot be elements of spec collections:

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

// WRONG - functions not allowed in Map values
ghost let handlers : Map<Text, Int -> Int> = Map.empty();  // Error M0242

Related Topics

• Function Declarations - Basic function syntax
• Higher-Order Functions - Functions as values
• Anonymous Functions - Lambda expressions
• Generic Type Definitions - Parameterized types
• Pure Functions - Side-effect free functions

Summary

• Type parameters use angle brackets: func name<T>(x : T) : T
• Multiple parameters: func swap<A, B>(a : A, b : B) : (B, A)
• Explicit instantiation: identity<Int>(42)
• Type inference works when types can be determined from context
• Generic functions support full verification contracts
• The verifier monomorphizes generics: each type combination is verified separately
• Actor classes and shared functions cannot have user-defined type parameters
• Generic types define parameterized data structures: type Maybe<T> = { #none; #just : T }