# Effects and the host

> Time, timers, files, sounds and the network, without a line of IO in the app.

A Cairn app never performs an effect. It returns effects as **data**, and the host performs them.
What the host learns comes back as messages, decoded by a proved decoder. That keeps every
function in the app pure, so everything in the previous chapters still applies.

This chapter follows the fixture's Flash button, which sets a timer and hears it fire, and the
framework's own types for the rest.

## Two ways in

A person's actions arrive through `update`, as before: every one names a control on screen.
Everything else, the clock, timers, replies to requests and outside inputs, arrives through a
second function, `receive`, as a **message**.

```lean
/-- Runtime → app, through `App.receive`: the outside world. -/
inductive Msg where
  /-- The current time, delivered before anything else whenever it changed. -/
  | clock (t : Time)
  /-- A timer the app set has come due. -/
  | timer (name : String)
  /-- The answer to request `id`. -/
  | reply (id : Nat) (r : Reply)
  /-- An event from an active subscription. -/
  | sub (s : Sub) (e : SubEvent)
deriving Repr, BEq, Inhabited
```

`lean/Cairn/Effects.lean`, lines 266–276

Both return the new state and a list of effects:

```lean
/-- App → host (and runtime). -/
inductive Effect where
  | setClipboard (s : String)
  | beep
  /-- Move keyboard focus to the control `c`. The runtime runs this one, not the host: after the
  step's actions it sets `ui.focus := some c`, and keeps it only if `c` is a focusable control
  of the new tree (docs/runtime.md). No `blur` is delivered for a field it takes focus from.
  The host decodes it and does nothing. -/
  | focus (c : ControlRef)
  /-- Start (or restart) the timer `name`, due `ms` milliseconds from now. The runtime keeps
  timers; the host only wakes it (docs/effects.md). -/
  | setTimer (name : String) (ms : Nat)
  /-- Forget the timer `name`; nothing if it isn't set. -/
  | cancelTimer (name : String)
  /-- Ask the host to do `r`; it answers with `Msg.reply id _`, exactly once. At most
  `App.maxInFlight` requests of capped kinds (`Request.Kind.capped`) are with the host at a time;
  the runtime holds the rest and sends them, oldest first, as slots free. -/
  | request (id : Nat) (r : Request)
  /-- Withdraw request `id` (docs/effects.md, "Requests in flight"). Its reply never reaches the
  app. A request still waiting for a slot is dropped and never sent; one already sent is cancelled
  on the host (`URLSessionTask.cancel`), and its id stays taken until the host's one reply to it
  arrives, which the runtime swallows. Nothing if `id` is not pending. -/
  | cancelRequest (id : Nat)
  /-- End the app. The host terminates after running the frame's other effects. -/
  | quit
  /-- Move the scroll box or virtual list `box` (its `Style.scrollRef`) to `to`, clamped as every
  offset is. The runtime runs this one, like `focus`: after the step's deliveries and layout it
  sets the offset against the tree just laid and lays out again (docs/runtime.md, "Scrolling").
  A box not on screen is left alone. The host decodes it and does nothing. -/
  | scrollTo (box : ControlRef) (to : ScrollTarget)
  /-- Set the Dock tile's badge to `label`; `none` clears it (docs/effects.md, "The Dock badge
  and announcements"). The host shows exactly the label; Lean decides what it says. -/
  | badge (label : Option String)
  /-- Ask assistive apps (VoiceOver) to speak `text`, for news that has no focus of its own
  ("Couldn't like the post; it's back as it was"). Posted once, with exactly this text. -/
  | announce (text : String) (priority : Priority)
deriving Repr, BEq, Inhabited
```

`lean/Cairn/Input.lean`, lines 164–200

Keeping the two apart is what lets every claim theorem keep saying "every action names a control":
messages from the world name none.

## Time

The host stamps every batch of events with the time, and the app hears it first, before any action
or message in that batch. So an app that stores the time always has the current time when any of
its functions run, including when a button is pressed. A stopwatch keeps it in its state, from the
`clock` message, to show the time since Start.

The monotonic clock never goes backwards in the runtime, whatever the host sends; that is a
theorem, not a promise.

## Timers

An app sets a named timer with `setTimer name ms` and cancels it with `cancelTimer name`. The
timers are kept by the runtime, in Lean, and the host's only job is to wake it at the earliest
deadline. So "a cancelled timer never fires" is proved, with no race between a host timer that
already fired and a cancel on its way. The fixture's timer is named, with how long the note shows:

```lean
/-- The timer Flash sets, and how long the note shows. -/
def flashTimer : String := "flash"
def flashMs : Nat := 400
```

`test/fixture/lean/Fixture.lean`, lines 147–149

Flash sets it. A move that asks for effects uses `emit` instead of `apply`: the new state, and the
effects:

```lean
move ^6 flashMove (s : State) "Flash" in ^1 where
  does "Press Flash."
  sees "A note shows, and goes when the timer the press set fires."
  on press
    emit := ({ s with flash := true }, [.setTimer flashTimer flashMs])
    post s' := s'.flash = true ∧ s'.items = s.items
    sound := by intro s; exact ⟨rfl, rfl⟩
```

`test/fixture/lean/Fixture.lean`, lines 277–283

When the timer comes due, `receive` hears it by name and takes the note down:

```lean
/-- Whether a message is Flash's timer. -/
def isFlash : Msg → Bool
  | .timer n => n == flashTimer
  | _ => false

/-- The world's messages: Flash's timer clears the note; replies and timers of the likes go to
`Like.receive`. -/
def receive (s : State) (m : Msg) : State × List Effect :=
  let o := Like.receive false s.likes s.nextReq m
  ({ s with flash := if isFlash m then false else s.flash, likes := o.1, nextReq := o.2.1 }, o.2.2)
```

`test/fixture/lean/Fixture.lean`, lines 503–512

## Requests

A request asks the host to do something that answers back: read or write a file, play a sound,
make an HTTP request, and more. The app picks the request's id, and the reply comes back to
`receive` under that id, exactly once. Failure is an ordinary reply: a missing file is
`failed notFound`, never an exception. The request kinds, today:

```lean
/-- Something the host does that answers back. Closed: adding a kind is a constructor, its
encoding, a `Reply.answers` case and one host handler (docs/effects.md). -/
inductive Request where
  | readFile (path : String)
  /-- Replace the file atomically, creating missing parent directories. -/
  | writeFile (path : String) (data : ByteArray)
  /-- A named system sound ("Tink", "Pop", "Basso", …). -/
  | playSound (name : String)
  /-- An HTTP request. With a `secret`, the host adds its header as it sends (a missing secret
  answers `failed notFound` and sends nothing). With a non-empty `capture`, a 2xx reply whose
  body is a JSON object has each listed top-level string field (`(field, account)`) written to
  the Keychain item `account` and its value replaced by `""` in the body Lean receives; all or
  nothing: a body that isn't a JSON object, or a listed field that is missing, repeated or not
  a string, answers `failed invalid` and writes nothing. Other replies pass through as they
  came. With `redact`, the request carries a secret the person typed (a secure field's text,
  `Cairn.Text.SecureField`): every dump, log and report prints its URL, headers and body as
  `<redacted N bytes>`, and the host sends it as given. -/
  | http (method url : String) (headers : List (String × String)) (body : ByteArray)
      (timeoutMs : Nat) (secret : Option Secret := none)
      (capture : List (String × String) := []) (redact : Bool := false)
  /-- Append to the file, creating it (mode 600) and missing parent directories. -/
  | appendFile (path : String) (data : ByteArray)
  /-- The names in a directory (not `.` and `..`), sorted by their UTF-8 bytes. -/
  | listDir (path : String)
  /-- Remove a file or a symbolic link; never a directory. -/
  | deleteFile (path : String)
  /-- The app in front: its process id and name. -/
  | frontmostApp
  /-- Whether the app holds `p`; with `prompt`, the system also asks the person if it doesn't. -/
  | permission (p : Permission) (prompt : Bool)
  /-- Bring process `pid` to the front and type `text` into it as key events, then Return if
  `pressReturn`. Needs Accessibility. -/
  | typeText (pid : Nat) (text : String) (pressReturn : Bool)
  /-- `http` with a body of parts the host assembles and an optional secret header (OpenAI's
  transcription request: multipart framing from Lean, the clip's WAV and the key from the
  host). -/
  | upload (method url : String) (headers : List (String × String)) (secret : Option Secret)
      (body : List Part) (timeoutMs : Nat)
  /-- The host may drop the clip's samples. -/
  | forgetClip (clip : Nat)
  /-- Open `target` with its default app (the Finder for a folder, the default editor for a
  text file, System Settings for its URLs): a path (`~/` is the home folder) or a URL with a
  scheme. -/
  | openItem (target : String)
  /-- Whether an app with this bundle identifier is running. -/
  | appRunning (bundleId : String)
  /-- The value of `key` in the defaults domain `domain` (`defaults read domain key`), as UTF-8
  text: a string as it is, a number or a boolean as its text (booleans as `1` or `0`). -/
  | readDefault (domain key : String)
  /-- Create the directory and its missing parents, each private (mode 700); `done` if it is
  already a directory. -/
  | makeDir (path : String)
  /-- Load the image at `source` (a file path, `~/` for the home folder, or an `http`/`https`
  URL) and answer its size in pixels (`Reply.image`); the host keeps the decoded pixels under
  `source` and paints them for `Style.image`s that name it. Lean never sees the pixels. An image
  the host already holds is answered from what it holds, unless `reload`, which reads `source`
  again. -/
  | loadImage (source : String) (reload : Bool)
  /-- Delete the Keychain item `account` (`Secret.Source.keychain`): `done`, also when there is
  none. -/
  | forgetSecret (account : String)
deriving Repr, BEq, Inhabited
```

`lean/Cairn/Effects.lean`, lines 69–130

The runtime keeps a table of pending requests and delivers a reply only to a pending id, in a
shape that answers its kind. A duplicate, late or misshapen reply is dropped before the app sees
it. A Save button asks for a `writeFile` and a Load button a `readFile`, and `receive` takes
the `done` and the `bytes` that come back:

```lean
inductive Reply where
  /-- `writeFile`, `appendFile`, `deleteFile`, `makeDir`, `forgetSecret` and `playSound`
  succeeded. -/
  | done
  /-- `readFile`'s contents, or `readDefault`'s value. -/
  | bytes (data : ByteArray)
  /-- An HTTP response, whatever its status. -/
  | http (status : Nat) (headers : List (String × String)) (body : ByteArray)
  /-- Any request can fail. -/
  | failed (fault : Fault) (message : String)
  /-- `listDir`'s names. -/
  | names (names : List String)
  /-- `frontmostApp`'s process id and name (empty when it has none). -/
  | app (pid : Nat) (name : String)
  /-- `permission`'s or `appRunning`'s answer. -/
  | flag (granted : Bool)
  /-- `loadImage`'s answer: the image's size in pixels (after its orientation is applied). -/
  | image (width height : Nat)
deriving Repr, BEq, Inhabited

/-- Whether a reply has the shape that answers a request of kind `k`. -/
def Reply.answers : Request.Kind → Reply → Bool
  | _, .failed .. => true
  | .readFile, .bytes _ => true
  | .writeFile, .done | .playSound, .done | .appendFile, .done | .deleteFile, .done => true
  | .typeText, .done | .forgetClip, .done | .openItem, .done | .makeDir, .done => true
  | .forgetSecret, .done => true
  | .readDefault, .bytes _ => true
  | .http, .http .. | .upload, .http .. => true
  | .listDir, .names _ => true
  | .frontmostApp, .app .. => true
  | .permission, .flag _ | .appRunning, .flag _ => true
  | .loadImage, .image .. => true
  | _, _ => false
```

`lean/Cairn/Effects.lean`, lines 164–197

## Subscriptions

Some inputs keep coming: a tick every second, a file that changes, the microphone, a global key.
An app doesn't start and stop them. It says which ones it wants in each state, and after every
step the runtime starts exactly the new ones and stops exactly the ones no longer wanted. An event
from a stopped subscription never reaches the app, however late it arrives.

```lean
/-- An outside input an app asks for, as data derived from its state. -/
inductive Sub where
  /-- A tick every `ms` milliseconds (at least 1), from the host. -/
  | every (ms : Nat)
  /-- `changed` whenever the file at `path` changes: written, replaced, created or removed. -/
  | watchFile (path : String)
  /-- Record `clip` from the microphone while active: `started` once the microphone is running,
  then `audio`; or `failed` if it can't start. Stopping it stops the microphone. The host keeps
  the samples for `Part.wav`. Needs Microphone. -/
  | record (clip : Nat)
  /-- The key with virtual key code `code` (with `modifier`, the `NSEvent.ModifierFlags` bit
  that tells a modifier key's press from its release): `keyDown`, `keyUp`, and `otherKey` for
  any other key pressed while it is down. Needs Accessibility. -/
  | globalKey (code : Nat) (modifier : Option Nat)
  /-- Keep the host's decoded images (`Request.loadImage`) within about `bytes` bytes of pixels
  while active: past it the host drops the images used least recently, never one the latest
  frame draws nor the one it just loaded, and reports each with `evicted` (^1011). Without it
  the host keeps every image. The smallest budget of those active wins. -/
  | imageCache (bytes : Nat)
deriving Repr, DecidableEq, Inhabited
```

`lean/Cairn/Effects.lean`, lines 201–220

## Putting it together

The machine gains its `receive`:

```lean
def machine : Machine State := { init := {}, moves := moves%, receive }
```

`test/fixture/lean/Fixture.lean`, line 516

`toApp` carries it into the `App`, which also has the app's subscriptions and the effects to run
at launch, once the clock is known. The fixture has neither. A stopwatch would set both on what
`toApp` returns: a tick every second, and a `readFile` of its saved laps at launch.

```lean
structure App (S : Type) where
  init : S
  /-- What the app shows: at most one window (a later window is ignored), panels and status
  items. An app with no window is an accessory app (no Dock icon, no main menu). -/
  surfaces : List (Surface S)
  /-- A person's moves: every action names a control on screen. -/
  update : S → Action → S × List Effect
  /-- The outside world: the clock, timers, replies and subscription events
  (docs/effects.md). Ignored by default. -/
  receive : S → Msg → S × List Effect := fun s _ => (s, [])
  /-- The outside inputs the app wants in this state. The runtime diffs them after every
  delivery and starts and stops subscriptions to match. -/
  subscriptions : S → List Sub := fun _ => []
  /-- Effects to run once, when the first clock arrives (so timers start from a real time). -/
  initEffects : List Effect := []
  /-- Every claim the app makes, from the claim commands. -/
  claims : List ClaimInfo
  /-- The control that has keyboard focus at launch, if it is focusable there. -/
  initFocus : Option ControlRef := none
  /-- How many requests of capped kinds (`Request.Kind.capped`: `http`, `upload`, `loadImage`)
  may be with the host at once (at least 1). The runtime queues the rest (docs/effects.md,
  "Requests in flight"). -/
  maxInFlight : Nat := 6
  /-- The window's smallest content size in this state, in points. The host keeps the window
  at least this big, so a person can't drag it smaller (`NSWindow.contentMinSize`; trusted,
  ^1010), and the view can be proved good at every size from it up (with `Grid.minBox`, for
  instance). `0 × 0`, no minimum, by default. -/
  minSize : S → Size := fun _ => ⟨0, 0⟩
  /-- The scroll boxes and virtual lists (by `Style.scrollRef`) whose offset, and what the
  runtime knows of their rows, outlive their leaving the view in this state: a list on a tab not
  shown comes back where it was. Any other box's offset is forgotten when it leaves the tree
  (docs/runtime.md, "Scrolling"). None by default. -/
  keepScroll : S → List ControlRef := fun _ => []
```

`lean/Cairn/App.lean`, lines 137–169

## Proving things about the world

Claims about the outside world are proved the same way. An invariant of a machine with `receive`
has a third clause, `receive`, proving the property is kept by every message too. It then holds
whatever the host sends, in any order with the person's actions. The fixture's ^7 has one: the
timer's message changes nothing it talks about
([chapter 2](https://cairn.iamnbutler.workers.dev/docs/guide/moves-and-flows.md#invariants)). An app
with requests can prove that pending requests always have ids below the next one, so a reply to a
later request is never taken for an earlier one, or that a tick arriving after Stop changes
nothing.

## What the host promises

Each kind of effect is an **assumption**, an `assume` claim saying what the host does ("writeFile
is atomic, and replies done only when the bytes are there"), checked by a fuzzer against the real
host. They are listed on the [trusted base](https://cairn.iamnbutler.workers.dev/docs/internals/trusted-base.md) page, and
[writing host effects](https://cairn.iamnbutler.workers.dev/docs/internals/host-effects.md) covers adding one.

From https://cairn.iamnbutler.workers.dev/docs/guide/effects/. All of Cairn's docs for language models: https://cairn.iamnbutler.workers.dev/llms.txt