Clojurians Log v2
datahike
🧪 wandler — a query planner for your in-app data pipelines. On Clojars now (experimental).
Your database has a query planner: it picks join orders, pushes down filters, chooses indexes — so you never hand-tune a query. Your in-memory map/`filter`/`reduce`/`group-by`/`join` pipelines get none of that. wandler is that planner for your pipeline code. Plug one in and it fuses the passes, drops intermediate collections, factorizes a group-by-over-join so the join is never built (O(N²)→O(N)), or runs it incrementally — and it re-plans automatically as you edit, so you never sit and reason about the optimal execution for each hot loop.
Types are just malli — the m/=> schema you may already write; change defn → a/defn and the pipeline is checked, optimized, and compiled:
clojure
(m/=> big-squares [:=> [:cat [:sequential :int]] :int])
(a/defn big-squares [xs]
(reduce + 0 (map (fn [x] (* x x)) (filter (fn [x] (< 10 x)) xs))))
(:stages-after (w/explain 'big-squares)) ;=> [foldl] ; 3 passes → 1
(:verified? (w/explain 'big-squares)) ;=> true ; proved equal to your original🧵 Under the hood. The optimizer is an e-graph (equality-saturation, egg-style) rewriter: it builds out the space of forms your pipeline is provably equal to under the rule set, then extracts the cheapest — each adopted rewrite carrying its kernel proof. Same idea as a modern query optimizer, except the rewrites are certified and the IR is your pipeline.
It also plans jointly with datahike and stratum: embed a d/q or stratum query right in a pipeline and the planner optimizes across the boundary — pushing the aggregation through the join, factorizing, choosing the drive direction — so the same planning + optimized execution those engines bring to your queries reaches the code around them too.
Extending it to your domain: the rewrite rules are just kernel-checked laws. Have a coding assistant add the laws for your operators (a custom fold, a domain join, a bespoke aggregation); once they're in, every pipeline that uses them gets planned automatically — even as you keep editing.
🧵 ansatz 0.2 — "Verified Clojure via Lean 4" — the kernel + DSL underneath (and what the assistant uses to check the rules it writes), now much easier to pick up. If you already write malli-instrumented Clojure, it's the gradual next step — keep your schema, change defn → a/defn:
clojure
(require '[ansatz.core :as a] '[malli.core :as m])
(a/load-init!) ; bundled Lean Init, zero setup (straight from the jar)
(m/=> dbl [:=> [:cat :int] :int]) ; just a malli schema
(a/defn dbl [x] (+ x x)) ; defn → a/defn — now machine-checked, still plain Clojure
(dbl 21) ; => 42(a/load-init!) loads a bundled Lean Init environment from the jar, no store to build; full Init / Mathlib fetched on demand.
• malli support — m/=> schemas become kernel signatures; [:map …] → named-field records (keyword access verifies, runtime stays plain maps); [:int {:min 1}] → refinements you still use as plain numbers.
• Better tactics — faithful funext, simp only / simp_all only, a split cluster, omega improvements, ac_rfl.
• Bugfixes — omega hypothesis handling, codegen, several simp universe fixes.
Repos: https://github.com/replikativ/ansatz · https://github.com/replikativ/wandler