First-Class Modules

Modules are first-class values in Sector9: you can pass them as function parameters, return them from functions, store them in variables, and select between them conditionally. Verification follows the module type and member contracts through those indirections without turning the module into an actor boundary.

Overview

First-class modules enable powerful abstraction patterns:

• Functor pattern - functions that accept any module with a required interface
• Module factories - functions that create and return configured modules
• Conditional selection - choosing between modules at runtime
• Module aliasing - storing modules in local variables for convenience
• Higher-order patterns - passing module functions to other functions

These patterns are supported by verification when the module surface is runtime-legal and the functions exposed through it are pure or contract-typed where needed. Contracts on module-typed parameters are checked, and postconditions are preserved through module indirection.

Modules as Function Parameters

Functions can accept module-typed parameters. The caller passes any module that satisfies the required interface:

first-class-functor.sr9

// Module as function parameter (functor pattern)
// A function that accepts any module with the required interface

module Calculator {
  // Accept any module with inc and dec functions
  public func compute(M : module { inc : Nat -> Nat; dec : Nat -> Nat }) : Nat
    requires M.inc(0) == 1;    // Module must satisfy this
    ensures result == 1;
  {
    let x = M.inc(0);
    let _ = M.dec(5);
    x
  };
};

// A module that satisfies the required interface
module Ops {
  public func inc(n : Nat) : Nat
    ensures result == n + 1;
  { n + 1 };

  public func dec(n : Nat) : Nat
    ensures result == n - 1;
  { n - 1 };
};

The Calculator.compute function accepts any module with inc and dec methods. The requires clauses constrain what the passed module must satisfy. Any module matching the interface and satisfying the preconditions can be passed.

Key points:

• The module type specifies required members: module { inc : Nat -> Nat; dec : Nat -> Nat }
• Contracts can reference module members: requires M.inc(0) == 1
• The verifier checks that the passed module satisfies the preconditions

Returning Modules from Functions

Functions can return modules. This enables the factory pattern where functions create configured modules:

first-class-factory.sr9

// Module factory - function returning a module
// The returned module captures values from the enclosing scope

module Scaler {
  // Returns a module with an apply method that scales by the given factor
  public func make(scale : Nat) : module { apply : Nat -> Nat } {
    module Inner {
      public func apply(n : Nat) : Nat
        ensures result == n * scale;
      {
        n * scale
      };
    };
    Inner
  };
};

The make function returns a module with an apply method. The returned module captures the scale parameter from the enclosing scope, creating a closure. The postcondition ensures result == n * scale references the captured value.

Key points:

• Return type specifies the module interface: module { apply : Nat -> Nat }
• The inner module can capture values from the outer scope
• Contracts on the returned module are verified

Conditional Module Selection

You can select between modules at runtime using conditional expressions:

first-class-conditional.sr9

// Conditional module selection
// Choose between modules at runtime based on a condition

module Fast {
  public func process(n : Nat) : Nat
    ensures result == n + 1;
  { n + 1 };
};

module Slow {
  public func process(n : Nat) : Nat
    ensures result == n + 1;
  { n + 1 };
};

// Type alias for the common interface
type Processor = module { process : Nat -> Nat };

module Selector {
  public func pick(useFast : Bool) : Processor {
    if (useFast) Fast else Slow
  };
};

Both branches of the conditional must return modules with compatible types. The type alias Processor defines the common interface.

Key points:

• Both branches must satisfy the same module type
• Type aliases make common module types reusable
• The verifier reasons about both possible modules

Module Aliasing

Modules can be stored in local variables, creating aliases:

first-class-alias.sr9

// Module aliasing - storing modules in local variables

module Original {
  public func getValue() : Nat
    ensures result == 42;
  { 42 };
};

module User {
  public func useAlias() : Nat
    ensures result == 42;
  {
    // Create a local alias for the module
    let Alias = Original;
    // Use the alias like the original
    Alias.getValue()
  };
};

The local binding let Alias = Original creates an alias. Calling Alias.getValue() is equivalent to calling Original.getValue(). This is useful for:

• Shortening long module paths
• Re-exporting modules from other modules
• Creating local names for imported modules

Higher-Order Functions with Module Functions

Module functions can be passed as first-class values to higher-order functions:

first-class-higher-order.sr9

// Using module functions with higher-order functions
// Module functions can be passed as first-class values

module MathOps {
  // Pure functions can be passed as values
  public pure func double(x : Int) : Int { x * 2 };
  public pure func triple(x : Int) : Int { x * 3 };
};

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

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

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

The apply function accepts any function of type Int -> Int. Module functions like MathOps.double can be passed directly. For local pure functions, the verifier can use the body; for contract-typed or imported functions, it uses the declared contract unless an imported helper is explicitly inline pure.

Callback Requirements

Functions passed as first-class values must be pure or contract-typed. This ensures the verifier can reason about their behavior symbolically:

Rejected

first-class-impure_reject.sr9

// ERROR: Function values must be pure
// Non-pure functions cannot be passed as first-class values

module Ops {
  // Missing 'pure' modifier - this function has implicit effects
  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)  // Error M0360: higher-order function values must be pure
  };
};

Correct

module Ops {
  // Add 'pure' modifier - now can be passed as value
  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)  // Works: addOne is pure
  };
};

Error M0360: higher-order function values must be pure or contract-typed (add 'pure' or a type contract)

Pure function values cannot:

• Modify state (no var mutations)
• Call await or perform async operations
• Close over actor fields or hidden mutable array state
• Use assert, trap, or runtime:assert

Verification Behavior

When modules are passed as values, the verifier:

1. Checks preconditions - Verifies that the passed module satisfies requires clauses
2. Assumes postconditions - Uses the module's method postconditions for reasoning
3. Maintains parametric verification - Proofs work for any module satisfying the contract
4. Preserves contracts through indirection - Calling M.func() uses M.func's postcondition

The verification system treats module values as abstract references with known method contracts. This enables modular verification without needing the module's implementation at every call site, but it also means the interface must state the facts callers need.

Common Patterns

Dependency Injection

Pass different module implementations to change behavior:

type Logger = module { log : Text -> () };

module ConsoleLogger {
  public func log(msg : Text) : () { /* print to console */ };
};

module FileLogger {
  public func log(msg : Text) : () { /* write to file */ };
};

module App {
  public func run(L : Logger) : () {
    L.log("Starting...");
  };
};

Strategy Pattern

Select algorithms through module parameters:

type Sorter = module { sort : [Nat] -> [Nat] };

module QuickSort {
  public func sort(arr : [Nat]) : [Nat] { /* ... */ };
};

module MergeSort {
  public func sort(arr : [Nat]) : [Nat] { /* ... */ };
};

module Processor {
  public func process(S : Sorter, data : [Nat]) : [Nat] {
    S.sort(data)
  };
};

Module Re-Export

Re-export modules under different names:

import Internal "./internal";

module Public {
  // Re-export as public API
  public let Utils = Internal.Helpers;
  public type Config = Internal.Helpers.Config;
};

Restrictions

First-class modules have some limitations:

Pattern	Supported	Notes
Module as parameter	Yes	Any module matching the type
Module as return value	Yes	Factory pattern
Module in local variable	Yes	Aliasing
Conditional selection	Yes	Both branches same type
Module in collections	No	Cannot use in Set, Map, Seq
Module-level mutable state	No	Modules cannot have var fields
Recursive module functions	No	Pure functions must be non-recursive

Module-level state is not allowed:

// REJECTED - modules cannot have mutable state
module Wrong {
  var counter : Nat = 0;  // Error M0014
  public func bump() : Nat { counter += 1; counter };
};

Modules are stateless containers. Use actors for stateful components.

Modules cannot be collection elements:

// REJECTED - modules not allowed in collections
ghost {
  let m : Set<module { f : () -> Nat }> = Set.empty();  // Error M0242
}

Related Topics

• Module definitions for creating modules
• Module types for structural typing
• Higher-order functions for functions as values
• Pure functions for the pure modifier
• Spec collections for why module values are not collection elements

Summary

• Modules are first-class values: pass, return, store, select
• Module parameters use structural typing based on required members
• Contracts on module parameters are verified with requires clauses
• Module factories return configured modules that capture scope values
• Conditional selection requires both branches to match the same type
• Function values extracted from modules must be pure or contract-typed
• Modules cannot have mutable state or appear in spec collections