Change tasks to support parametric code; add clientLeaves

1 files changed, 20 insertions, 2 deletions

diff --git a/doc/manual.tex b/doc/manual.tex
index a8d799d8..5a7110cb 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -962,8 +962,8 @@ $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\
 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$
 
 $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{
-  \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind}
-  & \Gamma \vdash e_2 :: \mt{Basis}.\mt{transaction} \; \{\}
+  \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind} \; \tau
+  & \Gamma \vdash e_2 :: \tau \to \mt{Basis}.\mt{transaction} \; \{\}
 }$$
 
 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
@@ -2093,6 +2093,24 @@ The HTTP standard suggests that GET requests only be used in ways that generate
 
 Ur/Web includes a kind of automatic protection against cross site request forgery attacks.  Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server.  Signing and signature checking are inserted automatically by the compiler.  This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect.
 
+\subsection{Tasks}
+
+In many web applications, it's useful to run code at points other than requests from browsers.  Ur/Web's \emph{task} mechanism facilitates this.  A type family of \emph{task kinds} is in the standard library:
+
+$$\begin{array}{l}
+\mt{con} \; \mt{task\_kind} :: \mt{Type} \to \mt{Type} \\
+\mt{val} \; \mt{initialize} : \mt{task\_kind} \; \mt{unit} \\
+\mt{val} \; \mt{clientLeaves} : \mt{task\_kind} \; \mt{client}
+\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 $\mt{task} \; e_1 = e_2$, where $e_1$ is a task kind with data $\tau$, and $e_2$ is a function from $\tau$ to $\mt{transaction} \; \mt{unit}$.
+
+The currently supported task kinds are:
+\begin{itemize}
+\item $\mt{initialize}$: Code that is run in each freshly-allocated request context.
+\item $\mt{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 $\mt{clientLeaves}$ task code, even though the corresponding browser was never informed of the client handle's existence.  In other words, in general, $\mt{clientLeaves}$ handlers will be called more times than there are actual clients.
+\end{itemize}
+
 
 \section{The Foreign Function Interface}