Where contracts meet effects
A JVM language with algebraic effects, runtime specs, and property-based contracts
Algebraic Effects
First-class effect system with deep handlers. Mock any side effect in tests. 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.
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 :open / :as alias / { selective }. 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, dot-access, ::: JVM capability tracking.
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 installThis 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.irjEveryday commands
irij file.irj ## run a source file
irij test ## run tests/test-*.irj
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 listEmacs users: editors/emacs/irij-mode.el and irij-nrepl.el ship in the repo.
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.53975Algebraic 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 sumContracts (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
;; 355Structured 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 + 1Protocols
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: