Type Checking

The AodhML type checker performs static analysis to ensure type safety before runtime. It supports inference, generics, and trait bounds.

Type Checker Pipeline

1. Name Resolution
   → Bind identifiers to their declarations
   → Build symbol tables

2. Type Inference
   → Infer types from context
   → Unify type variables

3. Type Validation
   → Check function signatures
   → Verify operator types
   → Ensure pattern exhaustiveness

4. Trait Resolution
   → Verify trait bounds
   → Select trait implementations

Type Inference Algorithm

AodhML uses Hindley-Milner style type inference with extensions for subtyping:

fn infer(expr: &Expr, env: &TypeEnv) -> Result<Type, TypeError> {
    match expr {
        Literal(Int(n)) => Ok(Type::I32),  // Default integer type
        Literal(Float(n)) => Ok(Type::F64), // Default float type
        Literal(String(s)) => Ok(Type::String),
        Literal(Bool(b)) => Ok(Type::Bool),

        Identifier(name) => {
            env.lookup(name)
               .ok_or(TypeError::Undefined(name.clone()))
        }

        Binary(op, left, right) => {
            let lt = infer(left, env)?;
            let rt = infer(right, env)?;
            check_binary_op(op, lt, rt)
        }

        // ... etc
    }
}

Generic Instantiation

When a generic function is called, the type checker instantiates it with concrete types:

// Generic definition
fn identity<T>(x: T) -> T { return x }

// Call site
identity(42)     // T = i32
identity(3.14)   // T = f64
identity("hi")   // T = String

Shape Checking

A unique feature of AodhML: tensor shapes are tracked at the type level where possible:

let a = Tensor::zeros([3, 4])   // Tensor<f32, [3, 4]>
let b = Tensor::zeros([4, 5])   // Tensor<f32, [4, 5]>
let c = a @ b                    // Tensor<f32, [3, 5]> — inferred!

// Compile error if shapes don't match:
let d = Tensor::zeros([3, 4])
let e = a @ d  // Error: incompatible shapes [4,5] and [3,4]