Type Systems

How the compiler catches bugs before your code ever runs.

Why Types Matter

Every value in your program has a type — a classification that tells us what operations are valid. The number 42 is an Int. The text "hello" is a String. The function add has type (Int, Int) -> Int.

Types let the compiler catch mistakes:

# Python
def add(a, b):
    return a + b

add("hello", 5)
# TypeError at runtime!
# Can only concatenate str to str

// Nova
fn add(a: Int, b: Int) -> Int {
    a + b
}

add("hello", 5)
// Error at compile time!
// Expected Int, found String

The difference is when you find the bug. In Python, you find it when a user triggers that code path. In Nova, you find it before anyone runs the program.

Static vs. Dynamic Typing

Languages fall into two camps:

• Dynamically typed (Python, JavaScript, Ruby): Types are checked at runtime. Variables can hold any type. Flexibility but more runtime errors.
• Statically typed (Rust, Go, Nova, TypeScript): Types are checked at compile time. Variables have fixed types. More upfront work but fewer runtime errors.

Nova is statically typed, but with type inference — you don't always need to write types explicitly. The compiler figures them out.

// You can write types explicitly
let x: Int = 42;
let name: String = "Nova";

// Or let the compiler infer them
let x = 42;           // Inferred: Int
let name = "Nova";    // Inferred: String
let sum = x + 10;     // Inferred: Int

How Type Checking Works

The type checker walks the AST and assigns types to every expression. It follows rules like:

Type Checking in Code

impl TypeChecker {
    fn check_expr(&mut self, expr: &Expr) -> Type {
        match expr {
            // Literals have known types
            Expr::Literal(Literal::Int(_)) => Type::Int,
            Expr::Literal(Literal::Float(_)) => Type::Float,
            Expr::Literal(Literal::String(_)) => Type::String,

            // Variables: look up in environment
            Expr::Var(name) => self.env.lookup(name),

            // Binary expressions: check both sides
            Expr::Binary { left, op, right } => {
                let left_type = self.check_expr(left);
                let right_type = self.check_expr(right);

                match (op, left_type, right_type) {
                    // Int + Int = Int
                    (Add, Type::Int, Type::Int) => Type::Int,
                    // String + String = String
                    (Add, Type::String, Type::String) => Type::String,
                    // Comparison operators return Bool
                    (Eq | Lt | Gt, _, _) => Type::Bool,
                    // Everything else is an error
                    _ => self.error("Type mismatch"),
                }
            }

            // Function calls: check arguments match parameters
            Expr::Call { name, args } => {
                let func_type = self.env.lookup_fn(name);
                for (arg, param_type) in args.iter().zip(&func_type.params) {
                    let arg_type = self.check_expr(arg);
                    if arg_type != *param_type {
                        self.error("Argument type mismatch");
                    }
                }
                func_type.return_type
            }
        }
    }
}

Bidirectional Type Checking

Nova uses bidirectional type checking — information flows both ways. Sometimes we synthesize a type from an expression (bottom-up), and sometimes we check an expression against an expected type (top-down).

// Synthesizing: figure out the type from the expression
let x = 42;  // Synthesize: 42 has type Int, so x has type Int

// Checking: verify expression matches expected type
let y: Int = 42;  // Check: does 42 have type Int? Yes!

// Checking helps with ambiguous literals
let z: Float = 42;  // Check: 42 can be Float, so z is Float

This bidirectional flow is especially useful for complex expressions where context helps resolve ambiguity.

Nova's Special Power: Refinement Types

Most languages stop at basic types like Int and String. But Nova goes further with refinement types — types with constraints.

Here's what this looks like in Nova:

// Regular types: can only check "is it an Int?"
fn divide(a: Int, b: Int) -> Int {
    a / b  // What if b is 0? Runtime error!
}

// Refinement types: can check "is it a non-zero Int?"
fn divide(a: Int, b: Int) -> Int
where
    requires b != 0  // Compile-time guarantee!
{
    a / b  // Now we KNOW b is never 0
}

With the requires clause, Nova refuses to compile code that might pass 0:

let result = divide(10, 0);  // Compile error!

let x = get_user_input();
let result = divide(10, x);  // Also error! x might be 0

// You must prove x is not 0
if x != 0 {
    let result = divide(10, x);  // Now OK!
}

More Refinement Type Examples

// Array access: index must be in bounds
fn get(arr: [T], index: Int) -> T
where
    requires index >= 0
    requires index < arr.len()
{
    arr[index]  // Guaranteed safe!
}

// User age: must be positive and reasonable
type Age = Int where self > 0 && self < 150;

// Percentage: must be 0-100
type Percentage = Float where self >= 0.0 && self <= 100.0;

// Non-empty string
type NonEmptyString = String where self.len() > 0;

The Type Environment

As the type checker walks the AST, it builds an environment — a map from names to types. Each scope creates a new layer in the environment.

fn example() {
    let x = 5;           // env: { x: Int }
    let y = 10;          // env: { x: Int, y: Int }

    {
        let z = 15;      // env: { x: Int, y: Int, z: Int }
        let sum = x + y + z;
    }                    // z goes out of scope

    // env: { x: Int, y: Int }
    // z is no longer accessible here
}

Function Types

Functions have types too. The type of a function tells you what arguments it takes and what it returns:

fn add(a: Int, b: Int) -> Int
// Type: (Int, Int) -> Int

fn greet(name: String) -> String
// Type: (String) -> String

fn print(msg: String) -> ()
// Type: (String) -> ()   (returns nothing)

This is crucial for higher-order functions — functions that take other functions as arguments:

fn map(arr: [Int], f: (Int) -> Int) -> [Int]
// f is a function from Int to Int

fn double(x: Int) -> Int { x * 2 }

let result = map([1, 2, 3], double);  // [2, 4, 6]

Generic Types

Sometimes you want a function that works with multiple types. Nova supports generics — type parameters that get filled in at call sites:

// A generic function: works for any type T
fn identity(x: T) -> T {
    x
}

// At each call site, T gets a concrete type
identity(42)       // T = Int
identity("hello") // T = String

// Generic types can have constraints
fn addNumeric>(a: T, b: T) -> T {
    a + b
}
// T must implement the Numeric trait (Int, Float, etc.)

Error Messages That Help

A good type system isn't just about catching errors — it's about explaining them clearly:

error[E0308]: mismatched types
  --> main.nova:5:12
   |
4  |     fn add(a: Int, b: Int) -> Int { a + b }
   |                                     ----- expected `Int` because of return type
5  |     add("hello", 5)
   |         ^^^^^^^
   |         |
   |         expected `Int`, found `String`
   |
   = note: arguments to `add` must be `Int`, not `String`
   = help: try converting the string to an integer:
           add("hello".parse()?, 5)

Nova's type checker uses spans (from the lexer and parser) to point exactly at the problematic code, and provides suggestions for fixing the issue.

What's Next?

Type checking ensures your code is well-typed, but it doesn't verify deeper properties. Can you prove your sorting function actually sorts? That your search algorithm terminates? That's where verification comes in — Nova's most advanced feature.