The effect model: which calls are observable effects, and which are known to be free of them.
A purity claim is a claim about every execution, so the analysis cannot simply assume that a call it knows nothing about is harmless. Every real purity checker ships an effect model of its standard library — Haskell encodes it in types, effect-typed languages in rows; on the BEAM it has to be a table, because the runtime offers no way to ask.
So calls land in one of three buckets:
- impure — a known observable effect. Names the category, so the report can say what the effect is rather than just that there is one.
- pure — known to compute a value and nothing else.
- unknown — neither. The analysis reports these as unprovable rather than guessing, which is the difference between a verification and an opinion.
That third bucket is the honest part. Assuming unknown calls are pure would make the checker report success far more often and mean nothing; assuming they are impure would flag every real program. Saying "I cannot see past this" is the only answer that keeps a "verified" worth having.
Two dimensions, not one
Every impure call also carries a mode: :read or :write.
Purity cares about neither — reading a clock or the process dictionary
already breaks referential transparency, so both modes are equally
disqualifying. Other contracts care a great deal. Inside a database
transaction, Application.get_env/2 is harmless and HTTPoison.post/2
is an incident: one has nothing to undo, the other has already left the
machine. A model with only "is this an effect" cannot tell them apart and
would report every config read as a transaction hazard.
Mode defaults to :write, so a call nobody has classified is assumed to
change something. That is the safe direction: a false "this is
irreversible" costs a look, a false "this is harmless" costs the bug.
Scope
Effects here are observable: something outside the function can tell they happened. Allocation, arithmetic, matching and exceptions are not effects — a function that raises still computes a value or fails and leaves nothing behind.
Summary
Types
Whether an effect changes anything a rollback or a retry would care about.
Functions
Every impure category, for exhaustiveness checks and reporting.
Classify a remote call.
Whether a call changes anything, or merely observes it.
Modules whose calls dispatch to an open set of implementations.
Modules treated as free of observable effects.
Types
@type category() ::
:io
| :process
| :process_dict
| :ets
| :port
| :node
| :time
| :random
| :network
| :code_loading
| :logging
@type mode() :: :read | :write
Whether an effect changes anything a rollback or a retry would care about.
Defaults to :write for anything unlisted, because assuming an unknown
effect is harmless is the expensive mistake.
Functions
@spec categories() :: [category()]
Every impure category, for exhaustiveness checks and reporting.
Classify a remote call.
iex> Argus.Purity.Effects.classify("IO", "puts")
{:impure, :io, :write}
iex> Argus.Purity.Effects.classify("Application", "get_env")
{:impure, :process, :read}
iex> Argus.Purity.Effects.classify(":erlang", "+")
:pure
iex> Argus.Purity.Effects.classify(":erlang", "put")
{:impure, :process_dict, :write}
iex> Argus.Purity.Effects.classify("String.Chars", "to_string")
{:opaque, :protocol}
iex> Argus.Purity.Effects.classify("MyApp.Repo", "all")
:unknownWhether a call changes anything, or merely observes it.
iex> Argus.Purity.Effects.mode("File", "read")
:read
iex> Argus.Purity.Effects.mode("File", "write")
:write@spec protocol_modules() :: [String.t()]
Modules whose calls dispatch to an open set of implementations.
@spec pure_modules() :: [String.t()]
Modules treated as free of observable effects.