init lux

SKILLS.md

@@ -0,0 +1,734 @@
+# 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)