Skip to main content

Module Types

Module types describe the required structure of a module using structural typing. They are useful for parameterized proof code, dependency injection, and first-class module APIs, but they are still subject to Sector9's runtime/proof boundary checks.

Overview​

A module type specifies what functions, types, and values a module must provide. Unlike nominal typing where types are distinguished by name, module types use structural typing: any module with matching members is compatible, regardless of its name or where it was defined.

This enables powerful patterns:

  • Functor parameters - functions that accept any module with the required interface
  • Module factories - functions that return modules matching a type specification
  • Dependency injection - passing different implementations without changing code

Basic Syntax​

A module type is written using the module { ... } syntax, listing the required members and their types:

module { memberName : memberType; ... }

For example, a module type requiring an add function:

module { add : (Nat, Nat) -> Nat }

Module Type Parameters​

Functions can accept module-typed parameters. Any module with compatible members can be passed:

module-type-basic.sr9
// Basic module type syntax
// A module type describes the required structure of a module

// A function that accepts any module with an "add" method
module Calculator {
  public func compute(M : module { add : (Nat, Nat) -> Nat }) : Nat
    ensures result == 10;
  {
    M.add(3, 7)
  };
};

// Any module with a compatible "add" function can be passed
module Adder {
  public func add(a : Nat, b : Nat) : Nat
    ensures result == a + b;
  { a + b };
};

Here Calculator.compute accepts any module with an add function of type (Nat, Nat) -> Nat. The Adder module satisfies this requirement.

Structural Typing​

Sector9 uses structural typing for modules, also called "duck typing." Two module types are compatible if they have compatible members - names and identity do not matter.

Key properties:

  • Compatibility is based on structure, not name
  • A module with more members than required is compatible (width subtyping)
  • Member types must be compatible (depth compatibility)
  • Field names must match exactly
module-type-width.sr9
// Width subtyping: modules with extra fields are compatible
// A module can have MORE members than required

module Consumer {
  // Only requires "getValue" - extra fields are ignored
  public func read(M : module { getValue : () -> Nat }) : Nat
    ensures result == M.getValue();
  {
    M.getValue()
  };
};

// This module has more than required - still compatible
module Provider {
  public func getValue() : Nat
    ensures result == 42;
  { 42 };

  public func setValue(n : Nat) : () { };  // Extra - ignored

  public func reset() : () { };            // Extra - ignored
};

The Provider module has extra methods (setValue, reset) but still satisfies the type module { getValue : () -> Nat } because it has the required getValue method with the correct signature.

Module Type in Contracts​

Module-typed parameters can appear in requires and ensures clauses. This lets you express properties about the module's behavior:

module-type-functor.sr9
// Functor pattern: module parameters with contracts
// The function requires specific properties from the module argument

module FunctorExample {
  // M must have inc/dec methods with specific behaviors
  public func apply(M : module { inc : Nat -> Nat; dec : Nat -> Nat }) : Nat
    requires M.inc(0) == 1;     // Module must satisfy this contract
    requires M.dec(5) == 4;     // And this one
    ensures result == 1;
  {
    let x = M.inc(0);
    let _ = M.dec(5);
    x
  };
};

// A module that satisfies the functor's requirements
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 requires clauses specify what the passed module must satisfy:

  • M.inc(0) == 1 - calling M.inc with 0 returns 1
  • M.dec(5) == 4 - calling M.dec with 5 returns 4

The caller must pass a module whose methods satisfy these contracts. The verifier checks that the passed module's postconditions imply the required preconditions.

Returning Modules​

Functions can return modules. The return type specifies the module structure:

module-type-return.sr9
// Returning modules from functions (module factories)
// The return type specifies the module's required structure

module ModuleFactory {
  // Returns a module with an "apply" method
  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 scale from the enclosing scope, creating a closure.

Type Compatibility Rules​

Width Subtyping​

A module type with more members is a subtype of one with fewer. Extra members are ignored:

// This is compatible:
module { a : Nat; b : Nat; c : Nat }  <:  module { a : Nat; b : Nat }

Depth Compatibility​

Member types must be compatible. A function with different parameter or return types is not compatible unless normal function subtyping and contract rules allow the replacement:

// NOT compatible - return types differ:
module { f : Nat -> Nat }  NOT <:  module { f : Nat -> Int }

Field Name Matching​

Field names must match exactly. Modules with different field names are not compatible:

// NOT compatible - names differ:
module { increment : Nat -> Nat }  NOT <:  module { inc : Nat -> Nat }

Common Errors​

Missing Required Field​

If a module is missing a required field, the type checker rejects it:

module-type-mismatch_reject.sr9
// Module type mismatch - REJECTED
// The module is missing a required field

module Consumer {
  public func process(M : module { foo : Nat -> Nat; bar : Nat -> Nat }) : Nat {
    M.foo(1) + M.bar(2)
  };
};

// Error: Missing required field "bar"
module Incomplete {
  public func foo(n : Nat) : Nat { n + 1 };
  // "bar" is missing!
};

module UseIncomplete {
  public func test() : Nat {
    Consumer.process(Incomplete)
  };
};

Signature Mismatch​

If a field exists but has the wrong type signature:

// Required: module { process : Nat -> Nat }
// Provided: module { process : Int -> Int }
// Error: type mismatch in field 'process'

Verification Considerations​

When module-typed parameters are used:

  1. Contract checking - The verifier assumes the passed module's contracts hold
  2. Parametric verification - Proofs work for any module satisfying the type
  3. No actor boundary - Module values do not introduce a message boundary or persistent identity

Plain function members such as compute : Nat -> Nat expose only that function shape. Use function type contracts when the interface itself should carry behavior, or add explicit requires clauses on the consumer when the consumer needs facts about a particular call:

// This constrains what M.compute must return
public func use(M : module { compute : Nat -> Nat }) : Nat
  requires M.compute(0) == 0;  // Explicit contract requirement
  ensures result == 0;
{
  M.compute(0)
}

Inline vs Named Module Types​

Module types can be written inline or defined as type aliases:

// Inline module type
func process(M : module { run : () -> Nat }) : Nat { M.run() };

// Named module type alias
type Runner = module { run : () -> Nat };
func process(M : Runner) : Nat { M.run() };

Named type aliases improve readability when the same module type appears multiple times.

Summary​

  • Module types use module { field : type; ... } syntax
  • Structural typing: compatibility based on structure, not name
  • Width subtyping: extra fields are allowed
  • Module parameters can appear in contracts with requires/ensures
  • Functions can return modules matching a type specification
  • Field names and member types must be compatible for assignment or calls