Add automatic effect inference for functions and lambdas that don't
explicitly declare their effects. The implementation:
- Tracks inferred effects during type checking via `inferred_effects`
- Uses `inferring_effects` flag to switch between validation and inference
- Functions without explicit `with {Effects}` have their effects inferred
- Lambda expressions also support effect inference
- When effects are explicitly declared, validates that inferred effects
are a subset of declared effects
- Pure functions are checked against both declared and inferred effects
This makes the effect system more ergonomic by not requiring explicit
effect annotations for every function while still maintaining safety.
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Lux
A functional programming language with first-class effects, schema evolution, and behavioral types.
Vision
Most programming languages treat three critical concerns as afterthoughts:
- Effects — What can this code do? (Hidden, untraceable, untestable)
- Data Evolution — Types change, data persists. (Manual migrations, runtime failures)
- Behavioral Properties — Is this idempotent? Does it terminate? (Comments and hope)
Lux makes these first-class language features. The compiler knows what your code does, how your data evolves, and what properties your functions guarantee.
Core Principles
1. Effects Are Explicit and Composable
fn fetchUser(id: UserId): User with {Database, Http} =
let profile = Http.get("/users/{id}")
let prefs = Database.query(userPrefsQuery(id))
User.merge(profile, prefs)
-- Testing: swap real effects for mocks
test "fetchUser returns merged data" =
run fetchUser(testId) with {
Database = mockDb({ testId: testPrefs }),
Http = mockHttp({ "/users/{testId}": testProfile })
}
|> Assert.eq(expectedUser)
No hidden side effects. No dependency injection boilerplate. Effects are declared, handlers are swappable, composition just works.
2. Schema Evolution Is Built-In
type User @v1 {
name: String,
email: String
}
type User @v2 {
name: String,
email: String,
age: Option<Int> -- optional field: auto-compatible
}
type User @v3 {
fullName: String, -- renamed: requires migration
email: String,
age: Option<Int>,
from @v2 = { fullName: v2.name, ..v2 }
}
The compiler tracks compatibility. Breaking changes are compile errors. Migrations are code, not config.
3. Behavioral Types Are First-Class
fn retry<F, T>(action: F): Result<T, Error>
where F: fn() -> T with {Fail},
where F is idempotent -- enforced!
=
match action() {
Ok(v) => Ok(v),
Err(_) => action() -- safe: we know it's idempotent
}
fn sort<T: Ord>(list: List<T>): List<T>
is pure,
is total,
where result.len == list.len,
where result.isSorted
Properties like pure, total, idempotent, commutative are part of the type system. The compiler proves what it can, tests what it can't.
Example
-- Define an effect
effect Logger {
fn log(level: Level, msg: String): Unit
}
-- Define a versioned type
type Config @v1 {
host: String,
port: Int
}
type Config @v2 {
host: String,
port: Int,
timeout: Duration,
from @v1 = { timeout: Duration.seconds(30), ..v1 }
}
-- A function with explicit effects and properties
fn loadConfig(path: Path): Config @v2 with {FileSystem, Logger}
is total
=
Logger.log(Info, "Loading config from {path}")
let raw = FileSystem.read(path)
Config.parse(raw)
-- Run with handlers
fn main(): Unit with {Console} =
let config = run loadConfig("./config.json") with {
FileSystem = realFs,
Logger = consoleLogger
}
Console.print("Loaded: {config}")
Status
Current Phase: Prototype Implementation
The interpreter is functional with:
- Core language (functions, closures, pattern matching)
- Effect system (declare effects, use operations, handle with handlers)
- Type checking with effect tracking
- REPL for interactive development
See:
- SKILLS.md — Language specification and implementation roadmap
- docs/VISION.md — Problems Lux solves and development roadmap
- docs/OVERVIEW.md — Use cases, pros/cons, complexity analysis
Design Goals
| Goal | Approach |
|---|---|
| Correctness by default | Effects, schemas, and behaviors are compiler-checked |
| Incremental adoption | Start simple, add properties/versions as needed |
| Zero-cost abstractions | Effect handlers inline, versions compile away |
| Practical, not academic | Familiar syntax, clear errors, gradual verification |
Non-Goals
- Not a systems language (no manual memory management)
- Not a scripting language (static types required)
- Not a proof assistant (verification is practical, not total)
Building
Requires Rust 1.70+:
# Build the interpreter
cargo build --release
# Run the REPL
cargo run
# Run a file
cargo run -- examples/hello.lux
# Run tests
cargo test
Examples
See the examples/ directory:
hello.lux— Hello World with effectsfactorial.lux— Recursive functionseffects.lux— Custom effects and handlersdatatypes.lux— ADTs and pattern matchingfunctional.lux— Higher-order functions and pipes
Quick REPL Session
$ cargo run
Lux v0.1.0
Type :help for help, :quit to exit
lux> let x = 42
lux> x * 2
84
lux> fn double(n: Int): Int = n * 2
lux> double(21)
42
lux> [1, 2, 3] |> List.reverse
[3, 2, 1]
lux> List.map([1, 2, 3], double)
[2, 4, 6]
lux> String.split("a,b,c", ",")
["a", "b", "c"]
lux> Some(42) |> Option.map(double)
Some(84)
lux> :quit
Contributing
This project is in early design. Contributions welcome in:
- Language design discussions (open an issue)
- Syntax bikeshedding
- Semantic formalization
- Compiler implementation (once design stabilizes)
License
MIT