Type System

Status: in progress

This article covers the type system foundations. The formal subtyping rules and full lattice definition will be expanded from spec source 03_TYPES.csl.

Overview

Sigil’s type system has four jobs:

1. Prevent LoA violations — distinct phantom types for coordinate spaces, units, and memory ownership
2. Track effects — effect rows are part of function types
3. Enable correct autodiff — the Differentiable constraint and related traits
4. Support verification — type-level invariants that the SMT solver can check

Primitive types

Type	Description
bool	Boolean
i8, i16, i32, i64, i128	Signed integers
u8, u16, u32, u64, u128	Unsigned integers
f16, f32, f64	Floating point (f16 is GPU-only)
usize, isize	Platform-width integers

Vector and matrix types

SIMD-native vector types are built into the language, not a library:

Vec2, Vec3, Vec4          // f32 vectors
Vec2i, Vec3i, Vec4i       // i32 vectors
Vec2u, Vec3u, Vec4u       // u32 vectors

Mat2x2, Mat3x3, Mat4x4   // column-major f32 matrices
Mat3x4                    // useful for transform matrices

These map directly to SPIR-V vector/matrix types on the GPU and SIMD registers on the CPU.

Phantom type parameters

Phantom types are zero-cost type parameters that exist only at compile time:

// Vec3<S> where S is a space tag
struct Vec3<S = ()> {
    x: f32, y: f32, z: f32
}

// Space tags — marker types with no fields
struct World;
struct View;
struct Clip;
struct Screen;

// These are incompatible types:
let world_pos: Vec3<World> = Vec3::new(1.0, 0.0, 0.0);
let clip_pos:  Vec3<Clip>  = Vec3::new(0.5, 0.5, 0.0);

// This is a compile error — types don't match:
// let bad: Vec3<Clip> = world_pos;

// Transforms convert between spaces explicitly:
let view_pos: Vec3<View> = camera.world_to_view(world_pos);

At codegen, all phantom parameters are erased. Vec3<World> and Vec3<Clip> both compile to identical SIMD operations.

Function types and effects

Function types include their effect row:

// Type of a pure function (f32, f32) -> f32
fn add(a: f32, b: f32) -> f32  // effect row: empty (pure)

// Type of an I/O function
fn print(s: &str) !io

// Type of a GPU shader
fn vs_main(v: Vertex) -> Vec4<Clip> !gpu

// First-class function values carry their effects
let f: fn(f32) -> f32 = |x| x * x;         // pure function value
let g: fn(&str) !io   = |s| println!(s);    // io function value

The Differentiable trait

Any type that can participate in automatic differentiation must implement Differentiable:

trait Differentiable {
    type Tangent;        // the type of the derivative (often same as Self)
    fn zero() -> Self::Tangent;
    fn add_tangent(self, t: Self::Tangent) -> Self;
}

// Built-in impls:
// f32: Differentiable<Tangent = f32>
// Vec2, Vec3, Vec4: Differentiable
// Vec3<S>: Differentiable (phantom param erased in tangent space)

Structs whose fields are all Differentiable automatically derive it via #[derive(Differentiable)].

Algebraic types

Structs (product types)

struct Sphere {
    center: Vec3<World>,
    radius: f32,
}

Enums (sum types)

enum Light {
    Directional { direction: Vec3<World>, color: Vec3 },
    Point       { position: Vec3<World>, intensity: f32 },
    Spot        { /* ... */ },
}

Enums in Sigil are full algebraic data types, not C-style integer enums.

Capabilities

The capability system gates access to hardware resources and privileged operations. Capabilities are type-level tokens that must be passed explicitly:

// To create a GPU buffer, you need the GpuAllocator capability
fn create_buffer<T>(cap: &GpuAllocator, data: &[T]) -> Buffer<T> !gpu {
    // ...
}

Capabilities cannot be forged — you can only obtain them from the runtime or from a caller who holds one. This prevents GPU allocation from happening in unauthorized contexts.

Full capability system documentation: §B.4 Capability System

See also

• §B.3 Effect System
• §B.4 Capability System
• §C.1 Autodiff — Differentiable in depth
• Spec source: 03_TYPES.csl