Generic Type Definitions

Generic types are parameterized type definitions. Instead of writing separate aliases for Box<Int>, Box<Bool>, and Box<Text>, you define one shape Box<T> and instantiate it with concrete types. The same monomorphization model used for generic functions applies to generic type definitions during verification.

Basic Syntax

Type parameters appear in angle brackets after the type name:

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

The <T> declares a type parameter. Inside the type definition, T acts as a placeholder for any concrete type. When you use the type, provide a concrete type argument.

Multiple Type Parameters

Types can have multiple parameters separated by commas:

type Pair<A, B> = (A, B);
type Result<T, E> = { #ok : T; #err : E };
type Triple<X, Y, Z> = (X, Y, Z);

Use descriptive names when the meaning is clear: <Key, Value> for maps, <Ok, Err> for results.

Common Generic Type Patterns

generic-type-basic.sr9

// Basic generic type definitions

module GenericTypes {
  // Single type parameter
  public type Box<T> = { value : T };

  // Multiple type parameters
  public type Pair<A, B> = (A, B);

  // Generic variant (tagged union)
  public type Result<T, E> = { #ok : T; #err : E };

  // Generic option wrapper
  public type Option<T> = ?T;

  // Recursive generic type
  public type List<T> = ?(T, List<T>);
};

persistent actor {
  public func useBox() : async Nat
    ensures result == 42;
  {
    let b : GenericTypes.Box<Nat> = { value = 42 };
    b.value
  };

  public func usePair() : async Int
    ensures result == 10;
  {
    let p : GenericTypes.Pair<Int, Bool> = (10, true);
    p.0
  };

  public func useResult() : async Nat
    ensures result == 100;
  {
    let r : GenericTypes.Result<Nat, Text> = #ok(100);
    switch r {
      case (#ok(n)) n;
      case (#err(_)) 0;
    }
  };
}

These patterns appear throughout Sector9 code:

Pattern	Definition	Purpose
Box<T>	{ value : T }	Wrap a single value
Pair<A, B>	(A, B)	Two values together
Option<T>	?T	Optional value
Result<T, E>	{ #ok : T; #err : E }	Success or failure
List<T>	?(T, List<T>)	Linked list

Instantiating Generic Types

Use a generic type by providing type arguments in angle brackets:

let box : Box<Int> = { value = 42 };
let pair : Pair<Text, Bool> = ("hello", true);
let result : Result<Nat, Text> = #ok(100);

Type arguments replace type parameters throughout the definition. Box<Int> becomes { value : Int }.

Type Inference

The compiler can infer type arguments from context:

// Explicit: type arguments provided
let b1 : Box<Int> = { value = 42 };

// Inferred: type determined from usage
let b2 = { value = 42 };  // Underlying record type inferred

Aliases are transparent, so inference usually finds the underlying structural type rather than a nominal alias name. Provide explicit type arguments when:

• The type cannot be inferred
• You want to be explicit for readability
• Multiple valid types could apply

Bounded Type Parameters

Constrain type parameters with upper bounds using <::

generic-type-bounds.sr9

// Generic types with bounded type parameters

module Bounded {
  // T must have a 'name' field
  public type Named<T <: { name : Text }> = {
    item : T;
    count : Nat
  };

  // T must have an 'id' field
  public type Identified<T <: { id : Nat }> = {
    data : T;
    timestamp : Int
  };
};

persistent actor {
  type Person = { name : Text; age : Nat };
  type Product = { id : Nat; price : Nat };

  public func testNamed() : async Text
    ensures result == "Alice";
  {
    let p : Person = { name = "Alice"; age = 30 };
    let named : Bounded.Named<Person> = { item = p; count = 1 };
    named.item.name
  };

  public func testIdentified() : async Nat
    ensures result == 42;
  {
    let prod : Product = { id = 42; price = 100 };
    let entry : Bounded.Identified<Product> = { data = prod; timestamp = 0 };
    entry.data.id
  };
}

The bound T <: { name : Text } restricts T to types with at least a name field. Any type satisfying the constraint can be used.

Bound Syntax

// Single bound
type Named<T <: { name : Text }> = { item : T };

// Multiple parameters with bounds
type Keyed<K <: { id : Nat }, V> = Map<K, V>;

// Default bound (implicit)
type Any<T> = { data : T };  // T <: Any (implicit)

Without an explicit bound, type parameters default to Any, accepting any type.

Recursive Generic Types

Generic types can reference themselves to create recursive data structures:

generic-type-recursive.sr9

// Recursive generic type definitions

module Recursive {
  // Linked list
  public type List<T> = ?(T, List<T>);

  // Binary tree
  public type Tree<T> = {
    value : T;
    left : ?Tree<T>;
    right : ?Tree<T>
  };

  // Helper to count list elements
  public pure func length<T>(list : List<T>) : Nat {
    switch list {
      case null 0;
      case (?(_, tail)) 1 + length<T>(tail);
    }
  };
};

persistent actor {
  public func testList() : async Nat
    ensures result == 3;
  {
    // Build list: 1 -> 2 -> 3 -> null
    let list : Recursive.List<Nat> = ?(1, ?(2, ?(3, null)));
    Recursive.length<Nat>(list)
  };

  public func testTree() : async Int
    ensures result == 10;
  {
    let tree : Recursive.Tree<Int> = {
      value = 10;
      left = null;
      right = null
    };
    tree.value
  };
}

Valid Recursive Patterns

// Linked list: base case is null
type List<T> = ?(T, List<T>);

// Binary tree: base case is null children
type Tree<T> = { value : T; left : ?Tree<T>; right : ?Tree<T> };

// Variant with recursive case
type Expr<T> = { #lit : T; #add : (Expr<T>, Expr<T>) };

Recursive types must have a valid base case. The type must be "productive" - not infinitely expanding.

Generic Types with Spec Collections

Ghost state often uses generic spec collections:

generic-type-spec.sr9

// Generic types with spec collections

persistent actor {
  // Ghost state using generic spec collections
  ghost var balances : Map<Nat, Nat> = Map.empty<Nat, Nat>();
  ghost var _allowed : Set<Nat> = Set.empty<Nat>();
  ghost var log : Seq<Int> = Seq.empty<Int>();

  invariant Map.card(balances) >= 0;
  invariant Seq.len(log) >= 0;

  public func deposit(user : Nat, amount : Nat) : async ()
    modifies balances
    ensures Map.contains(user, balances);
  {
    ghost {
      let current = Map.getOr(balances, user, 0);
      balances := Map.update(balances, user, current + amount);
    };
  };

  public func record(value : Int) : async ()
    modifies log
    ensures Seq.len(log) == old(Seq.len(log)) + 1;
  {
    ghost {
      log := Seq.concat(log, Seq.singleton(value));
    };
  };
}

The built-in spec collections are all generic:

Collection	Type	Purpose
Map<K, V>	Key-value pairs	Associative mapping
Set<T>	Unique elements	Membership tracking
Seq<T>	Ordered elements	Indexed access
Multiset<T>	Elements with counts	Bag semantics

Element Type Restrictions

Spec collection elements, keys, and values must be spec-immutable, except opaque/token handles by identity. These types are rejected:

// WRONG: mutable records
type Cell = { var x : Int };
ghost let cells : Set<Cell> = Set.empty();  // Error M0242

// WRONG: mutable arrays
ghost let arrs : Seq<[var Int]> = Seq.empty();  // Error M0242

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

// WRONG: actor types
ghost let actors : Map<actor {}, Nat> = Map.empty();  // Error M0242

Valid element types include primitives, immutable records, tuples, options, and variants with immutable payloads. See collection-linearity restrictions for the verifier rule behind this.

Variance

Generic types have variance that determines subtyping behavior:

Position	Variance	Subtyping Rule
Output (return)	Covariant	Box<Sub> <: Box<Super>
Input (parameter)	Contravariant	Handler<Super> <: Handler<Sub>
Both	Invariant	Exact match required

Variance in Practice

// Covariant: option element
?Sub <: ?Super  // when Sub <: Super

// Covariant: variant payloads
{ #ok : Sub } <: { #ok : Super }

// Invariant: mutable containers
[var Sub] is NOT a subtype of [var Super]

See Subtyping Rules for complete variance rules.

Verification and Monomorphization

Sector9 uses monomorphization for verification. Each generic type used with different type arguments creates a specialized version internally.

When you write:

type Box<T> = { value : T };
let intBox : Box<Int> = { value = 42 };
let boolBox : Box<Bool> = { value = true };

The verifier treats Box<Int> and Box<Bool> as distinct types. Each instantiation is verified with its concrete types.

Viper Output

In generated Viper code (--viper), generic types appear as specialized definitions:

// Box<Int> becomes a distinct ADT
adt Box$Int { ... }

// Box<Bool> becomes another ADT
adt Box$Bool { ... }

Type arguments are encoded in the generated names.

Restrictions

Several patterns are rejected for generic type definitions.

Non-Productive Types

Types must have a valid base case:

// Rejected: no base case
type Bad<T> = Bad<T>;

// Rejected: circular without termination
type A<T> = B<T>;
type B<T> = A<T>;

Expansive Types

Type parameters must appear as immediate arguments, not wrapped:

Valid

// T is immediate argument
type Good<T> = ?Good<T>;

// T in tuple, recursion immediate
type List<T> = ?(T, List<T>);

// T in variant payload
type Tree<T> = { #leaf : T; #node : (Tree<T>, Tree<T>) };

Invalid

// T wrapped in optional
type Bad<T> = ?Bad<?T>;  // Rejected

// T in record wrapping
type Worse<T> = Bad<{ tag : T }>;  // Rejected

Cyclic Bounds

Type parameter bounds cannot form cycles:

// Rejected: self-referential bound
func f<A <: A>(a : A) { };

// Rejected: mutual cycle
func g<A <: B, B <: A>(a : A, b : B) { };

Outer Scope Capture

Types cannot capture parameters from enclosing scopes:

// Rejected: D references outer parameter A
class C<A>() {
  type D = A;  // Error M0137
};

Error Reference

Error Code	Condition
M0137	Type references outer scope parameter
M0043	Cyclic type bounds
M0044	Duplicate type parameter names
M0045	Wrong number of type arguments
M0046	Type argument violates bound
M0242	Mutable type in spec collection

Best Practices

1. Use generics for reusable abstractions: type Result<T, E> is better than separate IntResult, BoolResult, etc.

2. Prefer explicit type arguments: When in doubt, write Box<Int> rather than relying on inference

3. Name parameters meaningfully: <Key, Value> is clearer than <K, V> for complex types

4. Document bounds: When a type parameter has constraints, explain why in comments

5. Keep recursion simple: Prefer direct recursion like List<T> over complex mutual recursion

Related Topics

• Type aliases for non-generic type naming
• Subtyping rules for variance and compatibility
• Generic functions for functions with type parameters
• Spec collections for built-in generic proof types
• Spec collection restrictions for spec-immutable requirements

Summary

• Define generic types with type Name<T> = ...
• Multiple parameters: type Pair<A, B> = (A, B)
• Instantiate with type arguments: Box<Int>
• Bounds constrain parameters: <T <: Constraint>
• Recursive types need valid base cases
• Spec collection elements, keys, and values must be immutable
• The verifier specializes generic uses: each instantiation is verified with its concrete type arguments
• Non-productive, expansive, and cyclic definitions are rejected