Push Ifs Up and Fors Down: The Idiom, Its Algebra, and Its Limits

This explains and justifies the programming idiom "push ifs up and fors down": move branching decisions toward callers and concentrate iteration into tight, branch-free batch routines. Examples show turning a function that accepts Option into one that accepts a concrete Walrus by handling None at the call site, and replacing repeated calls with a single frobnicate_batch that loops internally for vectorized, cache-friendly execution. The same pattern appears in databases where projections and selections are executed early (pushed down into scans) while expensive joins are deferred until inputs are smaller, and where engines use batch/vectorized execution instead of per-row volcano-style next() calls.

The write-up frames these moves algebraically: pushing an if up corresponds to restricting to a subobject via an inclusion map (predicate-defined subset), and Option is a coproduct 1 + Walrus so branching factors into separate summands. The familiar rewrite law filter p . map f == map f . filter (p . f) is derived by factoring filter through Maybe (keep) and catMaybes and using naturality; it saves work only when p . f reduces to a cheap input predicate. Practical limits are emphasized: conditionals can move out only when loop-invariant, selections below joins only when they reference one side, and fors-down is a performance, not a semantic, transformation.