Tasks

In many web applications, it's useful to run code at points other than requests from browsers. Ur/Web's task mechanism facilitates this. A type family of task kinds is in the standard library:

$$\begin{array}{l} \mathsf{con} \; \mathsf{task\_kind} :: \math... ...athsf{int} \to \mathsf{task\_kind} \; \mathsf{unit} \end{array}$$

A task kind names a particular extension point of generated applications, where the type parameter of a task kind describes which extra input data is available at that extension point. Add task code with the special declaration form $\mathsf{task} \; e_1 = e_2$ , where $e_1$ is a task kind with data $\tau$ , and $e_2$ is a function from $\tau$ to $\mathsf{transaction} \; \mathsf{unit}$ .

The currently supported task kinds are:

• $\mathsf{initialize}$ : Code that is run when the application starts up.
• $\mathsf{clientLeaves}$ : Code that is run for each client that the runtime system decides has surfed away. When a request that generates a new client handle is aborted, that handle will still eventually be passed to $\mathsf{clientLeaves}$ task code, even though the corresponding browser was never informed of the client handle's existence. In other words, in general, $\mathsf{clientLeaves}$ handlers will be called more times than there are actual clients.
• $\mathsf{periodic} \; n$ : Code that is run when the application starts up and then every $n$ seconds thereafter.