Capability-safe · Polysemy · Micro-OS
The Haskell Effect Kernel
Vortex turns a Haskell effect type into a safe, remote shell. You define which operations exist; users stream monadic code that type-checks against only your DSL.
Vortex turns a Haskell effect type into a safe, remote shell. You define which operations exist; users stream monadic code that type-checks against only your DSL.
A wisp — a heavily restricted user — connects over a websocket or ssh and streams monadic code blocks in. Each block is type-checked against a DSL with nothing else in scope, run through per-user interpreters, and answered with show-rendered Haskell. The boundary between what a user asks for and what they may do is drawn by the type checker, not a runtime sandbox — reach past the DSL and the block doesn't fail when it runs, it fails to compile.
A block runs only if it type-checks against the effect row. The forbidden operation isn't caught at runtime — it's unnameable.
A DSL's exported names are exactly the operations a user may call. Widen the surface by editing one list.
Identity comes from SSH CA principals, not Linux uids. The same script means different things to different callers.
Compile and run budgets, with output force-bounded, so neither non-termination nor a lazy infinity can escape.
Define effects as a polysemy row, re-export only what a user may name, and pair
it with interpreters. The export list is the sandbox: nothing in scope lifts
IO into the row, so a script can compose your operations freely but can reach
nothing you didn't grant.
Effect signatures and the script type — a coproduct of your operations as a free monad.
A module re-exporting just the smart constructors. This list is the capability set.
Interpreters, chosen per user, folding the free monad into IO — or a pure value.
-- the theory: a pure effect row, no IO in sight data Dice m a where Roll :: Int -> Dice m Int makeSem ''Dice type Spell = Sem '[Say, Dice, Who] -- the syscall table: the export list IS the sandbox module Spellbook (say, roll, whoami) where -- the model: interpreters, per wisp runSpell wisp emit = runM . runWho wisp . runDice . runSay emit
The spellbook example. whoami answers from the subject, so the
same syntax speaks differently to different wisps.
Type freely over a socket or pipe a script in. Blocks stream in, values come
back as real Haskell — not JSON — read back with readMaybe at the type you asked
for. Bindings persist for the session; let binds a recipe, <-
captures a value.
Agents get first-class discovery: :commands reflects the whole typed
API from the DSL's export list — so the list can never drift from what a user can actually
call — and :type checks a call without running it, so an agent can validate before
it commits.
Failures go to stderr; results print bare — piped output is clean data.
The security boundary is the type checker, not a runtime sandbox. Each guarantee is a property the design gives you, not a check that can have holes.
A block that runs is well-typed against the DSL. GHC gives this for free.
The only maps from a user's syntax into IO are the folds the host chose. Initiality, as a theorem.
Every block produces a result or is killed at the deadline. The shell never hangs.
Swap the GHC oracle for a total elaborator and a DSL becomes total by construction — Dhall's guarantee, as a choice of one package.
A shell DSL folds into IO — effects reach the world. A config DSL folds into a pure value — the same machinery becomes a config language. “Which format the config is in” is a choice of front-end the back-end never sees. Vortex can replace bashrc files just as it can replace dhall files.
Say, Dice and Who interpreted into IO — a live shell where blocks actually do things: roll a die, speak a line, ask who's asking.
A package set as a vortex script instead of a dhall file — folded purely into a value, driving nix generation. Capability-free by type, exactly Dhall's guarantee.