This is a follow-up to my previous post on Dhall-to-Effect and provably safe task orchestration. If you haven't read that one, the short version is: we use Banach space norm bounds, SMT solvers (Z3/Yices), and Dhall to ensure invalid build topologies are unrepresentable at compile time.
In the previous post, we used Dhall as a static configuration layer to define threshold values, which were then evaluated as SMT constraints before a single algebraic effect was allowed to fire.
But static graphs are only half the battle. Eventually, tasks have to actually run, fail, recover, and make decisions based on previous steps.
If our goal is to "never lie to the type system," how do we model conditional execution and fault isolation without falling back into the trap of weakly-typed runtime booleans and cascading failure states?
The answer, surprisingly, was to look at 1970s mainframe architecture, grab Apache Pekko and Spring Batch, and turn Dhall into an interactive stack machine assembler.
Here’s a look at the newly released batch-bridge module for Siunertaq.
🦕 Back to the Future: z/OS JES2 Meets Pekko
If you want to orchestrate batch jobs safely, the gold standard isn't a modern YAML-based cloud pipeline—it's IBM's z/OS JES2 (Job Entry Subsystem).
In JES2, a job is a sequence of steps. If a step fails (ABENDs), the entire job doesn't necessarily crash. Subsequent steps can inspect the return code of the failed step and decide whether to run a recovery operation, skip execution, or halt entirely. It provides strict, predictable fault isolation.
To bring this into the functional Scala world, I paired Spring Batch (for step context and lifecycle) with Apache Pekko (for actor-based fault isolation).
The JobSupervisorActor manages a tree of StepExecutorActor instances under Pekko's OneForOneStrategy. If a step throws a StepAbended exception, the supervisor catches it. Only that specific actor is stopped. Sibling steps continue unaffected, deciding their own fate based on the job context. We get mainframe-grade fault isolation using purely functional actor semantics.
🎛️ Execution Control as an Algebraic Data Type
Most modern orchestrators handle conditional execution like this: run_if_failed: true or some arbitrary bash script injected into a YAML file.
But arbitrary booleans are an anti-pattern when you want verifiable states. Instead, batch-bridge models JCL-style COND statements as an Algebraic Data Type (ADT):
// The Scala 3 ADT representing JCL condition codes
enum CondExpr derives CanEqual:
case Compare(threshold: Int, op: CondOp) // COND=(4,LT) -> skip if 4 < prevRC
case Even // COND=EVEN -> always execute
case Only // COND=ONLY -> execute ONLY if a previous step ABENDed
Because this is an ADT, invalid execution orders are structurally caught. The CondEvaluator intercepts the logic before the actor even starts. You cannot have a recovery step marked Only running if no previous step has explicitly registered an ABEND.
And crucially, this ADT is declared natively in Dhall.
🥞 The Stack Machine as an Input Device
Here is where the architecture gets really fun.
In the previous iteration, Dhall simply provided static threshold numbers. Now, Dhall acts as the input device supplying actual opcodes to a BSD Quiver stack machine (ProgramEval.exec).
Each Spring Batch step defines an input_prog—a list of StackInstr (Stack Instructions) defined in BatchJob.dhall.
-- Inside BatchJob.dhall
let Step : Type =
{ name : Text
, cond : CondExpr
, input_prog : List StackInstr
}
At execution time, the step doesn't run arbitrary shell scripts. Instead, the Spring Batch StackMachineTasklet takes the Dhall-provided instruction list, evaluates it using the core module's arithmetic IR, and stores the result directly in the Spring Batch JobExecutionContext. Downstream steps read these verified results to make CondExpr routing decisions.
We have entirely bypassed intermediate serialization formats (like writing to a temporary JSON file). The algebraic IR in the core module is directly driving the batch execution layer.
💻 The REPL as a Live Control Plane
Because Dhall is a total functional language (it is Turing-incomplete and provably terminates), it gives us a superpower: we can use its REPL as a live configuration interface.
Instead of restarting the JVM to tweak a batch job, you can drop into the Dhall REPL:
$ dhall repl
:load BatchJob.dhall
:let myEmergencyStep = { name = "recovery", cond = CondExpr.Only, input_prog = [ StackInstr.Push 0 ] }
When you evaluate this, dhall-to-json serializes the output, and circe decodes it into a fully typed BatchJobDef on the Scala side.
Because Dhall’s type checker enforces the schema (ensuring that cond matches the CondExpr ADT and input_prog is a valid sequence of StackInstr), the shape of the job is proven valid before the JVM executes a single instruction.
🔮 What’s Next: Tying it back to MLIR
With the batch-bridge in place, we now have:
- SMT-verified threshold bounds (Z3/Yices) defining what is allowed to run.
- A total-functional REPL (Dhall) defining the stack instructions and execution conditions.
- An Actor-backed Batch layer executing the graph with JES2-style fault isolation.
The next frontier is performance. Future work will introduce an mlir-bridge to map these BSDArrow decompositions and stack ops directly into the MLIR Affine Dialect, JIT-compiling the verified norm constraints via LLVM IR.
If you're interested in marrying old-school mainframe resilience with modern type-level functional programming, check out the new release.
The codebase is at github.com/Yoshyhyrro/Siunertaq. As always, PRs improving proof coverage or documentation are deeply appreciated. 🙏
Top comments (0)