A result type can be the same while effects differ. Handlers can remove one effect and add another.
By the end: interpret a conservative effect summary and distinguish it from a runtime trace.
Result and behavior answer different questions
Two functions can both return Int while one reads a file, another changes shared state, and a third may raise an exception. A result type alone need not record these behaviors. An effect system adds information about permitted or possible computation effects.
Our separate effect lab gives operations explicit summaries: literal has none, parse may throw, load performs io, and save performs io plus state. A sequence collects the union. The lab does not execute these operations, inspect real code, or infer the core language’s function effects.
Separate a returned value from an outward effect
A result type answers what kind of value a computation returns if it returns normally. It need not say what happens before that return. Consider two paper examples that both return the integer 7. One computes it using addition. Another reads a stored setting before returning it. Their result types can both be Int while their permissions differ. An effect is a category of behavior that the analysis records separately from the returned value. Here io means input or output, state means changing stored state, and throw means raising an exception.
The effect lab is separate from the authored expression trees used for inference. Its operation names are entries in a fixed dictionary, not source text that the core inference engine or interpreter understands. There is no free-text parser in that core either. In this lab, literal has the empty summary {}, parse has {throw}, load has {io}, and save has {io, state}. Braces describe a set, a collection in which membership matters but order and duplicates do not. The labels are declared assumptions about these names, not facts discovered by executing them.
Four declared operations supply different memberships
Operation
Declared set
What the set permits
literal
{}
None of the tracked effects
parse
{throw}
Possible exception
load
{io}
Input/output
save
{io, state}
Input/output and state change
These are stipulated summaries. No argument, returned value, or actual execution is needed to look up each set.
An empty set contains none of the tracked labels. It differs from a set containing a label whose operation happened zero times in a particular run. The first is an analysis result under the declared rules. The second is an observation of execution. For example, a parsing operation might accept its input and return normally. Its declared summary still contains throw because failure is permitted on other inputs. The summary does not report the probability of failure or require a failure every time. It represents a possibility that callers must account for.
To combine operation summaries, take their union. Union includes a label if either input set contains it. Start with literal and parse as a paper sequence. Literal contributes no members, and parse contributes throw, so the combined set is {throw}. Now append load. Its io joins the existing throw, yielding {io, throw}. Appending another load would leave exactly the same set because io was already present. This calculation deliberately forgets how many loads occur. A system intended to enforce an input/output budget would need more information than these memberships.
For the paper sequence load, parse, save, compute the summary in stages. The first operation contributes {io}. Combining parse gives {io, throw}. Save contributes io and state, but io is already present. Only state is new, so the final set is {io, state, throw}. Reversing these three names preserves the union because the membership question ignores order. That does not establish that the computations are interchangeable. Saving before parsing might change the world before discovering an invalid input. Equal summaries can describe operations with different ordering and failure behavior.
Repeated io does not add a second set member
Thick outlines mark newly added members. Save adds state; its io was already present after load. Geometry has no quantitative scale.
This loss of detail is useful when a caller needs a permission check rather than a history. Suppose a paper caller allows io and throw but forbids state. Load followed by parse fits those permissions, while parse followed by save does not. The decisive evidence is the state member, not the number of operations or their result type. Such an allowed-set policy is a reasoning example, not an extra control in this lab. It shows how a small summary can answer one precise question while leaving execution order and returned values unspecified.
Compose effects and inspect handlers
A pure exception handler removes throw from the protected computation’s outward summary in this model. A logging handler also contributes io. Handling an exception therefore does not automatically make a computation effect-free. The handler’s own behavior matters.
This deliberately conservative analyzer includes the logging handler’s io even when the protected operations have no throw effect. It does not prove the handler runs. It also does not model exceptions raised by the handler itself. These are explicit simplifications of effect composition, not the full Koka effect-row calculus.
Calculate a handler summary without inventing a trace
An exception handler catches a failure from a protected computation and supplies a response. The outward effect summary describes what can escape that protected region after the handler has acted. Here a pure catch removes throw and adds no tracked effect of its own. Calling this handler pure describes the rule assigned to it in this small analyzer. It does not mean that catching a failure reverses every earlier action. If load has already performed input/output before parse fails, handling the failure cannot make that earlier input/output absent from the computation's behavior.
Calculate load followed by parse under pure catch. Before handling, union produces {io, throw}. Removing throw leaves {io}. The result still permits input/output because the handler only addresses exceptions. For parse followed by save, the initial union is {io, state, throw}. Removing throw leaves {io, state}. The state member remains even though a particular failed parse might prevent save from running. The analyzer does not inspect those paths. It uses all declared operation summaries, so its output can contain behavior absent from one execution without contradicting that execution.
Handling and logging are separate set operations
Stage
Pure catch
Logging catch
Protected parse
{throw}
{throw}
Remove throw
{}
{}
Include handler contribution
{}
{io}
Each row shows an intermediate set for the same protected parse operation. The handler contributes effects after throw is removed.
The logging catch differs in one rule. After removing throw, it adds io for its own possible logging. With parse alone, the raw summary {throw} first becomes {}, then becomes {io}. With load followed by parse, {io, throw} first becomes {io}, and adding logging leaves {io}. These identical final sets have different explanations. In one case the handler introduces the only input/output permission. In the other, the protected computation already needs that permission. Set membership records neither the source of every action nor how often logging happens.
More generally, removing a member and then adding handler effects are different operations. If a handler could itself raise an exception, removing all throw information without accounting for that handler would be misleading. This lab's two handlers have no declared throw contribution, so the issue does not arise inside its rules. A different handler specification would require a different calculation. The same reasoning applies when a recovery action writes state or performs network access. Handling one effect does not justify deleting unrelated effects or forgetting effects contributed by the recovery code.
The strongest contrast is literal under logging catch. The protected summary is {}, so no throw is available for the handler to catch under these declarations. Nevertheless the lab reports {io}. It always includes logging's declared contribution, even when that contribution would be unreachable. This is a conservative rule, meaning that it keeps an extra possible effect rather than trying to prove the logging path impossible. It is less precise than a path-sensitive analysis, which would distinguish possible routes through code. The lab has no routes or handler execution to inspect.
Logging is included without a reachable throw
Both calculations start from literal. The logging result records the conservative handler rule, not evidence that logging happened.
Keep the region being summarized explicit. A paper program might handle parse locally and then call save outside that handler. Removing throw from the inner region says nothing about later unhandled operations. Conversely, a summary for an entire protected sequence includes effects from every declared operation before the handler adjustment. These region distinctions explain why real effect systems need rules for nested computations and function calls. The controls below expose only one call list and one whole-list handler. They do not let you move the handler between operations or construct nested protected regions.
Inspect the rules and their result
Compose declared effects and a handler
Operation in order
Declared effects
load
io
parse
throw
Before handler
{io, throw}
After handler
{io, throw}
Outward effects: io, throw.
Operation presets replace the call list and reset the handler to none. Handler controls retain the call list. The analyzer unions declared effects, removes handled throw, and includes logging io conservatively even if the handler is unreachable. It neither executes calls nor analyzes divergence. An empty result is not a totality certificate.
Protected effects
Handler
Outward summary
throw
Pure catch
Empty
throw
Logging catch
io
io, state, throw
Pure catch
io, state
Handlers change an effect summary under stated rules; they are not a runtime log.
Use the presets to isolate each composition rule
Begin with Load then parse and No handler in the existing lab. Read the operation rows before the summary panels. Load supplies io and parse supplies throw, so both panels should show {io, throw}. Choose Pure catch without changing the operation preset. The left panel stays fixed while the right loses throw. Choose Logging catch next. The right remains {io}, because io already belongs to the protected summary. This controlled comparison isolates handler choice. It does not compare two executions, and there is no hidden runtime input whose parsing success changes the result.
Now choose Parse then save. An operation preset replaces the whole list and resets the handler to No handler. That reset matters because otherwise a changed result could have two explanations. The raw set now has io, state, and throw. Reapply Pure catch and then Logging catch. Both leave {io, state}, but for different rule applications. Pure catch contributes nothing, whereas logging contributes io that was already present. The state member is unaffected in either calculation. A catch is not a transaction rollback, which would require rules for undoing or withholding changes.
The three existing call presets distinguish handler rules
Call preset
No handler
Pure catch
Logging catch
Literal only
{}
{}
{io}
Load then parse
{io, throw}
{io}
{io}
Parse then save
{io, state, throw}
{io, state}
{io, state}
Compare across a row while retaining calls. Choosing another operation preset resets the selected handler to No handler.
Choose Literal only and inspect the reset No handler state. Both sets are empty. Pure catch keeps them empty because there is no throw member to remove. Logging catch changes only the outward set to {io}. This is the preset that distinguishes conservative handler accounting from actual handler reachability. Returning to Load then parse resets the handler again. If you compare the two presets while forgetting that reset, you may attribute the disappearance of io to the wrong mechanism. The operation rows and selected handler together specify the entire input to this analyzer.
A paper comparison can expose another limitation without adding controls. Imagine parse followed by save on an invalid document and the same sequence on a valid document. The first may stop before saving; the second may save. The analyzer gives both the same declared union because it receives neither document nor parse outcome. Even swapping the order to save followed by parse would keep the same raw set. Those hypothetical histories explain information omitted by the summary. They are not output traces produced by this widget, which never executes parse or save at all.
Set inclusion gives a precise way to compare summaries. A is a subset of B when every member of A also belongs to B. For example, {io} is a subset of {io, state}, but {throw} is not. If a paper caller allows only io, an outward {io} satisfies its permission boundary, while {io, state} exceeds it. Adding state makes the required permission set larger even when the returned value stays unchanged. The relation compares permissions, not execution counts or program quality. The current lab shows sets but does not implement this caller-policy check.
An io-only paper policy accepts some outward summaries
Protected calls and handler
Outward set
Subset of allowed {io}?
Literal, no handler
{}
Yes, no members exceed permission
Load then parse, pure catch
{io}
Yes
Parse then save, pure catch
{io, state}
No, state is not allowed
Load then parse, no handler
{io, throw}
No, throw is not allowed
This policy comparison is a paper example, not a lab control. State fails because it lies outside the allowed set.
You can also reason about a change that leaves the summary unchanged. Replacing pure catch with logging catch on Parse then save changes the handler rule but not its final members. That equality does not prove the handler implementations equivalent. One may write a log where the other does not, and their recovery results could differ in a richer language. The summary intentionally merges many behaviors into the same description. To explain an unchanged display, inspect each intermediate removal and addition rather than concluding that the changed control has no meaning or no possible runtime consequence.
Absence claims need a trusted specification
An effect summary says what may occur under the supplied rules, not what did occur on one run. A conditional can have a possible io effect even when one branch does no io. Safe over-approximation can reject some uses without showing an actual side effect happened.
Some systems track nontermination as an effect; others use purity only to exclude certain observable effects. Koka’s total effect has its own stronger meaning. Our empty set does not certify totality, security, performance, or business correctness. The separate functional-programming/effect-systems course remains a larger topic.
Interpret absence relative to the effects actually tracked
A conservative summary aims to include every behavior allowed by its rules, while sometimes including behavior that will not occur. This is an over-approximation, a description containing at least the relevant possibilities rather than exactly the observed ones. Logging catch on literal illustrates an extra member. Omitting save's state member would be the opposite mistake, an under-approximation that hides a declared possibility. Over-approximation can be inconvenient for callers with narrow permissions, but under-approximation defeats the permission check. Whether an implementation achieves the intended coverage still depends on its rules and their faithful implementation.
An absence conclusion depends on the vocabulary being analyzed. If a summary lacks state, this lab says no declared state effect remains. It has no label for network destinations, file names, personal data, or monetary transfers. Consequently, io alone cannot distinguish a permitted local read from a forbidden disclosure. A security policy would need finer permissions and trustworthy operation declarations. It might also need relationships between inputs and outputs. Reusing the word effect does not supply those missing distinctions, and a small set should not be interpreted as a complete security classification.
Different hypothetical histories can share one declared summary
Paper case: parse then save
Possible history
Declared raw set
Invalid document
Parse fails before save
{io, state, throw}
Valid document
Parse returns; save follows
{io, state, throw}
The histories are paper possibilities, not simulator output. The analyzer receives operation names, not parse outcomes or runtime documents.
Termination means that a computation eventually finishes rather than continuing indefinitely. The core inference interpreter has resource limits, and this effect lab does not analyze termination at all. Its empty set means only that io, throw, and state are absent after the declared rules. Koka's documented effect vocabulary separately represents possible divergence, meaning nontermination, and gives its total effect a stronger interpretation. You cannot transfer that interpretation to {} here. The two analyses have different languages and tracked properties, even though both discuss effects and may print an apparently empty or pure description.
Likewise, an effect-free result does not state the intended answer. A paper function returning 2 instead of the required 1 might perform no input/output, change no state, and raise no exception. Its effect description would miss the arithmetic mistake because that mistake concerns the result specification. A result type such as Int also misses it because both numbers are integers. To express the requirement, state the relation between input and output or test it against suitable examples. Result classification and behavior classification can both be useful while leaving this separate obligation unresolved.
Effects also differ from equality constraints in the earlier engine. Unification makes two type trees agree by replacing unknown variables consistently. This lab instead takes unions of known label sets and removes one label for a handler. It creates no unknown effect variables and solves no equations between effect rows. An effect row is an extensible description that can include an unspecified remainder of effects. That machinery belongs to richer systems, not these controls. Treating the current io member as a type unknown would confuse a fixed permission category with an unresolved inference question.
An empty literal summary answers only tracked questions
Question for literal with no handler
Evidence from this analyzer
Contains io, throw, or state?
No, its stipulated set is empty
Terminates?
Not analyzed
Returns the intended business answer?
Not analyzed
Keeps private data secret?
No information-flow analysis
Absence applies to the three declared labels. Questions outside that vocabulary require evidence the effect lab does not produce.
The transferable calculation is to name the protected operations, combine their declared possibilities, account for the handler's own behavior, and interpret the final set within that vocabulary. This works for reviewing a proposed effect interface even when no operation executes. If a caller asks for a stronger guarantee, identify the missing distinction rather than guessing from an empty display. For this lab, the defensible result is a finite set computed from the selected names and handler. It is neither a history of side effects nor a proof of totality, secrecy, or the intended business result.
Exercises
Catch and log
A computation has effects io and throw. A logging catch handles throw and performs io. What remains?
Hint
Remove handled throw, then include the handler’s own effect.
Worked answer
Stage
Effect set
Protected computation
{io, throw}
After handling throw
{io}
Add logging effect
{io}
Set membership is not an execution count.
io remains. It was already possible in the protected computation and is also contributed by the handler. The set contains io once; it does not count how many operations occur. Catching the exception does not undo prior input/output.
An empty summary
The lab reports an empty effect set. Does that establish that a real function terminates and computes the desired answer?
Hint
Ask which properties this lab actually tracks.
Worked answer
Property
Tracked here?
io, throw, state labels
Yes
Termination
No
Correct business result
No
An absence guarantee cannot exceed the analysis vocabulary.
No. The lab tracks only stipulated io, throw, and state labels. It does not analyze recursion or prove the result specification. A different language may track divergence explicitly and give an empty effect a stronger meaning. Read that language’s definition rather than transferring this label across systems.
Sources and further reading
Selected reference passages support the definitions and algorithms below. The examples, explanations, and implementations are original. Terminology and assumptions are stated within each lesson; source review is not an independent audit of this course. Optional links are not runtime dependencies.
Selected effect-type, exception, divergence, and totality examples. Our finite effect-set union is not Koka row inference or an empirical performance claim.