Type System

1. Abstract

This RFC specifies Aura’s static type system: nominal class/interface types, nullability (T vs T?), generics with monomorphization, subtyping via inheritance and interface implementation, local type inference, overload resolution, flow-sensitive narrowing, and soundness goals.

It assumes the surface from RFC-001 and leaves runtime representation details to RFC-004 / RFC-006.

Toolchain today (2026-08-11, production gate): nominal classes/interfaces/struct/enum, inheritance with virtual dispatch, monomorphized generics + bounds, local null flow + !! / ?: / ?., type-argument inference, fun types/Ty::Fun, lambdas with value and reference captures, scoped nonowning ref T with lexical escape checks, borrow-safe Array field returns, generic HOFs, recursive multi-level nested generic substitution in sema and codegen, Array<Interface>, shared owned mutable var captures for class/Array/Fun, snapshot and epoch-invalidated live collection iterators, key-based and invalidation-checked live HashMap entry mutation, async/task types with borrow barriers, formatter/structured diagnostics/test reports, and Result-based std.io wrappers. Overload resolution covers top-level functions, class/companion methods, interface methods, constructors, defaults, varargs, generic bounds, and ambiguity diagnostics. Mutable ref mut T, nullable references, and nested references are deliberately rejected with stable diagnostics; general async ownership is complete for the supported owned values and task boundaries. Escaping mutable Array captures use an owned shared-cell contract rather than borrowed views; ref T remains non-escaping and separately checked.

2. Motivation

2.1 Problem statement

A Java-like object model without modern nullability recreates classic NPE classes of bugs. A Go-like GC language without a strong static system shifts defects to production. Aura needs a sound-enough, ergonomic system that matches RFC-000 decisions.

2.2 Why now

Type rules gate compiler architecture, stdlib signatures, and reflection reification policy.

2.3 Success metrics

3. Goals

• Static type checking as default for all Aura code.
• Expressive generics without unbounded type-level Turing tar pits (policy budget).
• Clear, teachable subtyping (nominal + interfaces).
• First-class nullability and Result integration.
• Coherent overloading and method resolution rules.

4. Non-goals

• Full dependent types.
• Gradual typing / any as a production default (may have dyn later—not v1).
• Higher-kinded types in v1.
• Structural typing as the default (optional structural records later).
• General ownership/borrow types as the default model; C21 ships only a scoped non-owning ref MVP.

5. Prior art & alternatives

6. Design

6.1 Overview

Aura is nominally typed with a single inheritance hierarchy for classes and multiple interface implementation. Subtyping is explicit (extends/implements), not inferred from shape.

Nothing  <:  all types          (bottom)
T        <:  T?
ClassS   <:  ClassT             if S extends T (transitively)
ClassC   <:  I                  if C implements I

Any (top for references) exists for rare heterogeneous APIs; prefer generics.

6.2 Type kinds

Higher-kinded types: not in v1.
Existentials / opaques: type Handle = opaque Long or package-private class—lean simple opaque alias later.

6.3 Nullability & error types

Nullability

• T is non-null for reference types. Assigning null is a type error.
• T? accepts T or null.
• Dereference / method call on T? requires: safe call ?., explicit check + smart cast, ?:, or !!.
• Primitives are non-null; use Int? for optional primitives (boxed/nullable representation).

Lattice (simplified): Nothing <: T <: T? <: Any? (details refined in formalization).

Errors

Exceptions are unchecked: function types do not list throws. Documentation/@throws may exist for tooling but is not type-enforced in v1.

Result is a nominal generic sum type in prelude/stdlib:

enum Result<T, E> {
  case Ok(value: T)
  case Err(error: E)
}

6.4 Subtyping & assignability

Assignability S assignable to T when S <: T after nullability adjustment.

Class subtyping: single inheritance; transitive.
Interface subtyping: if I : J, then I <: J. Implementing class is subtype of each interface.
Variance:

Boxing: primitives convert to/from wrapper types only where defined (minimal implicit; prefer explicit conversions).

6.5.1 C21 borrow/ref direction (selected)

C21 adopts a deliberately small, non-owning reference track to make Array field returns and collection views explicit. The proposed MVP surface is:

fun first(items: Array<Int>): Int {
  val item: ref Int = ref items.get(0)
  return item
}

ref T is an ephemeral, non-null, immutable borrow of an existing T. ref mut T is reserved and rejected; mutable access uses owned var cells or an explicit collection mutation API. A borrow may be created only from an addressable local, parameter, or field, may be used within the owner's lexical scope, and is never an owning value. clone() or an explicit owning move remains the escape hatch when a value must outlive its owner.

Runtime impact is limited to borrow-aware sema metadata and codegen of a non-owning pointer/view whose use is bounded by a checked lifetime. The GC remains responsible for owning objects; the MVP adds no reference counting, pinning, scheduler, or collector changes.

The production boundary rejects mutable borrows, borrow storage in heap objects, nullable or nested references, and references escaping through returns/closures/tasks. These are finalized non-goals for this release, not implicit or undocumented behavior. HashMap.entry(key) is a separate key-based owning handle, not a permission granted by ref to mutate through a borrowed collection entry.

6.5.2 C22 suspension and task borrow barriers

The C21 lifetime rule extends to every operation that can retain a value beyond the current synchronous expression. A ref T must be rejected when it would:

These checks are structural, not data-flow guesses: an operation's operand and the boundary token are both available to diagnostics. An owned value that is created before the boundary is valid, subject to ordinary type checking.

The stable diagnostic family is E-BORROW-ASYNC-ESCAPE. Its message is borrowed value cannot cross {operation} boundary, where {operation} is one of await, spawn, send, receive, or task storage. The primary span is the borrowed expression; the diagnostic includes a secondary boundary span and the note use an owned value (for example, clone()) before this boundary.

6.5 Generics

class Box<T>(var value: T)

interface Repo<T> where T : Entity {
  fun get(id: Id): T?
}

fun <T> identity(x: T): T = x

• Bounds: T : ClassOrInterface and multiple bounds T : A, B.
• Where clauses for complex constraints.
• Associated types: not v1 (use generic params).
• Specialization: not user-facing v1; compiler may specialize.
• Const generics: not v1.
• Implementation: monomorphization for concrete type args at codegen; interface-typed values use vtable / fat pointers as needed (RFC-004).

Reification at runtime: limited—see RFC-009. Prefer TypeToken/reified only if introduced later; v1 reflection may see erased interface views but mono preserves concrete layout in native code.

6.6 Type inference

• Bidirectional checking: check vs infer modes.
• Locals: infer from initializer.
• Generics: infer from arguments and expected type; explicit args when ambiguous.
• Returns: infer for expression-bodied locals; public API should state return types (style; may be enforced by lint).
• Lambdas: parameter types from expected functional interface / function type.
• No global HM inference across modules.

Ambiguity → hard error with candidate list (overloads/generics).

6.7 Interfaces & method resolution

• Interfaces may declare methods and default implementations.
• Method resolution: receiver static type → applicable members → most specific override; for interfaces, specificity rules + conflict error if two defaults collide without override.
• Orphan rule (locked): an implements / interface implementation for class C and interface I must live in the same package as C or the same package as I. No third-party packages may add implementations for foreign class + foreign interface pairs.
• Marker interfaces: empty interfaces allowed (Sendable-like names if needed—race model may not need them).

6.8 Flow-sensitive typing

After:

if (x is String) {
  // x : String
}
if (x != null) {
  // x : T when x was T?
}

Smart casts apply to stable locals (val) and limited var (not assigned in between). Fields are not smart-cast in place—copy to a local (val t = this.field) or use pattern matching.

Exhaustiveness: match on enums and sealed hierarchies must be complete or include else.

6.9 Type-level programming budget

Allowed: generics, bounds, associated constants no, type aliases, simple conditional types no.
Forbidden in v1: arbitrary Turing-complete type computation, HKTs, full dependent types.

6.10 Interop with reflection (RFC-009)

• Runtime type tokens for classes that opt into metadata retention.
• Generic concrete mono instances need not reify all type args unless metadata requested.
• Casts checked against runtime class metadata when available; otherwise best-effort + unsafe.

6.11 Examples

fun len(s: String?): Int {
  if (s == null) return 0
  return s.length()  // s : String
}

fun <T : Comparable<T>> max(a: T, b: T): T {
  return if (a.compareTo(b) >= 0) a else b
}

fun parseInt(text: String): Result<Int, ParseError> {
  // ...
  return Result.ok(42)
}

6.12 Error model / edge cases

6.13 Compatibility & migration

• Adding a method to an interface is a breaking change unless defaulted.
• Generic variance annotations are part of public ABI of source.
• Edition may tighten inference or nullability edge cases.

7. Open questions

8. Rationale & trade-offs

Nominal typing fits Java-like classes and stable APIs. Nullability as types eliminates an entire defect class at modest annotation cost. Monomorphization favors native perf and simpler GC type layouts at the cost of code size—mitigated by LLVM and incremental builds. Rejecting HKTs and global inference keeps the compiler and mental model implementable for MVP. Unchecked exceptions + Result matches RFC-000 without Java’s checked-exception fatigue.

9. Unresolved / future work

• Formal soundness proof sketch
• Variance inference vs annotation-only
• Gradual/dyn story post-v1
• Reified generics for reflection ergonomics

10. Security & safety considerations

• Type confusion via bad casts is a security boundary; prefer checked as.
• !! and unsafe casts must be auditable.
• Reflection-based access must respect visibility (RFC-009) or require privilege.

11. Implementation plan (optional)

12. References

• RFC-001, RFC-003, RFC-009
• TAPL (Pierce); Kotlin type system docs; Java generics (contrast erasure)

Changelog