Mercurial > urweb

comparison doc/manual.tex @ 652:9db6880184d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Revising manual, through main syntax section
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Mar 2009 10:16:59 -0400
parents 33500a15b872
children a0f2b070af01
comparison
equal deleted inserted replaced
651:bab524996fca 652:9db6880184d0
27 \begin{itemize} 27 \begin{itemize}
28 \item Suffer from any kinds of code-injection attacks 28 \item Suffer from any kinds of code-injection attacks
29 \item Return invalid HTML 29 \item Return invalid HTML
30 \item Contain dead intra-application links 30 \item Contain dead intra-application links
31 \item Have mismatches between HTML forms and the fields expected by their handlers 31 \item Have mismatches between HTML forms and the fields expected by their handlers
32 \item Include client-side code that makes incorrect assumptions about the ``AJAX''-style services that the remote web server provides
32 \item Attempt invalid SQL queries 33 \item Attempt invalid SQL queries
33 \item Use improper marshaling or unmarshaling in communication with SQL databases 34 \item Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers
34 \end{itemize} 35 \end{itemize}
35 36
36 This type safety is just the foundation of the Ur/Web methodology. It is also possible to use metaprogramming to build significant application pieces by analysis of type structure. For instance, the demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The type system guarantees that the admin interface sub-application that comes out will always be free of the above-listed bugs, no matter which well-typed table description is given as input. 37 This type safety is just the foundation of the Ur/Web methodology. It is also possible to use metaprogramming to build significant application pieces by analysis of type structure. For instance, the demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The type system guarantees that the admin interface sub-application that comes out will always be free of the above-listed bugs, no matter which well-typed table description is given as input.
37 38
38 The Ur/Web compiler also produces very efficient object code that does not use garbage collection. These compiled programs will often be even more efficient than what most programmers would bother to write in C. 39 The Ur/Web compiler also produces very efficient object code that does not use garbage collection. These compiled programs will often be even more efficient than what most programmers would bother to write in C. The compiler also generates JavaScript versions of client-side code, with no need to write those parts of applications in a different language.
39 40
40 \medskip 41 \medskip
41 42
42 The official web site for Ur is: 43 The official web site for Ur is:
43 \begin{center} 44 \begin{center}
152 153
153 \begin{center} 154 \begin{center}
154 \begin{tabular}{rl} 155 \begin{tabular}{rl}
155 \textbf{\LaTeX} & \textbf{ASCII} \\ 156 \textbf{\LaTeX} & \textbf{ASCII} \\
156 $\to$ & \cd{->} \\ 157 $\to$ & \cd{->} \\
158 $\longrightarrow$ & \cd{-->} \\
157 $\times$ & \cd{*} \\ 159 $\times$ & \cd{*} \\
158 $\lambda$ & \cd{fn} \\ 160 $\lambda$ & \cd{fn} \\
159 $\Rightarrow$ & \cd{=>} \\ 161 $\Rightarrow$ & \cd{=>} \\
162 $\Longrightarrow$ & \cd{==>} \\
160 $\neq$ & \cd{<>} \\ 163 $\neq$ & \cd{<>} \\
161 $\leq$ & \cd{<=} \\ 164 $\leq$ & \cd{<=} \\
162 $\geq$ & \cd{>=} \\ 165 $\geq$ & \cd{>=} \\
163 \\ 166 \\
164 $x$ & Normal textual identifier, not beginning with an uppercase letter \\ 167 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
180 &&& \mt{Unit} & \textrm{the trivial constructor} \\ 183 &&& \mt{Unit} & \textrm{the trivial constructor} \\
181 &&& \mt{Name} & \textrm{field names} \\ 184 &&& \mt{Name} & \textrm{field names} \\
182 &&& \kappa \to \kappa & \textrm{type-level functions} \\ 185 &&& \kappa \to \kappa & \textrm{type-level functions} \\
183 &&& \{\kappa\} & \textrm{type-level records} \\ 186 &&& \{\kappa\} & \textrm{type-level records} \\
184 &&& (\kappa\times^+) & \textrm{type-level tuples} \\ 187 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
188 &&& X & \textrm{variable} \\
189 &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\
185 &&& \_\_ & \textrm{wildcard} \\ 190 &&& \_\_ & \textrm{wildcard} \\
186 &&& (\kappa) & \textrm{explicit precedence} \\ 191 &&& (\kappa) & \textrm{explicit precedence} \\
187 \end{array}$$ 192 \end{array}$$
188 193
189 Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions. 194 Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
197 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\ 202 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
198 &&& \hat{x} & \textrm{constructor variable} \\ 203 &&& \hat{x} & \textrm{constructor variable} \\
199 \\ 204 \\
200 &&& \tau \to \tau & \textrm{function type} \\ 205 &&& \tau \to \tau & \textrm{function type} \\
201 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\ 206 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
207 &&& X \longrightarrow \tau & \textrm{kind-polymorphic function type} \\
202 &&& \$ c & \textrm{record type} \\ 208 &&& \$ c & \textrm{record type} \\
203 \\ 209 \\
204 &&& c \; c & \textrm{type-level function application} \\ 210 &&& c \; c & \textrm{type-level function application} \\
205 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\ 211 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
206 \\ 212 \\
213 &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\
214 \\
207 &&& () & \textrm{type-level unit} \\ 215 &&& () & \textrm{type-level unit} \\
208 &&& \#X & \textrm{field name} \\ 216 &&& \#X & \textrm{field name} \\
209 \\ 217 \\
210 &&& [(c = c)^*] & \textrm{known-length type-level record} \\ 218 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
211 &&& c \rc c & \textrm{type-level record concatenation} \\ 219 &&& c \rc c & \textrm{type-level record concatenation} \\
212 &&& \mt{fold} & \textrm{type-level record fold} \\ 220 &&& \mt{map} & \textrm{type-level record map} \\
213 \\ 221 \\
214 &&& (c,^+) & \textrm{type-level tuple} \\ 222 &&& (c,^+) & \textrm{type-level tuple} \\
215 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\ 223 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
216 \\ 224 \\
217 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\ 225 &&& [c \sim c] \Rightarrow \tau & \textrm{guarded type} \\
218 \\ 226 \\
219 &&& \_ :: \kappa & \textrm{wildcard} \\ 227 &&& \_ :: \kappa & \textrm{wildcard} \\
220 &&& (c) & \textrm{explicit precedence} \\ 228 &&& (c) & \textrm{explicit precedence} \\
221 \\ 229 \\
222 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\ 230 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
271 \\ 279 \\
272 &&& e \; e & \textrm{function application} \\ 280 &&& e \; e & \textrm{function application} \\
273 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\ 281 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
274 &&& e [c] & \textrm{polymorphic function application} \\ 282 &&& e [c] & \textrm{polymorphic function application} \\
275 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\ 283 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
284 &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\
276 \\ 285 \\
277 &&& \{(c = e,)^*\} & \textrm{known-length record} \\ 286 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
278 &&& e.c & \textrm{record field projection} \\ 287 &&& e.c & \textrm{record field projection} \\
279 &&& e \rc e & \textrm{record concatenation} \\ 288 &&& e \rc e & \textrm{record concatenation} \\
280 &&& e \rcut c & \textrm{removal of a single record field} \\ 289 &&& e \rcut c & \textrm{removal of a single record field} \\
281 &&& e \rcutM c & \textrm{removal of multiple record fields} \\ 290 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
282 &&& \mt{fold} & \textrm{fold over fields of a type-level record} \\
283 \\ 291 \\
284 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\ 292 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
285 \\ 293 \\
286 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\ 294 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
287 \\ 295 \\