Cairn.Effects
lean/Cairn/Effects.lean
The outside world as data (docs/effects.md): the time the host reports, the requests an app
can make and the replies they get, and the subscriptions an app can ask for. Cairn.Input
builds Effect and Event on these; the runtime's handling is Cairn.Runtime.World.
Structures 3
Time : Type
The host's clock. mono is monotonic milliseconds (timers and durations use it); wall
is milliseconds since the Unix epoch, UTC, and zone the local offset from UTC in seconds
(for dates).
mono : Natwall : Intzone : IntSecret : Type
A header whose value comes from a secret the host reads when it sends the request, so the
secret never reaches Lean, a frame or a log: header: scheme ++ value, where value is read
from source.
Level : Type
One 20 ms window of a recording (320 samples at 16 kHz), as integers.
sumSq : NatThe sum of its samples' squares.
peak : NatIts largest absolute sample (Int16.min counts as Int16.max).
Inductive types 11
Fault : Type
Why a request failed. Failure is an ordinary reply.
Permission : Type
A permission the person grants the app in System Settings (TCC).
accessibility : Permission
Privacy & Security › Accessibility: typing into other apps, hearing a global key.
microphone : Permission
Privacy & Security › Microphone: recording.
Part : Type
A part of an upload body: bytes Lean built, or audio the host holds.
Source : Type
Where the host reads a secret's value as it sends a request.
env (file name : String) : Source
The environment variable name if set and not empty, else name's line in the
KEY=value file file (Yap's API key).
keychain (account : String) : Source
The generic password item account in the login keychain, under the app's bundle
identifier as its service (docs/effects.md, "Secrets in the Keychain").
Request : Type
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).
readFile (path : String) : Request
writeFile (path : String) (data : ByteArray) : Request
Replace the file atomically, creating missing parent directories.
playSound (name : String) : Request
A named system sound ("Tink", "Pop", "Basso", …).
http (method url : String) (headers : List (String × String)) (body : ByteArray) (timeoutMs : Nat) (secret : Option Secret := none) (capture : List (String × String) := []) (redact : Bool := false) : Request
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.
appendFile (path : String) (data : ByteArray) : Request
Append to the file, creating it (mode 600) and missing parent directories.
listDir (path : String) : Request
The names in a directory (not . and ..), sorted by their UTF-8 bytes.
deleteFile (path : String) : Request
Remove a file or a symbolic link; never a directory.
frontmostApp : Request
The app in front: its process id and name.
permission (p : Permission) (prompt : Bool) : Request
Whether the app holds p; with prompt, the system also asks the person if it doesn't.
typeText (pid : Nat) (text : String) (pressReturn : Bool) : Request
Bring process pid to the front and type text into it as key events, then Return if
pressReturn. Needs Accessibility.
upload (method url : String) (headers : List (String × String)) (secret : Option Secret) (body : List Part) (timeoutMs : Nat) : Request
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).
forgetClip (clip : Nat) : Request
The host may drop the clip's samples.
openItem (target : String) : Request
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.
appRunning (bundleId : String) : Request
Whether an app with this bundle identifier is running.
readDefault (domain key : String) : Request
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).
makeDir (path : String) : Request
Create the directory and its missing parents, each private (mode 700); done if it is
already a directory.
loadImage (source : String) (reload : Bool) : Request
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.images 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.
forgetSecret (account : String) : Request
Delete the Keychain item account (Secret.Source.keychain): done, also when there is
none.
Kind : Type
The kind of a request, without its payload: what the runtime remembers while it is pending.
Reply : Type
done : Reply
writeFile, appendFile, deleteFile, makeDir, forgetSecret and playSound
succeeded.
bytes (data : ByteArray) : Reply
readFile's contents, or readDefault's value.
http (status : Nat) (headers : List (String × String)) (body : ByteArray) : Reply
An HTTP response, whatever its status.
names (names : List String) : Reply
listDir's names.
app (pid : Nat) (name : String) : Reply
frontmostApp's process id and name (empty when it has none).
flag (granted : Bool) : Reply
permission's or appRunning's answer.
image (width height : Nat) : Reply
loadImage's answer: the image's size in pixels (after its orientation is applied).
Sub : Type
An outside input an app asks for, as data derived from its state.
every (ms : Nat) : Sub
A tick every ms milliseconds (at least 1), from the host.
watchFile (path : String) : Sub
changed whenever the file at path changes: written, replaced, created or removed.
record (clip : Nat) : Sub
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.
globalKey (code : Nat) (modifier : Option Nat) : Sub
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.
imageCache (bytes : Nat) : Sub
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.
SubEvent : Type
What an active subscription reports.
tick : SubEvent
every's tick.
changed : SubEvent
watchFile's file changed.
audio (frames peak : Nat) (windows : List Level) : SubEvent
record: frames more samples, their largest absolute value peak, and the 20 ms
windows they complete, in order from the start of the clip.
started (t : Nat) : SubEvent
keyDown (t : Nat) : SubEvent
globalKey: the key went down or up, or another key went down while it was held, at
monotonic milliseconds t (the clock of Time.mono).
keyUp (t : Nat) : SubEvent
otherKey (t : Nat) : SubEvent
failed (fault : Fault) (message : String) : SubEvent
The subscription could not run (a permission missing, no microphone). It may still be running; an app stops it by not asking for it.
evicted (source : String) : SubEvent
imageCache: the host dropped source's pixels; sent after they are gone. An app that
forgets the image when it hears this (Images.evicted, which also stops waiting for its
loads) never takes an image for ready while the host has no pixels for it
(Images.Cache.ready_held).
SubCmd : Type
Runtime → host: start or stop a subscription, under the runtime's id for it.
Msg : Type
Runtime → app, through App.receive: the outside world.
timer (name : String) : Msg
A timer the app set has come due.
Definitions 5
bearer (account : String) : Secret
Authorization: Bearer <value of the Keychain item account>.
kind : Request → Kind
redact : Request → Bool
capped : Kind → Bool
The kinds that count toward the cap on requests in flight (App.maxInFlight, docs/effects.md
"Requests in flight"): the ones that can take seconds on the network. The others (files, sounds,
permissions, typing) are sent at once.
answers : Request.Kind → Reply → Bool
Whether a reply has the shape that answers a request of kind k.
Instances 43
instReprByteArray_cairn : Repr ByteArrayByte payloads print as their size. (Core has no Repr ByteArray.)
instInhabitedTime : Inhabited Time
instDecidableEqTime : DecidableEq Time
instReprTime : Repr Time
instDecidableEqFault : DecidableEq Fault
instReprFault : Repr Fault
instInhabitedFault : Inhabited Fault
instReprPermission : Repr Permission
instDecidableEqPermission : DecidableEq Permission
instInhabitedPermission : Inhabited Permission
instBEqPart : BEq Part
instInhabitedPart : Inhabited Part
instReprPart : Repr Part
instInhabitedSource : Inhabited Source
instDecidableEqSource : DecidableEq Source
instReprSource : Repr Source
instReprSecret : Repr Secret
instInhabitedSecret : Inhabited Secret
instDecidableEqSecret : DecidableEq Secret
instInhabitedRequest : Inhabited Request
instReprRequest : Repr Request
instBEqRequest : BEq Request
instReprKind : Repr Kind
instDecidableEqKind : DecidableEq Kind
instInhabitedKind : Inhabited Kind
instReprReply : Repr Reply
instInhabitedReply : Inhabited Reply
instBEqReply : BEq Reply
instInhabitedSub : Inhabited Sub
instReprSub : Repr Sub
instDecidableEqSub : DecidableEq Sub
instInhabitedLevel : Inhabited Level
instReprLevel : Repr Level
instDecidableEqLevel : DecidableEq Level
instReprSubEvent : Repr SubEvent
instDecidableEqSubEvent : DecidableEq SubEvent
instInhabitedSubEvent : Inhabited SubEvent
instInhabitedSubCmd : Inhabited SubCmd
instDecidableEqSubCmd : DecidableEq SubCmd
instReprSubCmd : Repr SubCmd
instReprMsg : Repr Msg
instBEqMsg : BEq Msg
instInhabitedMsg : Inhabited Msg