Mercurial > urweb

comparison doc/manual.tex @ 1348:8a169fc0838b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
1347:b106ca8200b1 1348:8a169fc0838b
960 \Gamma \vdash \tau :: \mt{Type} 960 \Gamma \vdash \tau :: \mt{Type}
961 } 961 }
962 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$ 962 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$
963 963
964 $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{ 964 $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{
965 \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind} 965 \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind} \; \tau
966 & \Gamma \vdash e_2 :: \mt{Basis}.\mt{transaction} \; \{\} 966 & \Gamma \vdash e_2 :: \tau \to \mt{Basis}.\mt{transaction} \; \{\}
967 }$$ 967 }$$
968 968
969 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ 969 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
970 \Gamma \vdash c :: \kappa 970 \Gamma \vdash c :: \kappa
971 }$$ 971 }$$
2091 2091
2092 The HTTP standard suggests that GET requests only be used in ways that generate no side effects. Side effecting operations should use POST requests instead. The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis. Any page that may have a side effect must be accessed through a form, all of which use POST requests, or via a direct call to a page handler with some argument of type $\mt{Basis.postBody}$. A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions. Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{<body onload=\{...\}>} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers. 2092 The HTTP standard suggests that GET requests only be used in ways that generate no side effects. Side effecting operations should use POST requests instead. The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis. Any page that may have a side effect must be accessed through a form, all of which use POST requests, or via a direct call to a page handler with some argument of type $\mt{Basis.postBody}$. A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions. Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{<body onload=\{...\}>} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers.
2093 2093
2094 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. 2094 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.
2095 2095
2096 \subsection{Tasks}
2097
2098 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:
2099
2100 $$\begin{array}{l}
2101 \mt{con} \; \mt{task\_kind} :: \mt{Type} \to \mt{Type} \\
2102 \mt{val} \; \mt{initialize} : \mt{task\_kind} \; \mt{unit} \\
2103 \mt{val} \; \mt{clientLeaves} : \mt{task\_kind} \; \mt{client}
2104 \end{array}$$
2105
2106 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}$.
2107
2108 The currently supported task kinds are:
2109 \begin{itemize}
2110 \item $\mt{initialize}$: Code that is run in each freshly-allocated request context.
2111 \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.
2112 \end{itemize}
2113
2096 2114
2097 \section{The Foreign Function Interface} 2115 \section{The Foreign Function Interface}
2098 2116
2099 It is possible to call your own C and JavaScript code from Ur/Web applications, via the foreign function interface (FFI). The starting point for a new binding is a \texttt{.urs} signature file that presents your external library as a single Ur/Web module (with no nested modules). Compilation conventions map the types and values that you use into C and/or JavaScript types and values. 2117 It is possible to call your own C and JavaScript code from Ur/Web applications, via the foreign function interface (FFI). The starting point for a new binding is a \texttt{.urs} signature file that presents your external library as a single Ur/Web module (with no nested modules). Compilation conventions map the types and values that you use into C and/or JavaScript types and values.
2100 2118