Effect Soundness

Feature: Compiler-enforced effect declarations Related metric: Effect Discipline (measures side effect management quality) C# equivalent: None (no effect system)

Overview

Calor's compiler checks declared effects against direct recognized operations and the resolved Calor call graph. A function marked §E{} cannot contain a known I/O operation or call a resolved effectful function without a matching declaration.

Unknown external calls, unresolved delegates, and raw interop are explicit soundness boundaries: the compiler surfaces diagnostics or assumptions rather than proving their behavior. --permissive-effects waives those boundaries and voids the effect guarantee.

Why It Matters

Hidden side effects cause real bugs:

Testing failures - "Pure" functions that secretly log make tests non-deterministic
Concurrency bugs - Functions assumed safe for parallel execution have hidden state
Performance surprises - What looks like a calculation actually hits the network
Security issues - Code assumed side-effect-free modifies databases

Effect soundness means:

You can rely on declarations for the resolved graph when there are no unresolved-call, interop-assumption, or waiver diagnostics
Refactoring across that checked surface exposes newly introduced known effects
Testing strategy follows directly from effects

It does not by itself prove thread safety, determinism, or freedom from effects hidden behind an unresolved boundary.

How It's Measured

The compiler traces effect violations through the resolved call graph:

Direct effects - Does the function body contain effectful operations?
Transitive effects - Do called functions have effects?
Declaration match - Are all effects properly declared in §E{...}?

Violations produce compile errors with full call chains:

Plain Text

error Calor0410: Function 'ProcessOrder' uses effect 'network'
                 but does not declare it
  Call chain: ProcessOrder → NotifyCustomer → SendEmail → HttpClient.PostAsync

Example

A function declared with only database effects:

Plain Text

§F{f001:ProcessOrder:pub}
  §I{Order:order}
  §O{bool}
  §E{db:rw}                    // Declares: only database effects

  §C{SaveOrder} order          // OK: SaveOrder has db effect
  §C{SendConfirmation} order   // ERROR: has network effect!
  §R true

The compiler catches this:

Plain Text

error Calor0410: Function 'ProcessOrder' uses effect 'net:w'
                 but does not declare it
  Call chain: ProcessOrder → SendConfirmation → EmailService.Send → HttpClient.PostAsync

To fix, either:

Add the effect: §E{db:rw,net:w}
Remove the effectful call
Use a different implementation without network effects

What It Catches

Hidden Network Calls

Plain Text

§F{f001:Calculate:pub}
  §O{i32}
  §E{}                         // Claims to be pure

  §B{rate:i32} §C{FetchExchangeRate} §/C  // ERROR: network!
  §R (* 100 rate)

Undeclared Database Writes

Plain Text

§F{f001:GetUser:pub}
  §I{i32:id}
  §O{User}
  §E{db:r}                     // Claims read-only

  §B{user:User} §C{Repository.GetById} id §/C
  §C{AuditLog.Write} id        // ERROR: this is db:w!
  §R user

Logging in "Pure" Functions

Plain Text

§F{f001:ValidateEmail:pub}
  §I{str:email}
  §O{bool}
  §E{}                         // Claims no effects

  §C{Logger.Debug} email       // ERROR: console write!
  §R §C{IsValidFormat} email §/C

Effect Propagation

Callers must include all effects of their callees:

Plain Text

// Callee has console write effect
§F{f002:LogMessage:pri}
  §I{str:msg}
  §O{void}
  §E{cw}
  §P msg

// Caller MUST include cw effect
§F{f001:ProcessAndLog:pub}
  §I{Data:data}
  §O{void}
  §E{db:rw,cw}                 // Must include cw because we call LogMessage

  §C{SaveData} data
  §C{f002:LogMessage} "Saved"

If ProcessAndLog declared only §E{db:rw}, the compiler would error:

Plain Text

error Calor0410: Function 'ProcessAndLog' uses effect 'cw'
                 but does not declare it
  Call chain: ProcessAndLog → LogMessage → Console.WriteLine

Effect Checking Modes

Default Mode (Warnings)

Unknown external calls produce warnings:

Bash

calor -i app.calr -o app.g.cs

Plain Text

warning Calor0411: Unknown effects for call to 'ThirdParty.DoSomething'

Strict Mode (Errors)

Promote unknown effects to errors:

Bash

calor -i app.calr -o app.g.cs --strict-effects

Plain Text

error Calor0411: Unknown effects for call to 'ThirdParty.DoSomething'
  Add effect declaration to manifest or declare pessimistic effects

Comparison with Implicit Effects

Aspect	C# (Implicit)	Calor (Explicit)
Side effects visible?	No - must read implementation	Yes - in function signature
Compiler enforcement	None	Resolved-call graph analysis with explicit unknowns
"Pure" guarantee	Convention only	Enforced when calls resolve; assumptions are surfaced
Refactoring safety	Must manually verify	Known-effect violations are caught within the checked surface
Testing strategy	Guesswork	Follows from effects

C# Example

// C#: What effects does this have?
public async Task<User> GetUser(int id)
{
    var user = await _repository.GetById(id);  // Database? Memory?
    _logger.Log($"Retrieved user {id}");        // Console? File? Network?
    await _cache.Set(user);                      // Memory? Redis?
    return user;
}
// Answer: You have NO IDEA without reading every dependency

Calor Equivalent

Plain Text

§F{f001:GetUser:pub}
  §I{i32:id}
  §O{User}
  §E{db:r,cw,net:rw}           // EXPLICIT: database read, console, network

  §B{user:User} §C{GetById} id §/C
  §C{Log} (concat "Retrieved user " (str id))
  §C{CacheSet} user
  §R user

Benefits for AI Agents

1. Filtering by Effect

Find all functions that access the database:

Plain Text

// Agent searches for §E{..db..}

2. Refactoring Safety

Use §E{} as a checked pure surface only when compilation has no unresolved or waived effect assumptions:

Plain Text

// §E{} does not alone prove that a function is safe to parallelize

3. Test Planning

§E{} - Unit test directly
§E{cw} - Mock console
§E{db:rw} - Mock database
§E{net:rw} - Mock HTTP

Effect Discipline - Side effect management benchmark
Correctness - Edge case handling benchmark