lux/SKILLS.md

# Lux Language Skills & Implementation Plan

## Table of Contents

1. [Effect System](#1-effect-system)
2. [Schema Evolution](#2-schema-evolution)
3. [Behavioral Types](#3-behavioral-types)
4. [Type System Foundation](#4-type-system-foundation)
5. [Implementation Roadmap](#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

```lux
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`:

```lux
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:

```lux
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

```lux
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:

```lux
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:

```lux
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:

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

#### Built-in Effects

```lux
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

```lux
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

```lux
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:

```lux
-- 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

```lux
-- 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

```lux
-- 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

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

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

#### API Versioning

```lux
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

```lux
-- 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

```lux
-- 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

```lux
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

```lux
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

```lux
-- 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:

```lux
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:

```lux
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:

```lux
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:

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

### Property Propagation

Properties flow through composition:

```lux
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
```

```lux
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

```lux
-- 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

```lux
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

```lux
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

```lux
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

```lux
-- 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

```lux
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

```lux
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

```lux
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

```lux
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)