io

readFile

extern readFile (path : String) : IO (Either String String)

The contents of a file, or why it could not be read.

writeFile

extern writeFile (path : String) (content : String) : IO (Either String Unit)

Writes a file (replacing what was there).

appendFile

extern appendFile (path : String) (content : String) : IO (Either String Unit)

Appends to a file (creating it).

getEnv

extern getEnv (name : String) : IO (Option String)

An environment variable’s value, if it is set.

getArgs

extern getArgs : IO (List String)

The program’s arguments.

listDir

extern listDir (path : String) : IO (Either String (List String))

The names in a directory, in dictionary order (without . and ..).

fileExists

extern fileExists (path : String) : IO Bool

Whether a file or a directory exists.

createDir

extern createDir (path : String) : IO (Either String Unit)

Makes a directory (and its parents).

removeFile

extern removeFile (path : String) : IO (Either String Unit)

Removes a file.

putErr

extern putErr (text : String) : IO Unit

Writes a line to the error output.

runProcess

extern runProcess (program : String) (args : List String) (stdin : String) : IO (Either String (Nat × (String × String)))

Runs a program with arguments and input, and waits: its exit code, output and error output.

spawnProcess

extern spawnProcess (program : String) (args : List String) (stdin : String) : IO (Either String String)

Starts a program with arguments and input without waiting: a handle for awaitProcess.

awaitProcess

extern awaitProcess (job : String) : IO (Either String (Nat × (String × String)))

Waits for a started program: as runProcess gives.

monadIO

instance monadIO : Monad IO

IO is a monad; its pure and bind are the IO primitives (IO.pure, IO.bind).

seq_

def seq_ {A : Type} {B : Type} (m : IO A) (k : IO B) : IO B

Runs m, discards its result, then runs k.

when

def when (b : Bool) (m : IO Unit) : IO Unit

Runs the action only when the condition is true.

unless

def unless (b : Bool) (m : IO Unit) : IO Unit

Runs the action only when the condition is false.

mapM_

def mapM_ {A : Type} (f : A -> IO Unit) (xs : List A) : IO Unit

Runs f on each list element in order, discarding the results.

expectEither

def expectEither {E : Type} {A : Type} (m : IO (Either E A)) : IO (Either E A)

Identity on fallible actions; e? expands through it so a type mismatch is reported at e with the expected IO (Either E A) shape.

mapIO

def mapIO {A : Type} {B : Type} (f : A -> IO B) (xs : List A) : IO (List B)

Runs f on each list element in order and collects the results; ys <- for x in xs do ... expands to it.

forIO

def forIO {A : Type} {B : Type} (xs : List A) (f : A -> IO B) : IO (List B)

mapIO with the list first, so the element type is known when the loop body is elaborated; target of ys <- for x in xs do ....

sequence_

def sequence_ (ms : List (IO Unit)) : IO Unit

Runs each action of a list in order.

replicateM_

def replicateM_ (n : Nat) (m : IO Unit) : IO Unit

Runs an action n times.

forInList

def forInList {A : Type} {S : Type} (xs : List A) (s : S) (f : A -> S -> IO S) : IO S

Expansion of for x in xs do ...: runs f on each element in order, threading a state through.

forInListCtl

def forInListCtl {A : Type} {S : Type} (xs : List A) (s : S) (f : A -> S -> IO (LoopCtl S)) : IO S

Stateful loop over a list whose body may stop early with loopStop; used for loops with break or continue.

forInListR

def forInListR {A : Type} {R : Type} {S : Type} (xs : List A) (s : S) (f : A -> S -> IO (LoopStep R S)) : IO (Either R S)

Stateful loop over a list whose body may break or return early; yields left v for an early return and right s when the loop ends.

forFrom_

def forFrom_ (lo : Nat) (n : Nat) (f : Nat -> IO Unit) : IO Unit

Runs f lo, f (lo+1), …, n times in order.

forRange_

def forRange_ (n : Nat) (f : Nat -> IO Unit) : IO Unit

Runs f 0, f 1, …, f (n-1) in order.

pureE

def pureE {E : Type} {A : Type} (a : A) : IO (Either E A)

A fallible action that succeeds with the given value.

throwE

def throwE {E : Type} {A : Type} (e : E) : IO (Either E A)

A fallible action that fails with the given error.

bindE

def bindE {E : Type} {A : Type} {B : Type} (m : IO (Either E A)) (k : A -> IO (Either E B)) : IO (Either E B)

Sequences fallible actions, continuing only on success and stopping at the first failure.

catchE

def catchE {E : Type} {A : Type} (m : IO (Either E A)) (h : E -> IO (Either E A)) : IO (Either E A)

Runs a fallible action and hands any failure to the handler.

liftE

def liftE {E : Type} {A : Type} (m : IO A) : IO (Either E A)

Lifts an infallible action into a fallible one.

orElseIO

def orElseIO {E : Type} {A : Type} (m : IO (Either E A)) (alt : IO (Either E A)) : IO (Either E A)

Runs a fallible action and falls back to alt if it fails.

Job

record Job

An external program to run: program name, arguments and standard input.

startJob

def startJob (j : Job) : IO (Either String String)

Starts an external program, returning a process handle or an error.

awaitJob

def awaitJob (h : Either String String) : IO (Either String (Nat × (String × String)))

Waits for a started (or failed-to-start) job and returns its exit code, stdout and stderr, as runProcess does.

Task

data Task (A : Type)

A result that can be awaited later: an already computed value, or a running external process with a function converting its result.

async

def async {A : Type} (e : IO A) : IO (Task A)

Starts a task; currently the action runs immediately and its result is stored.

awaitTask

def awaitTask {A : Type} (t : Task A) : IO A

Waits for a task to finish and returns its result; written await t inside do.

spawnTask

def spawnTask (j : Job) : IO (Task (Either String (Nat × (String × String))))

Starts an external program as a task that runs concurrently with other tasks.

runWindow

def runWindow (fuel : Nat) (running : List (Either String String)) (pending : List Job) : IO (List (Either String (Nat × (String × String))))

Sliding-window job runner: awaits the oldest running job and starts the next pending one, with fuel counting remaining jobs.

runAll

def runAll (limit : Nat) (jobs : List Job) : IO (List (Either String (Nat × (String × String))))

Runs external programs with at most limit (at least one) in parallel, returning results in the order of jobs.

Bool.whenTrue

def Bool.whenTrue (b : Bool) : Option (b = true)

The proof that a Boolean is true, when it is.

IO.Ensured

def IO.Ensured (R : Type) (p : R -> Bool) : Type

What an external function with ensures p gives: a value that passed p, with the proof, or the failure.

IO.ensure

def IO.ensure {R : Type} (broken : String) (p : R -> Bool) (m : IO (Either String R)) : IO.Ensured R p

An external function’s result checked against its contract p: a value that does not pass is the failure broken.