Static Typing for Compose

Goal

Introduce static type checking with local type inference, performed before runtime, without changing the interpreter execution model yet.

The system should:

• Catch type errors before execution
• Support constraint-based inference inside functions
• Produce rich diagnostics linked to spans (for LSP & errors)
• Preserve the current AST + interpreter architecture

---

High-level design

Typing model

• Statically typed language

• Local inference only

  • Function parameters and return types must be annotated
  • No inference across function boundaries

• Closures

  • Argument and return types inferred from usage

• Constraint-based inference

  • Types are inferred by collecting and resolving constraints
  • Ambiguous expressions are resolved using contextual constraints (e.g. return type)

---

Language rules

Functions

• Every function must declare:

  • Parameter types
  • Return type

• The function body is type-checked independently

• Return expressions must unify with the declared return type

fn sum(a: Int, b: Int) -> Int {
    a + b
}

---

Expressions & blocks

• Every expression has:

  • An original type (before coercions)
  • A final type (after coercions / context)

• Blocks:

  • If the last expression has no trailing semicolon, its value is returned
  • If it has a trailing semicolon, the block returns ()

This distinction must be preserved for diagnostics.

{
    foo();        // produces T, coerced to ()
    bar()         // produces U, returned
}

If a trailing semicolon causes a type mismatch, the error should suggest removing it.

---

Branching (if, match)

• Branches must unify to a single type unless context restricts it
• If the surrounding context expects T, branch results may be coerced to T
• Flow-sensitive narrowing is supported:

if (v is Some(s)) {
    s.len()   // s is available here
}

---

Generics

• Composite types (e.g. List, Map) are generic
• Type parameters may be inferred locally

fn f() -> List<Int> {
    List::empty()
}

---

Interfaces

• Interfaces introduce constraints, not concrete types
• Values may be erased to an interface type

let d: Drawable = Point::origin();

• Interface values in collections are allowed
• Method calls on interface values introduce trait constraints

---

Type system representation

Core entities

• TypeId
• TypeVarId
• Constraint
• ConstraintSource
• ExprId

Expression identity

• Each expression is assigned an ExprId

• Mapping:

  • SpanId -> ExprId
  • ExprId -> TypeInfo

• Syntax tree remains unchanged

• Semantic data is stored in side tables

---

Constraint sources

Each constraint records where it came from:

• Operator usage (+, >, etc.)
• Function or method calls
• Interface method calls
• Branch joins
• Assignment
• Return expressions
• Semicolon coercions
• Explicit type annotations

This enables Rust-like diagnostics:

error: mismatched types
  |
2 | vec.push(1)
  |           inferred Vec<Int> here
3 | vec.push(false)
  |           expected Int, found Bool

---

Cycles & resolution

• Constraints may not form chains or cycles

• Resolution uses unification with:

  • Occurs-check (detecting constraint cycles)
  • Deferred resolution for unresolved type variables

• Cycles that cannot be resolved are reported with full provenance

---

Outputs of the type checker

The static typing pass produces:

• ExprId -> TypeInfo

  • original type
  • final (coerced) type

• ExprId -> ConstraintSources

• A list of diagnostics with spans

• A stable data model usable by:

  • Interpreter
  • LSP
  • Future optimizations