Architecture

Type System

Nova uses a bidirectional type system with refinement types for verification. Bidirectional type checking provides better error messages than Hindley-Milner while supporting advanced features like higher-rank polymorphism. Refinement types enable compile-time verification of program properties.

Algorithm Comparison

Algorithm	Inference Power	Error Messages	Complexity
Hindley-Milner	Full inference	Poor locality	~800 LOC
Bidirectional	Partial inference	Excellent	~1000 LOC
Local Type Inference	Minimal	Best	~500 LOC

Bidirectional Type Checking

Bidirectional type checking separates type checking (verifying an expression has a known type) from type synthesis (inferring an expression's type). This distinction enables precise error localization.

Core Judgments

Type Representation

/// Nova's type representation
pub enum Type {
    // Primitive types
    Int,
    Float,
    Bool,
    String,
    Unit,

    // Compound types
    Array(Box<Type>),
    Tuple(Vec<Type>),
    Record(Vec<(String, Type)>),

    // Function types
    Function {
        params: Vec<Type>,
        result: Box<Type>,
    },

    // Polymorphism
    TypeVar(TypeVarId),
    Forall {
        var: TypeVarId,
        body: Box<Type>,
    },

    // Refinement types (Nova-specific)
    Refined {
        base: Box<Type>,
        predicate: Box<Expr>,  // must evaluate to Bool
    },

    // Unknown (for inference)
    Unknown(UnknownId),
}

Bidirectional Checker Implementation

pub struct TypeChecker {
    env: Environment,
    unknowns: Vec<Option<Type>>,
    errors: Vec<TypeError>,
}

impl TypeChecker {
    /// Check: verify expression has expected type
    pub fn check(&mut self, expr: &Expr, expected: &Type) -> Result<(), TypeError> {
        match (expr, expected) {
            // Lambda checks against function type
            (Expr::Lambda { params, body, .. }, Type::Function { params: param_tys, result }) => {
                if params.len() != param_tys.len() {
                    return Err(TypeError::ArityMismatch { .. });
                }

                // Extend environment with parameter types
                let extended = self.env.extend_many(
                    params.iter().zip(param_tys).map(|(p, t)| (p.name.clone(), t.clone()))
                );

                // Check body against result type
                self.with_env(extended, |tc| tc.check(body, result))
            }

            // If-then-else checks both branches
            (Expr::If { cond, then_branch, else_branch, .. }, ty) => {
                self.check(cond, &Type::Bool)?;
                self.check(then_branch, ty)?;
                self.check(else_branch, ty)
            }

            // Subsumption: synthesize and check subtype
            (expr, expected) => {
                let inferred = self.synth(expr)?;
                self.subtype(&inferred, expected)
            }
        }
    }

    /// Synth: infer expression's type
    pub fn synth(&mut self, expr: &Expr) -> Result<Type, TypeError> {
        match expr {
            // Literals synthesize their type
            Expr::Int(_) => Ok(Type::Int),
            Expr::Float(_) => Ok(Type::Float),
            Expr::Bool(_) => Ok(Type::Bool),
            Expr::String(_) => Ok(Type::String),

            // Variables look up in environment
            Expr::Var { name, .. } => {
                self.env.lookup(name)
                    .cloned()
                    .ok_or(TypeError::UndefinedVariable { name: name.clone(), .. })
            }

            // Function application
            Expr::Apply { func, args, .. } => {
                let func_ty = self.synth(func)?;
                match func_ty {
                    Type::Function { params, result } => {
                        if args.len() != params.len() {
                            return Err(TypeError::ArityMismatch { .. });
                        }
                        for (arg, param_ty) in args.iter().zip(&params) {
                            self.check(arg, param_ty)?;
                        }
                        Ok(*result)
                    }
                    _ => Err(TypeError::NotAFunction { .. })
                }
            }

            // Annotated expressions
            Expr::Annotated { expr, ty, .. } => {
                self.check(expr, ty)?;
                Ok(ty.clone())
            }

            // Binary operators
            Expr::Binary { op, lhs, rhs, .. } => {
                self.synth_binop(op, lhs, rhs)
            }

            _ => Err(TypeError::CannotInfer { .. })
        }
    }
}

Refinement Types (Nova-Specific)

Refinement types attach predicates to base types, enabling compile-time verification. This is Nova's key differentiator: contracts are not just runtime checks but are verified at compile time when possible.

Refinement Syntax

// A non-negative integer
type Nat = { x: Int | x >= 0 }

// A non-empty array
type NonEmpty<T> = { arr: Array<T> | len(arr) > 0 }

// A sorted array
type Sorted<T> = { arr: Array<T> | forall i, j. i < j => arr[i] <= arr[j] }

// Function with precondition and postcondition
fn sqrt(x: { n: Float | n >= 0.0 }) -> { r: Float | r >= 0.0 && r * r == x } {
    // ...
}

Refinement Type Checking

impl TypeChecker {
    /// Check refinement predicate validity
    fn check_refinement(
        &mut self,
        expr: &Expr,
        refined: &Type,
    ) -> Result<(), TypeError> {
        match refined {
            Type::Refined { base, predicate } => {
                // First check base type
                self.check(expr, base)?;

                // Try to verify predicate statically
                match self.verify_predicate(expr, predicate) {
                    VerifyResult::Verified => Ok(()),
                    VerifyResult::Falsified(counterexample) => {
                        Err(TypeError::RefinementViolation {
                            predicate: predicate.clone(),
                            counterexample,
                            ..
                        })
                    }
                    VerifyResult::Unknown => {
                        // Cannot verify statically, insert runtime check
                        self.insert_runtime_check(expr, predicate);
                        Ok(())
                    }
                }
            }
            _ => self.check(expr, refined)
        }
    }

    /// Attempt to verify predicate using SMT solver
    fn verify_predicate(
        &self,
        expr: &Expr,
        predicate: &Expr,
    ) -> VerifyResult {
        // Convert to SMT-LIB format
        let smt = self.to_smt(expr, predicate);

        // Check with Z3 or similar
        match self.smt_solver.check(&smt) {
            SatResult::Unsat => VerifyResult::Verified,
            SatResult::Sat(model) => VerifyResult::Falsified(model),
            SatResult::Unknown => VerifyResult::Unknown,
        }
    }
}

Type Inference for Unknowns

While bidirectional checking reduces annotation burden, Nova still needs inference for local variables and partial type information. This uses unification with unknown types.

impl TypeChecker {
    /// Create a fresh unknown type variable
    fn fresh_unknown(&mut self) -> Type {
        let id = UnknownId(self.unknowns.len());
        self.unknowns.push(None);
        Type::Unknown(id)
    }

    /// Unify two types, solving unknowns
    fn unify(&mut self, a: &Type, b: &Type) -> Result<(), TypeError> {
        let a = self.resolve(a);
        let b = self.resolve(b);

        match (&a, &b) {
            // Same type
            (Type::Int, Type::Int) => Ok(()),
            (Type::Float, Type::Float) => Ok(()),
            (Type::Bool, Type::Bool) => Ok(()),
            (Type::String, Type::String) => Ok(()),

            // Solve unknown
            (Type::Unknown(id), ty) | (ty, Type::Unknown(id)) => {
                if self.occurs_check(*id, ty) {
                    return Err(TypeError::InfiniteType { .. });
                }
                self.unknowns[id.0] = Some(ty.clone());
                Ok(())
            }

            // Structural types
            (Type::Array(a), Type::Array(b)) => self.unify(a, b),

            (Type::Function { params: p1, result: r1 },
             Type::Function { params: p2, result: r2 }) => {
                if p1.len() != p2.len() {
                    return Err(TypeError::ArityMismatch { .. });
                }
                for (a, b) in p1.iter().zip(p2) {
                    self.unify(a, b)?;
                }
                self.unify(r1, r2)
            }

            _ => Err(TypeError::TypeMismatch { expected: a, found: b, .. })
        }
    }

    /// Resolve unknown to its solution (if any)
    fn resolve(&self, ty: &Type) -> Type {
        match ty {
            Type::Unknown(id) => {
                match &self.unknowns[id.0] {
                    Some(resolved) => self.resolve(resolved),
                    None => ty.clone(),
                }
            }
            _ => ty.clone()
        }
    }
}

Implementation Plan

1. Implement Type enum with all variants
2. Build bidirectional check and synth functions
3. Add unification for unknown types
4. Implement refinement type checking with predicate verification
5. Integrate SMT solver for static verification
6. Add runtime check insertion for unverifiable predicates

References

• Complete and Easy Bidirectional Type Checking - Dunfield & Krishnaswami
• Typechecker Zoo - Type system implementations in Rust
• bidir-type-infer - Rust implementation
• Liquid Haskell - Refinement types inspiration
• Rust Type Inference - rustc's approach