Mercurial > urweb
comparison doc/manual.tex @ 657:74140535291d
Describe folders
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 12 Mar 2009 11:36:27 -0400 |
| parents | 3be5e6f01c32 |
| children | 81c5c2674215 |
comparison
equal
deleted
inserted
replaced
| 656:3be5e6f01c32 | 657:74140535291d |
|---|---|
| 1107 \\ | 1107 \\ |
| 1108 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\ | 1108 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\ |
| 1109 \\ | 1109 \\ |
| 1110 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} | 1110 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} |
| 1111 \end{array}$$ | 1111 \end{array}$$ |
| 1112 | |
| 1113 Another important generic Ur element comes at the beginning of \texttt{top.urs}. | |
| 1114 | |
| 1115 $$\begin{array}{l} | |
| 1116 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\ | |
| 1117 \\ | |
| 1118 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\ | |
| 1119 \hspace{.1in} \to (\mt{nm} :: \mt{Name} \to \mt{v} :: \mt{K} \to \mt{r} :: \{\mt{K}\} \to [[\mt{nm}] \sim \mt{r}] \Rightarrow \\ | |
| 1120 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\ | |
| 1121 \hspace{.1in} \to \mt{tf} \; [] \\ | |
| 1122 \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r} | |
| 1123 \end{array}$$ | |
| 1124 | |
| 1125 For a type-level record $\mt{r}$, a $\mt{folder} \; \mt{r}$ encodes a permutation of $\mt{r}$'s elements. The $\mt{fold}$ function can be called on a $\mt{folder}$ to iterate over the elements of $\mt{r}$ in that order. $\mt{fold}$ is parameterized on a type-level function to be used to calculate the type of each intermediate result of folding. After processing a subset $\mt{r'}$ of $\mt{r}$'s entries, the type of the accumulator should be $\mt{tf} \; \mt{r'}$. The next two expression arguments to $\mt{fold}$ are the usual step function and initial accumulator, familiar from fold functions over lists. The final two arguments are the record to fold over and a $\mt{folder}$ for it. | |
| 1126 | |
| 1127 The Ur compiler treates $\mt{folder}$ like a constructor class, using built-in rules to infer $\mt{folder}$s for records with known structure. The order in which field names are mentioned in source code is used as a hint about the permutation that the programmer would like. | |
| 1112 | 1128 |
| 1113 | 1129 |
| 1114 \section{The Ur/Web Standard Library} | 1130 \section{The Ur/Web Standard Library} |
| 1115 | 1131 |
| 1116 \subsection{Transactions} | 1132 \subsection{Transactions} |