Where contracts meet effects
A JVM language with algebraic effects, runtime specs, and property-based contracts
v0.11.376JVMVirtual ThreadsANTLR4
Algebraic Effects
First-class effect system with deep handlers. Mock any side effect in tests — println, read-line, the clock and the dice included, since the builtins perform Console, Time and Random. State-machine bytecode lowering for hot perform-loops.
Parametric Effect Rows
Higher-order fns declare row variables: fold :: (Fn):eff _ _ _ ::: eff. The callback's effect row binds eff and propagates into the caller's row at each call site. Compile-time enforcement, no runtime erasure.
Runtime Specs
Malli-inspired specs replace types. Certify values at construction, validate at boundaries. Spec-annotated pub fns are mandatory; lint enforces it.
Contracts
Pre/post conditions on functions, in/out contracts at module boundaries. Blame tracking — pre-failure accuses the caller, post-failure accuses the implementation.
Structured Concurrency
scope/fork/await, par, race, timeout. Java virtual threads with auto-cancellation. Spawned fibers inherit effect row + session namespace.
Child Processes
std.proc runs a command to completion (stdin, timeout, both streams) or starts one and talks to it a line at a time. It is an effect like any other, so a test drives a whole pipeline of git, compilers and CLIs through a scripted handler.
Terminal UI
std.term gives raw mode, decoded key/mouse/resize events and wcwidth as an effect — so a mock handler makes a whole TUI assertable as a string, with no tty. The uzor seed builds cell buffers, layout, widgets and an app loop on top.
Pipeline Operators
|> pipeline, @ map, /? filter, /+ fold. >> composition, ~ apply-to-rest.
Module System & Packages
use mod.name :as alias, then alias.name — for specs, variants and effects too (:: m.Mode, ::: m.Tick); { selective } for a few constant names. Each file reaches only what it imports. Git deps via irij.toml. Pub/private exports. Effect-gated APIs.
Bytecode-only Execution
irij build emits a self-contained JAR. State-machine handler lowering is the single execution path — no interpreter, no threaded fallback, no ambiguity.
Hot Redef + Java Interop
REPL-driven fn redefinition via invokedynamic + MutableCallSite. Java classes via Class/member, objects via obj#member and method references (@ #toUpperCase); every Java site needs ::: JVM, checked at compile time — or sits behind a cap that performs a named effect (::: Db, not ::: JVM), and irij.toml [trust] confines Java to the modules it lists (irij audit).
Java Libraries
List any Maven library in irij.toml [jvm] at an exact version: it's fetched with its dependencies, pinned by sha256 in irij.lock, reached through a cap like the JDK, and shipped inside the irij build JAR. Databases too — std.jdbc speaks to SQLite, PostgreSQL, H2… through the driver you list. Seeds bring libraries only where [trust] jars allows.
Model-Based Testing
A model declaration binds a Quint specification to the code implementing it — one clause per action, with the spec's nondet picks bound by name. Quint generates traces, Irij replays them and fails at the first diverging step; Apalache proves invariants. Generating needs the quint binary, replaying a committed trace needs nothing, because the CLI is reached through an effect.
Install
Irij runs on the JVM. All you need is a JDK 21+ (any distribution) and git — the build fetches everything else. Linux, macOS and WSL are supported; on Windows use gradlew.bat instead of ./gradlew.
Build and install to PATH
## clone the repo
git clone https://github.com/aldebogdanov/irij.git
cd irij
## build + install the launcher
./gradlew install
This writes the runtime to ~/.local/lib/irij.jar and an irij launcher script to ~/.local/bin/irij. Make sure that directory is on your PATH:
## add to ~/.bashrc or ~/.zshrc
export PATH="$HOME/.local/bin:$PATH"
Prefer not to install? ./gradlew shadowJar alone leaves a runnable JAR at build/libs/irij.jar — run it with java -jar build/libs/irij.jar file.irj.
Verify and take it for a spin
irij --version ## engine version
irij ## interactive REPL
echo 'println "Hello, Irij!"' > hello.irj
irij hello.irj
Everyday commands
irij file.irj ## run a source file
irij test ## run tests/test-*.irj
irij test -v ## … listing every test
irij quint doctor ## check the quint toolchain
irij install ## fetch seeds from irij.toml
irij build ## package a self-contained JAR
irij publish ## publish a seed to the registry
irij lsp ## LSP server for editors
irij --nrepl-server ## nREPL on port 7888
irij help ## full command list
Editors
VS Code
editors/vscode/ — highlighting, the language server (diagnostics, hover, go to definition, completion, expand selection) and a terminal REPL (Cmd/Ctrl+Enter sends the form at the cursor). Build it there with npm install && npm run package, then code --install-extension irij-*.vsix.
Emacs
editors/emacs/ — irij-mode.el (highlighting, offside indentation, eglot / lsp-mode wiring — start one with (add-hook 'irij-mode-hook #'lsp-deferred) or #'eglot-ensure), irij-nrepl.el (inline eval) and irij-selection.el (expand/shrink region along the syntax tree, also on puni's and expand-region's keys).
TextMate grammar
Anything else that reads TextMate grammars (Sublime Text, Zed, Shiki): editors/textmate/irij.tmLanguage.json.
Code Examples
Specs & Pattern Matching
spec Shape
Circle Float
Rect Float Float
fn area :: Shape Float
Circle r => 3.14159 * r * r
Rect w h => w * h
println (area (Circle 5.0))
;; 78.53975
Algebraic Effects
effect Logger
log :: Str -> ()
handler console :: Logger ::: Console
log msg =>
println msg
resume ()
with console
log "Starting..."
log "Done!"
Parametric Effect Rows
;; Row-variable `:eff` binds the callback's effects
;; and propagates them to the caller's effect row.
fn fold :: (Fn):eff _ Vec _ ::: eff
(f acc xs -> ...)
;; Pure use — no extra row at the call site.
total := fold (+) 0 #[1 2 3 4 5]
;; Effectful callback — Console flows in automatically.
fn shout ::: Console
=>
sum := fold (acc n -> println n ; acc + n) 0 #[1 2 3]
println sum
Contracts (pre / post / in / out)
fn withdraw :: Account Int Account
pre (account amt -> amt > 0)
post (result -> result.balance >= 0)
(account amt ->
{...account balance= account.balance - amt})
;; Blame-tracking: pre-fail accuses caller,
;; post-fail accuses the fn itself.
Pipelines & Seq Ops
nums := #[1 2 3 4 5 6 7 8 9 10]
result := nums
|> /? (n -> n > 3)
|> @ (n -> n * n)
|> /+
println result
;; 355
Structured Concurrency
scope s
a := s.fork (-> fetch "users")
b := s.fork (-> fetch "posts")
merge (await a) (await b)
;; Composable combinators
sum := par (+) (-> slow-calc 1) (-> slow-calc 2)
winner := race (-> slow) (-> fast)
ok := timeout 1000 (-> work)
Functions
;; Three fn body styles:
fn greet ::: Console ;; imperative
=> name
msg := "Hello, " ++ name
println msg
msg
fn add (x y -> x + y) ;; lambda
fn fib
0 => 1 ;; match arms
n => n * fib (n - 1)
Collections & Records
vec := #[1 2 3]
set := #{:a :b :c}
tup := #(42 "hello")
person := {name= "Alice" age= 30}
;; Immutable update
older := {...person age= 31}
;; Mutable opt-in
counter :! 0
counter <- counter + 1
Protocols
proto Show a
show :: a -> Str
impl Show for Int
show := (n -> to-str n)
impl Show for Vector
show := (v -> "[" ++ (join ", " (@ to-str v)) ++ "]")
println (show 42)
println (show #[1 2 3])
Model-Based Testing
;; a Quint spec generates the traces; Irij replays them
model bank :: "spec/bank.qnt" :pure
start => {balances= {alice= 0}}
deposit st who amount => {...st balances= (credit st.balances who amount)}
overdraft st _ _ => {...st last-error= "no funds"}
r1 := test "bank conforms" (-> qcheck bank {traces= 50})
;; diverged at step 4, action deposit
;; expected {alice= 11} actual {alice= 12}
Roadmap
Irij is in active development. Current status:
donePhase 0-2 Parser, AST, REPL, CLIdonePhase 3 Algebraic effects with deep handlersdonePhase 4 Module system + standard librarydonePhase 5 Structured concurrency (virtual threads)donePhase 6 Contracts, blame trackingdonePhase 7 Effect row declarations + enforcementdonePhase 8 Runtime specs, validation, lintdonePhase 9 Package management (deps.irj, git deps)donePhase 10 I/O: JSON, FileIO, HTTP client + serverdonePhase 11 Database effect (SQLite, std.db)donePhase 12 Package registry app + PlaygrounddonePhase 13 Java interop (Class/member, dot-access)donePhase 14 Bytecode compiler: state-machine effects, hot-redef, JVM capabilitydonev0.5.0 Effect-row soundness; full bytecode spec parity; pre/post contracts in bytecodedonev0.5.x Bytecode-mode parity for the full irij.online website; Irij source line numbers in JVM stack tracesdonev0.6.0 Parametric effect rows ((Fn):eff / (_ -> Bool):eff / ::: eff)donev0.6.13 Interpreter package + threaded handler lowering removed. Single execution model: state-machine bytecode.donev0.6.15 Spawn inherits namespace + per-session stdout (Playground cross-eval fn refs + spawn output capture). SM lowering: composed handlers, destructure pre-op binds.donev0.7.0 std.auth seed (sha256, hmac, random-token); SM-lowering correctness gaps closed; dev.irij.interpreter renamed to dev.irij.runtime; release auto-tagdonev0.7.1 Capabilities replace raw-* surface (Db, Http, Serve, FileIO, Session); Irij-record caps; named record specs with row params; inline `with do …`; LSP MVP (irij lsp)donev0.8.0 Handler:Effect specs (first-class handler values, dynamic-handler typing); LSP 2b.1 (symbol-aware hover, goto-def, identifier completion, effect-row diagnostics)donev0.8.1 Per-request HTTP handlers inherit caller's effect stack (SSE / multipart now work); `try` traps every Throwable (division by zero, casts, NPEs); GraalVM deferred to techdebtdonev0.8.2 Patch: empty-body HTTP responses send -1 length cleanly (redirects, 204s, errors from `irij publish`)donev0.8.3 `Map` spec accepts records (Tagged with namedFields); vrata-style `El`/`Node` flow through `:: Map` boundaries without ceremonydonev0.8.4 `with` + tail `if/else` returns the branch value (EffIR lowering); snake_case identifiers lex as one IDENT (SQL/JSON field names)donev0.8.5 Multi-class emission: inlined-module fns compile into per-source-file classes, so JVM stack frames name the right .irj instead of the root programdonev0.8.6 SSE "patch once" responses (a handler that patches and returns no longer crashes); `irij publish` Bearer authdonev0.8.7 `with` blocks whose tail is a block-form if/else return the branch value in every shape (EffIR + pure/SM paths)donestd.term Terminal effect: raw mode, decoded key/mouse/resize events, wcwidth, alt-screen. JLine-backed cap; escape decoding sits outside it so the grammar is testable with no tty. `mock-term` makes a whole TUI assertable as a string.doneLanguage fixes `party` replaces `role` as the choreography keyword (frees `user.role`); integer division/remainder are `quo`/`rem` (the old `mod` builtin was unreachable — the module keyword owned the name); `&&`/`||` short-circuit; product specs validate field types and are closed; `\e` string escapedoneMulti-tenant registry Users, sessions, API tokens, per-owner ownership; auth-gated publish; Datastar dashboard with token CRUDdonechereda Queue effect + SQLite cap; at-least-once with optional dedup keys; first opt-in seednextchereda-redis Redis backend for chereda; opt-in jedis dep gated by seed importdonebutterfly Reactive signal graph in Irij: signals, cached computes with automatic dependency tracking, watchers, batching, snapshot/restore time traveldoneuzor Terminal UI toolkit on std.term: cell buffers with per-line diffing, constraint layout, widgets, an app loop, mouse, overlays and themes — the rendering path is pure, so a whole TUI is tested without a terminaldonev0.9.0 Model-based testing: the `model` declaration binds a Quint specification to the code implementing it, `std.quint` replays generated traces and `verify` proves invariants with Apalache. Generation is an effect, so a committed trace replays in CI with no Quint installed. Replaces the `law` property testing removed in v0.6.12 — sampling is not proof, and the tool that samples also proves.donev0.9.235 std.proc: child processes as an effect (run to completion, or start and stream a line at a time); program arguments (`irij app.irj a b`, built jars) via std.env's env-args; Java methods on hidden JDK classes resolve through their public supertype; `model` is a keyword only at a declaration headdonev0.9.236 Keywords are field names: `cand.spec`, `{with= …}`, product-spec fields and destructuring — data decoded from JSON or a Quint spec names its fields freelydonev0.9.237 `try` and `on-failure` hand back the raised value: `error {code= :missing}` stays a map through `try`, fibers and Java calls, so callers match on fields instead of parsing textdonev0.9.239 `conj` adds to a Set; a pure `model` may name a `view` that renders state the way the spec's variables look, so a kernel with its own representation replays Quint traces directlydonev0.9.270 Security audit: `serve` hands out only resources/, PBKDF2 password hashes, a stoppable playground, safe seed fetching; Int never overflows; rationals (`2/3`); a module's names are its own; persistent vectors, maps and sets (building one element at a time is linear); piped `read-line`donev0.9.273 Compile errors name functions as written and say which file they come fromdonev0.9.275 `with m.handler` works inside another `with`donev0.9.277 Imports are enforced: a file reaches only what it declares, imports or has as a builtin, and each error names the `use` line to add; a local shadows an alias; `pub use` re-exportsdonev0.9.279 Top-level code sees a top-level binding's current value, not its first onedonev0.9.299 Specs, variants and effects through an import alias (`:: m.Mode`, `m.Calm`, `::: m.Tick`), and std, tests and examples import qualified; effect ops in `match` arms and inline `if`s; each `if` branch is its own scope; definitions may share a builtin's name; `newtype` compilesdonev0.9.309 Editor tooling: a VS Code extension (highlighting, LSP, terminal REPL); the Emacs mode follows the lexer (offside indentation, eglot / lsp-mode); expand/shrink selection over the LSP; `irij repl` reads multi-line inputdonev0.9.314 The language server no longer reports a qualified effect (`::: proc.Proc`) as an unbound row variable; Emacs expand/shrink asks the server under lsp-mode toodonev0.9.330 `irij test` and `irij quint doctor` in colour, and `irij test -v` lists every test; Quint 0.33.0 is the tested version, its traces identical to 0.32.0's; in Emacs, puni's and expand-region's keys expand along the syntax treedonev0.9.332 `std.resource`: a `Resource` effect (`resource-read`, `resource-exists?`) gives a program read-only access to its own `resources/` — the jar's bundle after `irij build`, else the directory beside it — without granting the diskdonev0.9.346 `cond` and `case` for multi-way choice; `resume` is a clause's last step (code after it is a compile error), and a clause that doesn't resume aborts from any depth; lambdas take patterns (`#(a b) -> a + b`), `true`/`false` patterns match only themselves, record update keeps a product spec; self-calls in match arms are tail calls; `obj#member` for Java, `#member` method referencesdonev0.9.348 Hardening: hashes and signatures refuse a Str with no UTF-8 encoding (a lone surrogate signed as `?`); Datastar keys every payload line; the server decodes the path per segment and refuses `%2F`, dot segments and invalid escapes, `req.query` is raw (`req.params` decoded); `route-prefix` matches whole segments; `random-int` & co. answer from a `Random` handler; strict `parse-int`/`parse-float`; `percent-encode`donev0.9.351 Builtins perform their effects: `now-ms` and `sleep` answer from a `Time` handler, and `print`, `println` and `read-line` from a `Console` handler (new `std.console`), so a test captures output or runs a fake clock over code that calls the builtins directly; `sleep` refuses a Float or a negative countdonev0.9.353 Float literals take an exponent (`1.5e3`, `1e-9`); a builtin given the wrong number of arguments says so ("to-str takes 1 argument, given 2") instead of "Unknown function"; inline `with … do` nests and works inside an expression (`with a do (with b do (op ()))`, `1 + (with h do (op ()))`)donev0.9.357 Strings print quoted inside collections, variants and records (`#["a b" "c"]`, not `#[a b c]`), escaped so the output reads back as source; `inspect` gives that form for any value, and `dbg`, the REPL echo and `assert-eq` use itdonev0.10.365 Effect rows you can trust: a `with` needs its handler's row, so a pure function can't print, read the clock or reach Java through a handler; a call through a Java `cap` performs the cap's effect, so code that opens a database declares `::: Db`, not `JVM`; irij.toml `[trust]` confines Java to the modules it lists, `irij audit` shows every site; `unsafe-jvm` is deprecateddonev0.10.368 Specs check what they say: a name nothing declares is a compile error, not a spec that accepts everything; a variant's fields are checked where it is built (`Circle "x"` for `Circle Float` is refused); applied parametric specs (`(Maybe Int)`) and variant names (`Nickel`, `(Just Int)`) as specs; builtin `Result a e` — `Ok a` or `Err e`, what `try` returnsdonev0.11.373 Java libraries: irij.toml `[jvm]` names Maven coordinates, fetched with their dependencies and pinned by hash in `irij.lock`, shipped inside `irij build`'s JAR; seeds bring libraries only where `[trust] jars` allows; `irij deps`. `std.db` is now `std.jdbc` — any JDBC database, the driver a `[jvm]` library — and `irij.jar` drops from 18 MB to 8 MBplannedFuture Linear types (capability + channel safety); channels (send/recv/select); choreographic programming; refinement types; content-addressed code; multi-resume effects (search/nondet/probabilistic); GraalVM native image