Extra

A modern, expressive programming language designed for building robust and scalable applications. Write cleaner code, faster.

Get Started

Refinement Types

Extra's refinement types let you define subsets of standard types with compile-time-enforced rules. Unlike TypeScript's nominal types or Rust's trait bounds, Extra uses set theory to express constraints like ranges, regex patterns, or exact collection sizes. These refinements propagate through conditionals, enabling branch-specific type narrowing.

type Port = Int(0..65535)
type IPv4 = Array(Int(0..255), length: =4)

let server: { ip: IPv4, port: Port } = {
  ip: [192, 168, 1, 256],
  port: 80
}

Literal Types as First-Class Types

In Extra, literals (true, 'hello', 42) are valid types. This enables exhaustive pattern matching and domain-specific type algebras (e.g., CSSColor = 'red' | 'blue' | HexCode). Combined with refinements, you can model business logic directly in the type system.

type PaymentStatus = "Pending" | "Paid" | "Failed"
type Payment = {
  amount: Float(>0),
  status: PaymentStatus
}

fn process(payment: Payment) -> String {
  switch (payment.status) {
    case: "Pending" => "⏳"
    case: "Paid"    => "✅"
    case: "Failed"  => "❌"
  }
}

Length-Aware Collections with Type Inference

Arrays, Dicts, and Sets track their lengths or key sets statically. Indexing becomes safe when paired with refinements, eliminating null checks. Extra also infers union types for heterogeneous collections while preserving type safety.

type User = { id: String, name: String }

fn insert_users(
  #users: Array(User, length: 1..100) 
): DatabaseResult {
  for (i in 0..users.length) {
    db.insert(users[i])
  }
}

insert_users([])
insert_users([{id: "1", name: "Extra"}])