Type Aliases

Type aliases give names to existing types, making code more readable and self-documenting. They are transparent: an alias does not create a new nominal type, it names a structural shape.

Basic Syntax

The type keyword creates a type alias:

type UserId = Nat;
type Amount = Int;
type Coordinate = (Int, Int);

After declaration, UserId and Nat are interchangeable. The alias adds semantic meaning without creating a distinct runtime or proof type.

Common Use Cases

Primitive Wrappers

Give semantic names to primitive types:

type-alias-primitive.sr9

// Type aliases for domain concepts
type UserId = Nat;
type Balance = Nat;
type Timestamp = Int;

persistent actor {
  var nextId : UserId = 0;
  var totalBalance : Balance = 0;

  public func createUser() : async UserId
    modifies nextId
    ensures result == old(nextId);
    ensures nextId == old(nextId) + 1;
  {
    let id = nextId;
    nextId += 1;
    id
  };

  public func deposit(amount : Balance) : async ()
    modifies totalBalance
    ensures totalBalance == old(totalBalance) + amount;
  {
    totalBalance += amount;
  };
}

Record Types

Name complex record structures:

type-alias-record.sr9

// Record type aliases for structured data
type Point = { x : Int; y : Int };
type Rectangle = { topLeft : Point; bottomRight : Point };

persistent actor {
  transient var position : Point = { x = 0; y = 0 };

  public func move(dx : Int, dy : Int) : async ()
    modifies position
    ensures position.x == old(position.x) + dx;
    ensures position.y == old(position.y) + dy;
  {
    position := { x = position.x + dx; y = position.y + dy };
  };

  pure func width(rect : Rectangle) : Int {
    rect.bottomRight.x - rect.topLeft.x
  };

  pure func height(rect : Rectangle) : Int {
    rect.bottomRight.y - rect.topLeft.y
  };
}

Variant Types

Create named variant types for state machines and enums:

type-alias-variant.sr9

// Variant type aliases for enums and state machines
type Status = { #pending; #approved; #rejected };
type Result<T> = { #ok : T; #err : Text };

persistent actor {
  transient var status : Status = #pending;

  public func approve() : async ()
    modifies status
    ensures status == #approved;
  {
    status := #approved;
  };

  public func reject() : async ()
    modifies status
    ensures status == #rejected;
  {
    status := #rejected;
  };

  pure func isComplete(s : Status) : Bool {
    switch (s) {
      case (#pending) { false };
      case (#approved) { true };
      case (#rejected) { true };
    }
  };

  pure func unwrapOr<T>(r : Result<T>, default : T) : T {
    switch (r) {
      case (#ok(value)) { value };
      case (#err(_)) { default };
    }
  };
}

Function Types

Simplify higher-order function signatures:

type-alias-function.sr9

// Function type aliases for higher-order code
type UnaryOp = Int -> Int;
type BinaryOp = (Int, Int) -> Int;

module Math {
  public pure func apply(f : UnaryOp, x : Int) : Int
    ensures result == f(x);
  {
    f(x)
  };

  public pure func negate() : UnaryOp {
    pure func(x : Int) : Int { -x }
  };

  public pure func double() : UnaryOp {
    pure func(x : Int) : Int { x * 2 }
  };
}

Module Types

Name module interfaces for reuse:

type-alias-module.sr9

// Module type aliases for interface reuse
type Processor = module {
  process : Nat -> Nat;
};

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

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

module Selector {
  // Type alias makes the return type clearer
  public func pick(useFast : Bool) : Processor {
    if (useFast) Fast else Slow
  };
};

Generic Type Aliases

Type aliases can have type parameters:

type Pair<A, B> = (A, B);
type Box<T> = { value : T };
type Result<T, E> = { #ok : T; #err : E };

Use them by providing type arguments:

let coords : Pair<Int, Int> = (10, 20);
let wrapped : Box<Text> = { value = "hello" };
let outcome : Result<Nat, Text> = #ok(42);

Bounded Type Parameters

Constrain type parameters with upper bounds using <::

type Named<T <: { name : Text }> = { item : T; count : Nat };

The bound restricts T to types with at least a name field. Without an explicit bound, parameters default to Any.

Visibility

Type aliases follow normal visibility rules:

module Types {
  // Public: usable outside this module
  public type UserId = Nat;

  // Private: only usable within this module
  type InternalId = Int;
};

Recursive Types

Type aliases can reference themselves for recursive data structures:

type Tree = {
  value : Int;
  left : ?Tree;
  right : ?Tree
};

type List<T> = ?(T, List<T>);

The verifier handles recursive types through normalization and cycle detection, but the type definition must remain productive.

Verification Behavior

Type aliases are transparent to verification. The verifier normalizes aliases to their underlying types, so:

• Proof obligations use the expanded form
• Pattern matching over aliased variants works correctly
• Mutable record aliases share permission predicates when aliased

For example, these are equivalent for verification:

type Status = { #pending; #done };
var state : Status = #pending;

// Same as:
var state : { #pending; #done } = #pending;

Restrictions

Several patterns are rejected:

Non-Productive Types

Type definitions must have a valid base case:

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

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

Expansive Types

Type parameters must appear as immediate arguments, not wrapped in larger expressions:

// Accepted: T is immediate
type Good<T> = ?Good<T>;

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

// Rejected: T in record
type Also_Bad<T> = { #nil; #cons : (T, Also_Bad<{ tag : T }>) };

Cyclic Bounds

Type parameter bounds cannot form cycles:

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

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

Open Type Definitions

Types cannot capture parameters from outer scopes:

// Rejected: D captures A from outer scope
class C<A>() {
  type D = A;
};

Best Practices

1. Use aliases for domain concepts: type Balance = Nat is clearer than raw Nat
2. Name function types: type Comparator<T> = (T, T) -> Int improves readability
3. Group related types: Place type aliases in dedicated modules for organization
4. Prefer aliases over inline types: Named types in signatures are easier to understand

Related Topics

• Records and variants for common alias targets
• Generic type definitions for parameterized aliases
• Type operators for deriving aliases with and, or, omit, pick, and spread
• Verified subtyping for the verification restrictions that still apply after aliases expand

Summary

• type Name = ... creates a type alias
• Aliases are interchangeable with their underlying types
• Generic aliases use <T> syntax with optional <: bounds
• Recursive types work with proper base cases
• The verifier expands aliases transparently
• Non-productive, expansive, and cyclic definitions are rejected