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 and raw interop are explicit soundness boundaries: the compiler surfaces diagnostics or assumptions rather than proving their behavior. Calling a callback is no longer one of them — since 0.15 the compiler reads the callback's declared §E{…} and charges it to the caller, and reports Calor0425 when one side carries no §E{…} and it cannot tell.

--permissive-effects waives the "cannot tell" boundary — Calor0411 and Calor0425 go unreported and Calor0410 becomes a warning — which voids the effect guarantee, since unknown calls are then counted as doing nothing. It never waives Calor0424, Calor0420, or Calor0421. See Effects.

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:

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

Violations produce compile errors with full call chains:

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:

§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:

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

To fix, either:

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

What It Catches

Hidden Network Calls

§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

§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

§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:

// 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:

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:

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

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

Strict Mode (Errors)

Promote unknown effects to errors:

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

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

Comparison with Implicit 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

§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:

// 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:

// §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

Next

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