Mercurial > urweb
comparison 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 |
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 |