Type Operators

Type operators manipulate and combine types at the type level, enabling flexible type definitions without runtime overhead. They are most useful for deriving public interfaces from richer internal record or module shapes.

Overview

Sector9 provides five type operators:

Operator	Purpose	Syntax
and	Type intersection (GLB)	T1 and T2
or	Type union (LUB)	T1 or T2
...	Type spread (merge fields)	{ ...T1; ...T2 }
omit	Remove fields from object type	omit T { f1; f2 }
pick	Select fields from object type	pick T { f1; f2 }

All type operators are resolved at compile time during type checking. They do not exist at runtime.

The and Operator (Intersection)

The and operator computes the intersection (greatest lower bound) of two types. The result is a type that satisfies both constraints.

Syntax

type Combined = Type1 and Type2

Behavior

For record types, intersection produces a type with all fields from both types:

type HasName = { name : Text };
type HasAge = { age : Nat };
type Person = HasName and HasAge;  // { name : Text; age : Nat }

When both types have the same field name, the field types are combined using GLB (greatest lower bound):

// Different fields → merged
type T1 = { a : Nat; b : Text } and { b : Text; c : Nat };
// Result: { a : Nat; b : Text; c : Nat }

// Same field, compatible types (Nat <: Int) → uses more specific
type T2 = { x : Nat } and { x : Int };
// Result: { x : Nat }

// Same field, identical types → unchanged
type T3 = { x : Text } and { x : Text };
// Result: { x : Text }

// Same field, incompatible types → results in None (warning M0166)
type T4 = { x : Text } and { x : Nat };
// Result: None (unusable type)

For variant types, intersection produces a type with only common cases:

type V1 = { #a : Nat; #b : Text };
type V2 = { #b : Text; #c : Bool };
type Common = V1 and V2;  // { #b : Text }

For primitive types, and returns the more specific type when one is a subtype of the other:

// Nat is a subtype of Int
type T = Nat and Int;  // Result: Nat

Example

type-and-basic.sr9

// Type intersection with 'and' operator
persistent actor {
  type HasName = { name : Text };
  type HasAge = { age : Nat };
  type HasBoth = { name : Text; age : Nat };

  // Intersection: combines constraints from both types
  type Person = HasName and HasAge;

  public func createPerson() : async Person
    ensures result.name == "Alice";
    ensures result.age == 30;
  {
    // Person requires both name and age fields
    { name = "Alice"; age = 30 }
  };

  // Intersection with overlapping fields
  type R1 = { a : Nat; b : Text };
  type R2 = { b : Text; c : Bool };

  // R1 and R2 requires both: { a : Nat; b : Text; c : Bool }
  type Combined = R1 and R2;

  public func combinedRecord() : async Combined
    ensures result.a == 1;
    ensures result.c == true;
  {
    { a = 1; b = "hello"; c = true }
  };
}

The or Operator (Union)

The or operator computes the union (least upper bound) of two types. The result is a type that can be either operand.

Syntax

type Either = Type1 or Type2

Behavior

For record types, union produces a type with only common fields:

type R1 = { a : Nat; id : Text };
type R2 = { b : Nat; id : Text };
type Common = R1 or R2;  // { id : Text }

For variant types, union produces a type with all cases from both:

type V1 = { #a : Nat };
type V2 = { #b : Text };
type All = V1 or V2;  // { #a : Nat; #b : Text }

For primitive types, or returns the more general type:

type T = Nat or Int;  // Result: Int

Example

type-or-basic.sr9

// Type union with 'or' operator
persistent actor {
  type HasX = { x : Nat };
  type HasY = { y : Nat };

  // Union: result has only common fields
  type Common = HasX or HasY;  // Result: {} (no common fields)

  // More useful example with overlapping fields
  type R1 = { common : Nat; a : Text };
  type R2 = { common : Nat; b : Bool };

  // Union keeps only common fields: { common : Nat }
  type SharedOnly = R1 or R2;

  public func useUnion() : async SharedOnly
    ensures result.common == 42;
  {
    // SharedOnly only has 'common' field
    { common = 42 }
  };

  // Union of compatible primitives
  // Nat or Int gives Int (wider type)
  public func widerType(n : Nat) : async Int
    ensures result >= 0;
  {
    let x : Int = n;  // Nat widens to Int
    x
  };
}

The ... Operator (Type Spread)

The spread operator merges fields from multiple object types into a single object type, similar to how and works but with explicit syntax inside braces.

Syntax

type Combined = { ...Type1; ...Type2; ...Type3 }

Behavior

The spread operator collects all fields from each spread type. When the same field appears in multiple types:

• Later spreads override earlier ones (right-biased)
• Field types must be compatible

type A = { v : Nat; a : Nat };
type B = { v : Nat; b : Nat };
type C = { v : Nat; c : Nat };

// Merges all fields from A, B, and C
type ABC = { ...A; ...B; ...C };  // { v : Nat; a : Nat; b : Nat; c : Nat }

Combining with Other Operators

Type spread works naturally with omit and pick:

type Full = { ...A; ...B; ...C };
type WithoutC = omit Full { c };     // Remove c field
type OnlyVA = pick Full { v; a };    // Keep only v and a

Adding New Fields

You can add new fields alongside spreads:

type Extended = { ...Base; extra : Bool };

Comparison with and

Both spread and and merge record types, but they differ in syntax and semantics:

Feature	Spread { ...A; ...B }	Intersection A and B
Syntax	Inside braces	Infix operator
Override	Right-biased	Must be compatible
With new fields	{ ...A; x : T }	Not directly supported

Use spread when you want explicit control over field merging or when you want to add fields in the same object literal. Use and for combining types where all fields must be compatible.

The omit Operator

The omit operator removes specified fields from an object or module type.

Syntax

type Reduced = omit SourceType { field1; field2; ... }

Behavior

• Removes listed fields from the source type
• Non-existent field names are silently ignored
• Preserves the object sort (record, module, actor)
• Works with both record types and module types

Example

type-omit-basic.sr9

// Remove fields with 'omit' operator
persistent actor {
  type Full = { x : Nat; y : Nat; z : Nat };

  // Remove specific fields
  type WithoutZ = omit Full { z };      // { x : Nat; y : Nat }
  type WithoutXY = omit Full { x; y };  // { z : Nat }

  public func useOmit() : async WithoutZ
    ensures result.x == 1;
    ensures result.y == 2;
  {
    { x = 1; y = 2 }
  };

  // Omit gracefully ignores non-existent fields
  type R = { a : Nat; b : Nat };
  type RWithoutMissing = omit R { a; missing };  // { b : Nat }

  public func omitMissing() : async RWithoutMissing
    ensures result.b == 10;
  {
    { b = 10 }  // 'missing' was ignored
  };

  // Works with module types too
  type ModType = module { getValue : () -> Nat; helper : () -> () };
  type PublicOnly = omit ModType { helper };
}

The pick Operator

The pick operator selects only specified fields from an object or module type.

Syntax

type Selected = pick SourceType { field1; field2; ... }

Behavior

• Keeps only the listed fields
• Non-existent field names are silently ignored
• Preserves field mutability (var fields remain mutable)
• Preserves the object sort (record, module, actor)

Example

type-pick-basic.sr9

// Select fields with 'pick' operator
persistent actor {
  type Full = { x : Nat; y : Nat; z : Nat };

  // Select specific fields
  type OnlyX = pick Full { x };         // { x : Nat }
  type OnlyXZ = pick Full { x; z };     // { x : Nat; z : Nat }

  public func usePick() : async OnlyXZ
    ensures result.x == 1;
    ensures result.z == 3;
  {
    { x = 1; z = 3 }
  };

  // Pick gracefully ignores non-existent fields
  type R = { a : Nat; b : Nat };
  type RPickMissing = pick R { a; missing };  // { a : Nat }

  public func pickMissing() : async RPickMissing
    ensures result.a == 5;
  {
    { a = 5 }  // 'missing' was ignored
  };

  // Preserves mutability (var fields)
  type MutRec = { var x : Nat; y : Nat };
  type MutX = pick MutRec { x };  // { var x : Nat }

  public func pickMutable() : async Nat
    ensures result == 11;
  {
    let r : MutX = { var x = 10 };
    r.x += 1;  // Still mutable
    r.x
  };
}

Operator Precedence

Type operators have the following precedence (highest to lowest):

1. omit, pick - Bind tightest
2. and, or - Bind looser

This means:

// Parses as: R1 and (omit R2 { a })
type T1 = R1 and omit R2 { a };

// Use parentheses for clarity when combining
type T2 = (R1 and R2) or R3;

Restrictions

Object Type Requirement

The omit and pick operators can only be applied to object types (records, modules). Applying them to primitive types results in error M0093:

type-op-non-object_reject.sr9

// Error: omit/pick can only be applied to object types
persistent actor {
  // These are rejected with error M0093
  type A = omit Nat { x };  // Error: Nat is not an object type
  type B = pick Nat { y };  // Error: Nat is not an object type
}

No Forward References

The and and or operators cannot be used with types that have forward or recursive references to undefined types. This results in error M0168:

// Error M0168: forward reference
type A = B and C;  // B and C not yet defined
type B = {};
type C = {};

Inconsistent Type Warnings

When and results in an empty type (None) or or results in an overly broad type (Any), the compiler issues warnings:

• M0166: Intersection results in empty type
• M0167: Union results in overly general type

// Warning M0166: intersection is None
type Empty = { x : Text } and { x : Nat };  // Same field, incompatible types

// Warning M0167: union is Any
type TooWide = [var Nat] or [var Int];  // Mutable element types cannot be widened

Verification Implications

Type operators are fully resolved during type checking before verification. They affect verification through:

1. Record classification - Mutable records (var fields) become heap references with ownership tracking
2. Field-level effects - The resulting type determines which fields appear in modifies/reads clauses
3. Subtyping - Narrower types from and enable more precise contracts

The verifier never sees the operators themselves, only the resolved types. Verification-mode restrictions for spec immutability and mutable identity still apply to those resolved types.

Summary

• and computes type intersection: result satisfies both constraints
• or computes type union: result can be either operand
• { ...T1; ...T2 } merges fields from multiple types (right-biased override)
• omit removes specified fields from object types
• pick selects specified fields from object types
• All operators resolve at compile time with no runtime cost
• omit/pick/... only work on object types (records, modules)
• and/or cannot use forward type references

Related Topics

• Differences from Motoko for Sector9-only type operators
• Records for object shapes that work well with omit, pick, and spread
• Verified subtyping for restrictions on the resolved types