diff doc/manual.tex @ 1348:8a169fc0838b

Change tasks to support parametric code; add clientLeaves
author Adam Chlipala <adam@chlipala.net>
date Sat, 18 Dec 2010 14:17:45 -0500
parents b106ca8200b1
children 87156c44824f
line wrap: on
line diff
--- a/doc/manual.tex	Sat Dec 18 10:56:31 2010 -0500
+++ b/doc/manual.tex	Sat Dec 18 14:17:45 2010 -0500
@@ -962,8 +962,8 @@
 \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 @@
 
 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}