comparison doc/manual.tex @ 1123:81ddb010751e

New release
author Adam Chlipala <adamc@hcoop.net>
date Tue, 12 Jan 2010 09:42:13 -0500
parents 8d0f195710f1
children f93dc2ea30c1
comparison
equal deleted inserted replaced
1122:85d194409b17 1123:81ddb010751e
1247 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} \\ 1247 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} \\
1248 \\ 1248 \\
1249 \mt{datatype} \; \mt{list} \; \mt{t} = \mt{Nil} \mid \mt{Cons} \; \mt{of} \; \mt{t} \times \mt{list} \; \mt{t} 1249 \mt{datatype} \; \mt{list} \; \mt{t} = \mt{Nil} \mid \mt{Cons} \; \mt{of} \; \mt{t} \times \mt{list} \; \mt{t}
1250 \end{array}$$ 1250 \end{array}$$
1251 1251
1252 The only unusual element of this list is the $\mt{blob}$ type, which stands for binary sequences. 1252 The only unusual element of this list is the $\mt{blob}$ type, which stands for binary sequences. Simple blobs can be created from strings via $\mt{Basis.textBlob}$. Blobs will also be generated from HTTP file uploads.
1253 1253
1254 Another important generic Ur element comes at the beginning of \texttt{top.urs}. 1254 Another important generic Ur element comes at the beginning of \texttt{top.urs}.
1255 1255
1256 $$\begin{array}{l} 1256 $$\begin{array}{l}
1257 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\ 1257 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\
1289 1289
1290 Ur is a pure language; we use Haskell's trick to support controlled side effects. The standard library defines a monad $\mt{transaction}$, meant to stand for actions that may be undone cleanly. By design, no other kinds of actions are supported. 1290 Ur is a pure language; we use Haskell's trick to support controlled side effects. The standard library defines a monad $\mt{transaction}$, meant to stand for actions that may be undone cleanly. By design, no other kinds of actions are supported.
1291 $$\begin{array}{l} 1291 $$\begin{array}{l}
1292 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\ 1292 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\
1293 \mt{val} \; \mt{transaction\_monad} : \mt{monad} \; \mt{transaction} 1293 \mt{val} \; \mt{transaction\_monad} : \mt{monad} \; \mt{transaction}
1294 \end{array}$$
1295
1296 For debugging purposes, a transactional function is provided for outputting a string on the server process' \texttt{stderr}.
1297 $$\begin{array}{l}
1298 \mt{val} \; \mt{debug} : \mt{string} \to \mt{transaction} \; \mt{unit}
1294 \end{array}$$ 1299 \end{array}$$
1295 1300
1296 \subsection{HTTP} 1301 \subsection{HTTP}
1297 1302
1298 There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies. Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure. 1303 There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies. Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure.
1552 \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\ 1557 \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\
1553 \mt{val} \; \mt{sql\_option\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; (\mt{option} \; \mt{t}) \\ 1558 \mt{val} \; \mt{sql\_option\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; (\mt{option} \; \mt{t}) \\
1554 \\ 1559 \\
1555 \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\ 1560 \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\
1556 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} 1561 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
1562 \end{array}$$
1563
1564 Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family.
1565 $$\begin{array}{l}
1566 \mt{con} \; \mt{serialized} :: \mt{Type} \to \mt{Type} \\
1567 \mt{val} \; \mt{serialize} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{serialized} \; \mt{t} \\
1568 \mt{val} \; \mt{deserialize} : \mt{t} ::: \mt{Type} \to \mt{serialized} \; \mt{t} \to \mt{t} \\
1569 \mt{val} \; \mt{sql\_serialized} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{serialized} \; \mt{t})
1557 \end{array}$$ 1570 \end{array}$$
1558 1571
1559 We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values. 1572 We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values.
1560 $$\begin{array}{l} 1573 $$\begin{array}{l}
1561 \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ 1574 \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\