lux/SKILLS.md

Lux Language Skills & Implementation Plan

Table of Contents

1. Effect System
2. Schema Evolution
3. Behavioral Types
4. Type System Foundation
5. Implementation Roadmap

---

1. Effect System

Overview

Effects make side effects explicit, trackable, and testable. Every function declares what it can do. Handlers interpret effects at runtime.

Core Concepts

Effect Declarations

effect Http {
  fn get(url: String): Response
  fn post(url: String, body: Bytes): Response
}

effect Database {
  fn query<T>(q: Query<T>): List<T>
  fn execute(q: Command): Int
}

effect Logger {
  fn log(level: Level, message: String): Unit
}

effect Async {
  fn await<T>(future: Future<T>): T
  fn spawn<T>(action: fn(): T): Future<T>
}

Effect Signatures

Functions declare their effects after with:

fn fetchUsers(): List<User> with {Database, Logger} =
  Logger.log(Info, "Fetching users")
  Database.query(selectAllUsers)

-- Multiple effects compose naturally
fn syncUsers(source: Url): Int with {Http, Database, Logger} =
  let users = Http.get(source) |> parseUsers
  Logger.log(Info, "Syncing {users.len} users")
  users |> List.map(upsertUser) |> List.sum

Effect Handlers

Handlers provide implementations:

handler realHttp: Http {
  fn get(url) = httpClientGet(url)
  fn post(url, body) = httpClientPost(url, body)
}

handler mockHttp(responses: Map<String, Response>): Http {
  fn get(url) = responses.get(url).unwrapOr(Response.notFound)
  fn post(url, _) = responses.get(url).unwrapOr(Response.notFound)
}

handler postgresDb(conn: Connection): Database {
  fn query(q) = conn.execute(q.toSql) |> parseRows
  fn execute(q) = conn.execute(q.toSql)
}

Running Effects

fn main(): Unit with {Console} =
  let users = run fetchUsers() with {
    Database = postgresDb(openConnection()),
    Logger = consoleLogger
  }
  Console.print("Found {users.len} users")

Effect Features

Effect Polymorphism

Write code generic over effects:

fn withRetry<E, T>(action: fn(): T with E, attempts: Int): T with E =
  match attempts {
    0 => panic("Retry exhausted"),
    n => try action() catch _ => withRetry(action, n - 1)
  }

Effect Constraints

Require specific effects:

fn transactional<T>(action: fn(): T with {Database}): T with {Database} =
  Database.execute(begin)
  let result = try action() catch e => {
    Database.execute(rollback)
    throw e
  }
  Database.execute(commit)
  result

Effect Inference

Effects can be inferred within function bodies, but signatures must be explicit:

fn helper() with {Logger} =       -- explicit signature
  let x = compute()               -- effect-free, inferred
  Logger.log(Debug, "x = {x}")    -- Logger effect used
  x

Built-in Effects

effect Fail {
  fn fail<T>(error: Error): T     -- early return / exceptions
}

effect State<S> {
  fn get(): S
  fn put(s: S): Unit
  fn modify(f: fn(S): S): Unit
}

effect Reader<R> {
  fn ask(): R
}

effect Random {
  fn int(range: Range<Int>): Int
  fn float(): Float
  fn shuffle<T>(list: List<T>): List<T>
}

effect Time {
  fn now(): Instant
  fn sleep(duration: Duration): Unit
}

Effect Semantics

• Lexical handling: Effects are handled at run boundaries
• Order independence: Multiple effects can be handled in any order
• Resumable: Handlers can resume computations (algebraic effect style)
• Zero-cost goal: Handlers inline when statically known

---

2. Schema Evolution

Overview

Types change over time. Data persists. Lux tracks type versions and ensures compatibility at compile time.

Core Concepts

Versioned Types

type User @v1 {
  name: String,
  email: String
}

type User @v2 {
  name: String,
  email: String,
  createdAt: Timestamp
}

Compatibility Rules

Auto-compatible changes (no migration needed):

• Adding optional fields
• Adding fields with defaults
• Widening numeric types (Int32 -> Int64)
• Adding enum variants (for extensible enums)

Breaking changes (require explicit migration):

• Removing fields
• Renaming fields
• Changing field types
• Removing enum variants

type User @v3 {
  fullName: String,               -- renamed from 'name'
  email: String,
  createdAt: Timestamp,

  -- Explicit migration required
  from @v2 = {
    fullName: v2.name,
    email: v2.email,
    createdAt: v2.createdAt
  }
}

Migration Chains

Migrations compose automatically:

-- Reading @v1 data as @v3:
-- 1. @v1 -> @v2 (auto: createdAt gets default)
-- 2. @v2 -> @v3 (explicit: name -> fullName)

fn loadLegacyUser(data: Bytes): User @v3 =
  Codec.decode<User>(data)        -- handles any version

Version Constraints

-- Accept any version >= @v2
fn processUser(user: User @v2+): Unit = ...

-- Accept exactly @v3
fn processUserV3(user: User @v3): Unit = ...

-- Return latest version
fn createUser(name: String): User @latest = ...

Schema Features

Serialization

-- Encode with version tag
let bytes = Codec.encode(user)    -- includes version marker

-- Decode to specific version (migrates if needed)
let user: User @v3 = Codec.decode(bytes)

-- Decode to any compatible version
let user: User @v2+ = Codec.decode(bytes)

Database Integration

table users: User @v3 {
  primaryKey: id,
  index: [email]
}

-- Compiler generates migration SQL when version changes
-- Or errors if migration is ambiguous

API Versioning

endpoint getUser: GET "/users/{id}" -> User @v2

-- Later: update endpoint
endpoint getUser: GET "/users/{id}" -> User @v3
  -- Compiler: "Breaking change for clients expecting @v2"
  -- Must either:
  -- 1. Keep old endpoint as getUser_v2
  -- 2. Prove @v3 is wire-compatible with @v2

Compatibility Checking

-- Compile-time compatibility proof
assert User @v2 compatibleWith User @v1  -- passes
assert User @v3 compatibleWith User @v1  -- fails: breaking change

-- Generate compatibility report
lux schema diff User @v1 User @v3
-- Output:
-- - 'name' renamed to 'fullName' (breaking)
-- - 'createdAt' added with default (compatible)

Schema Semantics

• Versions are types: User @v1 and User @v2 are distinct types
• Migrations are functions: from @v1 is a function @v1 -> @v2
• Compatibility is decidable: Compiler checks all rules statically
• Wire format is stable: Version tag + canonical encoding

---

3. Behavioral Types

Overview

Properties beyond input/output types. Express and verify behavioral guarantees like purity, totality, idempotency.

Core Concepts

Built-in Properties

-- Purity: no effects
fn add(a: Int, b: Int): Int
  is pure
= a + b

-- Totality: always terminates, no exceptions
fn safeDiv(a: Int, b: Int): Option<Int>
  is total
= if b == 0 then None else Some(a / b)

-- Idempotency: f(f(x)) == f(x)
fn normalize(s: String): String
  is idempotent
= s.trim.lowercase

-- Determinism: same inputs -> same outputs
fn hash(data: Bytes): Hash
  is deterministic

Refinement Types

type PositiveInt = Int where self > 0
type NonEmptyList<T> = List<T> where self.len > 0
type Email = String where self.matches(emailRegex)

fn head<T>(list: NonEmptyList<T>): T
  is total                        -- can't fail: list is non-empty
= list.unsafeHead

fn sqrt(n: PositiveInt): Float
  is total                        -- can't fail: n is positive

Output Refinements

fn sort<T: Ord>(list: List<T>): List<T>
  is pure,
  is total,
  where result.len == list.len,
  where result.isSorted,
  where result.isPermutationOf(list)

fn filter<T>(list: List<T>, pred: fn(T): Bool): List<T>
  is pure,
  is total,
  where result.len <= list.len,
  where result.all(pred)

Property Requirements

-- Require properties from function arguments
fn retry<F, T>(action: F, times: Int): Result<T, Error>
  where F: fn(): T with {Fail},
  where F is idempotent           -- enforced at call site!
= ...

fn memoize<F, A, B>(f: F): fn(A): B with {Cache}
  where F: fn(A): B,
  where F is pure,
  where F is deterministic
= ...

fn parallelize<F, T>(actions: List<F>): List<T> with {Async}
  where F: fn(): T,
  where F is commutative          -- order-independent
= ...

Verification Levels

Level 1: Compiler-Proven

Simple properties proven automatically:

fn double(x: Int): Int
  is pure                         -- proven: no effects
= x * 2

fn always42(): Int
  is total,                       -- proven: no recursion, no failure
  is deterministic                -- proven: no effects
= 42

Level 2: SMT-Backed

Refinements checked by SMT solver:

fn clamp(x: Int, lo: Int, hi: Int): Int
  where lo <= hi,
  where result >= lo,
  where result <= hi
= if x < lo then lo else if x > hi then hi else x
-- SMT proves postconditions hold

Level 3: Property-Tested

Complex properties generate tests:

fn sort<T: Ord>(list: List<T>): List<T>
  where result.isPermutationOf(list)    -- too complex for SMT
-- Compiler generates: forall lists, sort(list).isPermutationOf(list)
-- Runs as property-based test

Level 4: Assumed

Escape hatch for unverifiable properties:

fn externalSort<T: Ord>(list: List<T>): List<T>
  assume is idempotent            -- trust me (FFI, etc.)
= ffiSort(list)

Property Propagation

Properties flow through composition:

fn f(x: Int): Int is pure = x + 1
fn g(x: Int): Int is pure = x * 2

fn h(x: Int): Int is pure = f(g(x))   -- inferred pure

fn f(x: Int): Int is idempotent = x.abs
fn g(x: Int): Int is idempotent = x.abs  -- same function

-- Composition of idempotent functions is idempotent IF they're the same
-- or if one is a fixpoint of the other. Otherwise, not guaranteed.
fn h(x: Int): Int = f(g(x))       -- NOT automatically idempotent

---

4. Type System Foundation

Core Types

-- Primitives
Int, Int8, Int16, Int32, Int64
UInt, UInt8, UInt16, UInt32, UInt64
Float, Float32, Float64
Bool
Char
String

-- Collections
List<T>
Set<T>
Map<K, V>
Array<T>                          -- fixed size

-- Optionality
Option<T> = None | Some(T)
Result<T, E> = Err(E) | Ok(T)

-- Tuples
(A, B), (A, B, C), ...

-- Records
{ name: String, age: Int }

-- Functions
fn(A): B
fn(A, B): C
fn(A): B with {Effects}

Algebraic Data Types

type Color = Red | Green | Blue

type Tree<T> =
  | Leaf(T)
  | Node(Tree<T>, Tree<T>)

type Result<T, E> =
  | Ok(T)
  | Err(E)

Pattern Matching

fn describe(color: Color): String =
  match color {
    Red => "red",
    Green => "green",
    Blue => "blue"
  }

fn sum(tree: Tree<Int>): Int =
  match tree {
    Leaf(n) => n,
    Node(left, right) => sum(left) + sum(right)
  }

Type Classes / Traits

trait Eq {
  fn eq(self, other: Self): Bool
}

trait Ord: Eq {
  fn cmp(self, other: Self): Ordering
}

trait Show {
  fn show(self): String
}

impl Eq for Int {
  fn eq(self, other) = intEq(self, other)
}

Row Polymorphism

-- Extensible records
fn getName(r: { name: String, ..rest }): String = r.name

-- Works with any record containing 'name'
getName({ name: "Alice", age: 30 })
getName({ name: "Bob", email: "bob@example.com" })

-- Extensible variants
type HttpError = { NotFound | Timeout | ..rest }

---

5. Implementation Roadmap

Phase 0: Foundation

Goal: Minimal viable compiler

• Lexer and parser for core syntax
• AST representation
• Basic type checker (no effects, no versions, no properties)
• Interpreter for testing semantics
• REPL

Deliverable: Can type-check and interpret pure functional programs

fn fib(n: Int): Int =
  if n <= 1 then n else fib(n-1) + fib(n-2)

Phase 1: Effect System

Goal: First-class algebraic effects

• Effect declarations
• Effect signatures on functions
• Handler definitions
• run ... with syntax
• Effect inference within function bodies
• Effect polymorphism
• Built-in effects (Fail, State, etc.)

Deliverable: Can define, handle, and compose effects

effect Console { fn print(s: String): Unit }

fn greet(name: String): Unit with {Console} =
  Console.print("Hello, {name}!")

fn main() =
  run greet("World") with { Console = stdoutConsole }

Phase 2: Code Generation

Goal: Compile to a real target

• IR design (effect-aware)
• Backend selection (LLVM, WASM, or JS)
• Effect handler compilation (CPS or evidence-passing)
• Optimization passes
• Runtime library

Deliverable: Compiled programs that run natively or in browser

Phase 3: Schema Evolution

Goal: Versioned types with migrations

• Version annotations on types (@v1, @v2)
• Compatibility checker
• Migration syntax (from @v1 = ...)
• Migration chaining
• Codec generation
• Version constraints (@v2+, @latest)

Deliverable: Types with automatic serialization and migration

type Config @v1 { host: String }
type Config @v2 { host: String, port: Int, from @v1 = { port: 8080, ..v1 } }

let cfg: Config @v2 = Codec.decode(legacyBytes)

Phase 4: Behavioral Types

Goal: Property specifications and verification

• Property syntax (is pure, where result > 0)
• Built-in properties (pure, total, idempotent, etc.)
• Refinement type checking
• SMT solver integration (Z3)
• Property-based test generation
• Property inference for simple cases
• assume escape hatch

Deliverable: Compile-time verification of behavioral properties

fn abs(x: Int): Int
  is pure,
  is total,
  where result >= 0
= if x < 0 then -x else x

Phase 5: Ecosystem

Goal: Usable for real projects

• Package manager
• Standard library
• LSP server (IDE support)
• Documentation generator
• REPL improvements
• Debugger
• Profiler

Phase 6: Advanced Features

Goal: Full language vision

• Database effect with schema-aware queries
• HTTP effect with API versioning
• Incremental computation (bonus feature)
• Distributed effects (location-aware)
• Proof assistant mode (optional full verification)

---

Open Design Questions

Syntax

• Significant whitespace vs braces?
• Effect syntax: with {E1, E2} vs !E1 + E2 vs <E1, E2>?
• Version syntax: @v1 vs v1 vs #1?

Semantics

• Effect handler semantics: deep vs shallow handlers?
• Version compatibility: structural or nominal?
• Property verification: sound or best-effort?

Pragmatics

• Primary compile target: native, WASM, JS?
• Interop story: FFI design?
• Gradual adoption: can you use Lux from other languages?

---

References

Effect Systems

• Koka language (Daan Leijen)
• Eff language (Matija Pretnar)
• "Algebraic Effects for Functional Programming" (Daan Leijen)
• Frank language (Sam Lindley)

Schema Evolution

• Protocol Buffers / Protobuf
• Apache Avro
• "Schema Evolution in Heterogeneous Data Environments"

Behavioral Types

• Liquid Haskell (refinement types)
• F* (dependent types + effects)
• Dafny (verification)
• "Refinement Types for Haskell" (Vazou et al.)

General

• "Types and Programming Languages" (Pierce)
• "Practical Foundations for Programming Languages" (Harper)