# 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 ✅ COMPLETE

**Goal**: Minimal viable compiler

- [x] Lexer and parser for core syntax
- [x] AST representation
- [x] Basic type checker (Hindley-Milner inference)
- [x] Interpreter for testing semantics
- [x] REPL with history, completions, syntax highlighting

**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 ✅ COMPLETE

**Goal**: First-class algebraic effects

- [x] Effect declarations
- [x] Effect signatures on functions
- [x] Handler definitions
- [x] `run ... with` syntax
- [x] Effect inference within function bodies
- [x] Effect polymorphism
- [x] Built-in effects (Console, Fail, State, Random, File, Http, Time, Process, Test)

**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 ⚠️ PARTIAL

**Goal**: Compile to a real target

- [x] C backend (basic functions, Console.print)
- [ ] C backend extensions (closures, lists, pattern variables)
- [ ] JavaScript backend
- [ ] WASM backend
- [ ] Optimization passes

**Deliverable**: Compiled programs that run natively or in browser

**Current**: `lux compile <file>` compiles to C code. Compile and run with `--run` flag.

### Phase 3: Schema Evolution ⚠️ PARTIAL

**Goal**: Versioned types with migrations

- [x] Version annotations on types (`@v1`, `@v2`)
- [x] Migration syntax (`from @v1 = ...`)
- [x] Version constraints (`@v2+`, `@latest`)
- [x] Runtime versioned values
- [x] Schema registry & compatibility checking
- [ ] Type system integration (versions partially ignored in typechecker)
- [ ] Auto-migration generation
- [ ] Codec generation

**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 ⚠️ PARTIAL

**Goal**: Property specifications and verification

- [x] Property syntax (`is pure`, `is total`, `is idempotent`, etc.)
- [x] Built-in properties parsing
- [x] Pure function checking (no effects)
- [ ] Total function verification
- [ ] Idempotent verification
- [ ] Deterministic verification
- [ ] Where clause enforcement
- [ ] SMT solver integration (Z3)
- [ ] Property-based test generation
- [ ] `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 ✅ MOSTLY COMPLETE

**Goal**: Usable for real projects

- [x] Standard library (List, String, Option, Result, Math, Json modules)
- [x] LSP server (diagnostics, hover, completions)
- [x] REPL with history, tab completion, syntax highlighting
- [x] Formatter
- [x] Watch mode / hot reload
- [x] Basic debugger
- [x] Module system (imports, exports, aliases)
- [ ] Package manager (manifest parsing exists, not fully functional)
- [ ] Documentation generator
- [ ] Profiler

### Phase 6: Advanced Features

**Goal**: Full language vision

- [x] HTTP client effect
- [x] HTTP server effect
- [x] File system effect
- [x] Process/shell effect
- [x] Test effect (native testing framework)
- [ ] Database/SQL effect
- [ ] Incremental computation
- [ ] Distributed effects (location-aware)
- [ ] Proof assistant mode

---

## Resolved Design Decisions

### Syntax (Decided)

- [x] Braces for blocks, not significant whitespace
- [x] Effect syntax: `with {E1, E2}`
- [x] Version syntax: `@v1`, `@v2+`, `@latest`

### Semantics (Decided)

- [x] Deep handlers (algebraic effect style with resume)
- [x] Structural compatibility for records
- [x] Best-effort property verification (gradual)

### Pragmatics (In Progress)

- Primary target: Tree-walking interpreter (default), C backend for compilation
- FFI: Shell commands via Process effect
- [ ] JavaScript backend for browser use

---

## 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)