108 Procedures and Effects

Predica separates expressions from procedures. An expression denotes a value extension and may be used in queries, constraints, derived attributes, folds, and function bodies. A procedure is a no-result callable whose body is permitted to perform effects: it may update locations, print output, call other procedures, or perform database-state updates inside an open transaction.

Permission to perform effects is not a requirement to perform them. A procedure remains a procedure when its body happens to have no observable effect, because it has no result and its call is a statement.

proc recordShipment(ShipmentsSystem system, Supplier supplier, Part part, Integer qty)
{
    var Shipment shipment = Shipment {
        supplier = supplier,
        part = part,
        qty = qty
    };

    system.shipment ∪= shipment;
}

A procedure declaration uses the proc keyword followed by a name, parameters, and a statement block. It has no result type and cannot be used as an expression. Plain procedure parameters are read-only and non-owning. A parameter prefixed with & receives exclusive access to a caller variable, while one prefixed with ^ is owned by the procedure. Parameters are single-valued, like function parameters. Each argument must be assignable to the parameter type and must have static cardinality one after any cardinality-flow refinements. A procedure call is a statement:

recordShipment(system, supplier, part, 12);

The caller writes & when granting exclusive access and writes ^ when explicitly transferring ownership. An owned parameter may also be initialised from an ordinary expression, copying where necessary. See Parameter Access and Ownership.

Function calls and procedure calls deliberately live in different contexts. Calling a pure function for its result is an expression. Calling a procedure is a statement. A procedure call is not valid inside a query expression, a constraint, a derived attribute, a fold body, an expression-bodied function, or a pure block-bodied function.

Procedure names may be qualified through component aliases and namespaces, such as admin.recordShipment(system, supplier, part, 12);. Procedures do not have receiver-call syntax. The expression-style spelling supplier.recordShipment(system, part, 12); is not a procedure call merely because supplier is one of the arguments; write recordShipment(system, supplier, part, 12); instead.

Functions stay pure

Every func declaration denotes a pure function. An expression-bodied function is pure by construction. A block-bodied function is valid only when its statement body is statically pure: it may use local variables, local updates, loops, branches, read-only query expressions, and pure function calls, but it must not print, call a procedure, read or write program-global state, write database-state locations, or depend on an open transaction.

Side-effecting reusable operations are procedures, not impure functions. This keeps ordinary expression evaluation free of hidden updates and makes it clear when program execution crosses from query calculation into state change.

Procedure effects

A procedure body is checked as a procedure context. It may call pure functions and other procedures. It may update program-state locations. It may print. It may update database-state locations only when the call is executed with an open transaction for the relevant data partition.

The effect of a procedure is determined from its body and the procedures it calls. A procedure that may write database-state locations has a database-write effect. Calling such a procedure has the same transaction requirement as writing the database-state locations directly. The call must not silently filter away out-of-partition updates; partition validity is checked by the update rules.

Procedures may use a bare return; statement to leave the procedure early. A procedure cannot return a value. If a program needs a value, compute it with a function and pass it to a procedure, or assign it to a program variable before the procedure performs its updates.