Skip to main content

Function Declarations

Functions are the primary building blocks for organizing code in Sector9. This page covers the basic func syntax, parameters, return types, body forms, and where verification contracts attach.

Basic Syntax​

A function declaration uses the func keyword followed by a name, parameters, return type, and body:

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

The simplest function takes parameters and returns a value:

func add(x : Nat, y : Nat) : Nat {
  x + y
}

Functions with no parameters use empty parentheses:

func zero() : Nat {
  0
}

Parameters​

Typed Parameters​

Every parameter requires a type annotation. Multiple parameters are separated by commas:

func greet(name : Text, age : Nat) : Text {
  // use name and age
}

Single Parameter​

A function with one parameter:

func double(n : Int) : Int {
  n * 2
}

No Parameters​

Functions with no parameters still require parentheses:

func getTimestamp() : Nat {
  0  // placeholder
}

Return Types​

Explicit Return Types​

The return type follows the parameter list after a colon:

func isEven(n : Nat) : Bool {
  n % 2 == 0
}

Unit Return Type​

Functions that return no meaningful value use () (unit):

func logMessage(msg : Text) : () {
  // side effect only
}

Async Return Types​

Public actor methods return async types to support message passing:

public func getData() : async Nat {
  42
}

See async functions and await for actor-message control flow.

Body Forms​

Sector9 supports two body forms: block bodies and expression bodies.

Block Body​

The block body uses curly braces and can contain multiple statements. The last expression is the return value:

func compute(x : Nat, y : Nat) : Nat {
  let sum = x + y;
  let doubled = sum * 2;
  doubled  // returned
}

Expression Body​

For simple functions, use = followed by a single expression:

func square(n : Nat) : Nat = n * n;

This is equivalent to:

func square(n : Nat) : Nat {
  n * n
}

Expression bodies work well for short computations:

func isPositive(x : Int) : Bool = x > 0;
func triple(n : Int) : Int = n * 3;
func maxOf(a : Int, b : Int) : Int = if (a >= b) { a } else { b };

Visibility Modifiers​

Public Functions​

public makes a function accessible from outside the module or actor:

module {
  public func exported() : Nat { 42 }
}

In actors, public functions become callable methods:

persistent actor {
  public func greet() : async Text {
    "Hello"
  }
}

Private Functions​

Functions without public are private by default:

persistent actor {
  // Private - only callable within this actor
  func helper(x : Nat) : Nat {
    x + 1
  }

  public func useHelper(n : Nat) : async Nat {
    helper(n)
  }
}

Use private explicitly for clarity:

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

Functions in Different Contexts​

Module Functions​

Functions in modules are local by default:

module Math {
  public func add(a : Nat, b : Nat) : Nat {
    a + b
  }

  // Private helper
  func clamp(x : Nat, max : Nat) : Nat {
    if (x > max) { max } else { x }
  }
}

Actor Methods​

Public functions in actors become shared methods that return async types:

persistent actor Counter {
  var count : Nat = 0;

  public func increment() : async Nat
    modifies count
    ensures result == count;
  {
    count += 1;
    count
  }
}

Actor methods exposed as calls return async types. State-changing public methods also need accurate modifies clauses, and callers that depend on state preconditions should get entry_requires as well as internal requires.

Query Functions​

Use query for fast actor methods that are intended to be read APIs:

persistent actor {
  var balance : Nat = 0;

  public query func getBalance() : async Nat
    reads balance
    ensures result == balance;
  {
    balance
  }
}

Prefer keeping query functions read-only. If a query body writes actor fields, current verification requires an explicit modifies clause; do not rely on query execution for durable consensus state changes.

Verification Contracts​

Functions can include verification contracts in the signature. See Contracts for full details.

Preconditions​

requires specifies what must be true when the function is called:

func divide(a : Int, b : Int) : Int
  requires b != 0;
{
  a / b
}

Postconditions​

ensures specifies what must be true when the function returns:

func abs(x : Int) : Int
  ensures result >= 0;
{
  if (x >= 0) { x } else { -x }
}

Effect Annotations​

reads and modifies declare which actor fields the function accesses:

persistent actor {
  var total : Nat = 0;

  public func add(amount : Nat) : async Nat
    modifies total
    ensures total == old(total) + amount;
  {
    total += amount;
    total
  }
}

Contract Placement​

Contracts appear after the return type annotation but before the function body:

func name(params) : ReturnType
  requires precondition1;
  requires precondition2;
  ensures postcondition1;
  ensures postcondition2;
{
  // body
}

For actor methods with effects:

public func update(x : Nat) : async ()
  reads field1
  modifies field2
  entry_requires x > 0;
  requires x > 0;
  ensures field2 == old(field2) + x;
{
  // body
}

Common Patterns​

Returning Early with Conditionals​

The last expression is the return value:

func classify(n : Int) : Text {
  if (n < 0) {
    "negative"
  } else if (n == 0) {
    "zero"
  } else {
    "positive"
  }
}

Helper Functions​

Use private functions to break up complex logic:

persistent actor {
  var balance : Nat = 0;

  private func validate(amount : Nat) : Bool {
    amount > 0 and amount <= 10000
  }

  public func deposit(amount : Nat) : async Bool
    modifies balance
    entry_requires amount <= 10000;
    requires amount <= 10000;
  {
    if (validate(amount)) {
      balance += amount;
      true
    } else {
      false
    }
  }
}

Chaining Function Calls​

module {
  public func step1(x : Nat) : Nat { x + 1 }
  public func step2(x : Nat) : Nat { x * 2 }
  public func step3(x : Nat) : Nat { x - 1 }

  public func pipeline(x : Nat) : Nat {
    step3(step2(step1(x)))
  }
}

Common Mistakes​

Missing Async for Actor Methods​

persistent actor {
  // WRONG - public actor methods need async
  public func bad() : Nat {
    42
  }

  // CORRECT
  public func good() : async Nat {
    42
  }
}

Shared Functions Outside Actors​

// WRONG - shared functions must be in actors
shared func badShared() : async () {
  // rejected
}

// CORRECT - inside an actor
persistent actor {
  public func goodShared() : async () {
    // OK
  }
}

Contracts Inside Body​

// WRONG - contracts go in the signature
func bad(x : Nat) : Nat {
  requires x > 0;  // syntax error
  x
}

// CORRECT
func good(x : Nat) : Nat
  requires x > 0
{
  x
}

Missing Modifies Clause​

persistent actor {
  var x : Nat = 0;

  // WRONG - modifying x without declaring it
  public func bad() : async () {
    x := 1;  // verification error
  }

  // CORRECT
  public func good() : async ()
    modifies x
  {
    x := 1;
  }
}

Summary​

  • Functions use func keyword with name, parameters, return type, and body
  • Block bodies use { } and return the last expression
  • Expression bodies use = expression for simple functions
  • public makes functions accessible outside the module or actor
  • Actor methods return async types and can include modifies/reads clauses
  • Contracts (requires, ensures) appear between the signature and body
  • Private helper functions organize complex logic