Guide
Effects
Inferred from the calls a function makes, and checked against what it claims.
What a function can be doing is tracked, and it is inferred from the calls it makes rather than declared by hand. An annotation is a claim the compiler checks, not information it needs.
Inferred from the calls
A call into a capability is where an effect enters a program, and the registry declares the effects of every host-visible operation. That is what makes inference possible at all, and why a pure function is pure because of what it does not call rather than because it said so.
// `@deterministic` is a claim the compiler checks, not a note to the reader.
//
// A simulation is given its delta as a parameter rather than reaching out for one. That is what
// makes it a function of its inputs, which is the property a replay depends on.
@deterministic
fn step(position: f32, velocity: f32, dt: f32) -> f32 {
return position + velocity * dt
}
@pure
fn squared(x: f32) -> f32 {
return x * x
}
pure and deterministic are assertions
@pure says this function observes nothing. @deterministic says it is a function of its inputs. Both are checked against the calls inside them, and a violation names the call rather than the annotation.
Tracked whether or not a subsystem exists
An effect is a property of the code; availability is a property of the target. They are separate on purpose, so a file can be checked for what it does before anything decides whether it may.