Ordinary types describe the values an expression produces. An effect system additionally describes relevant interactions an expression may perform while producing them.

A typing judgment can be enriched from

$$\Gamma\vdash e:T$$

to something like

$$\Gamma\vdash e:T;!;\varepsilon,$$

where $\varepsilon$ summarizes effects such as state mutation, exceptions, I/O, allocation or asynchronous operations.

For example, a pure addition might have

$$\Gamma\vdash x+1:\text{Int};!;\varnothing,$$

while a function that writes to a file could have an IO effect.

Effects compose. If one subexpression may throw and another may perform I/O, the enclosing expression must account for both unless some construct handles or eliminates an effect.

This information can enforce architectural guarantees. A function declared pure can be prevented from calling effectful operations; an exception effect can indicate which computations require handling; region or state effects can limit which storage a function may mutate.

Effect systems move part of the behavioral contract from documentation into static reasoning. They do not prescribe one particular syntax: the general idea is to track computational behavior in addition to value shape, enabling finer guarantees than value types alone.