Mercurial > urweb

comparison demo/prose @ 773:74a090ff296e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
constraints demo
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 May 2009 12:01:55 -0400
parents 311ca1ae715d
children 412ccd97ab71
comparison
equal deleted inserted replaced
772:8ed1261f838c 773:74a090ff296e
98 98
99 <p>Here we see how we can abstract over common patterns of SQL queries. In particular, since standard SQL does not help much with queries over trees, we write a function for traversing an SQL tree, building an HTML representation, based on a user-provided function for rendering individual rows.</p> 99 <p>Here we see how we can abstract over common patterns of SQL queries. In particular, since standard SQL does not help much with queries over trees, we write a function for traversing an SQL tree, building an HTML representation, based on a user-provided function for rendering individual rows.</p>
100 100
101 <p>The signature of <tt>TreeFun.Make</tt> tells us that, to instantiate the functor, we must provide</p> 101 <p>The signature of <tt>TreeFun.Make</tt> tells us that, to instantiate the functor, we must provide</p>
102 <ol> 102 <ol>
103 <li> A primary key type <tt>key</tt></li> 103 <li>A primary key type <tt>key</tt></li>
104 <li> SQL field names <tt>id</tt> (for primary keys) and <tt>parent</tt> (for parent links)</li> 104 <li>SQL field names <tt>id</tt> (for primary keys) and <tt>parent</tt> (for parent links)</li>
105 <li> A type-level record <tt>cols</tt> of field names besides <tt>id</tt> and <tt>parent</tt></li> 105 <li>A type-level record <tt>cols</tt> of field names besides <tt>id</tt> and <tt>parent</tt></li>
106 <li> "Proofs" that <tt>id</tt> is distinct from <tt>parent</tt> and that neither of <tt>id</tt> and <tt>parent</tt> appears in <tt>cols</tt></li> 106 <li>"Proofs" that <tt>id</tt> is distinct from <tt>parent</tt> and that neither of <tt>id</tt> and <tt>parent</tt> appears in <tt>cols</tt></li>
107 <li> A witness that <tt>key</tt> belongs to the type class <tt>sql_injectable_prim</tt>, which indicates that both <tt>key</tt> and <tt>option key</tt> are fair game to use with SQL</li> 107 <li>A witness that <tt>key</tt> belongs to the type class <tt>sql_injectable_prim</tt>, which indicates that both <tt>key</tt> and <tt>option key</tt> are fair game to use with SQL</li>
108 <li> An SQL table <tt>tab</tt>, containing a field <tt>id</tt> of type <tt>key</tt>, a field <tt>parent</tt> of type <tt>option key</tt>, and every field of <tt>cols</tt></li> 108 <li>An SQL table <tt>tab</tt>, containing a field <tt>id</tt> of type <tt>key</tt>, a field <tt>parent</tt> of type <tt>option key</tt>, and every field of <tt>cols</tt></li>
109 </ol>
110
111 constraints.urp
112
113 <p>Ur/Web supports attaching SQL table constraints to table definitions. We've sprinkled a few such constraints throughout our examples so far, without mentioning them. This example shows a table with all four of the supported kinds of constraints. An application would generally try to avoid inserting data that violates constraints, but, in this example, we let you insert arbitrary data, so that you can see each of the constraints failing.</p>
114
115 <ol>
116 <li>The <tt>PRIMARY KEY</tt> constraint establishes the field of the table that we expect to use as a key in looking up specific rows. It is an error for two rows to share the same primary key.</li>
117 <li>The <tt>UNIQUE</tt> constraint is like <tt>PRIMARY KEY</tt>, with the difference being that a table may have many <tt>UNIQUE</tt> constraints but no more than one primary key.</li>
118 <li>The <tt>CHECK</tt> constraint declares a boolean assertion that must hold for every row of the table.</li>
119 <li>The <tt>FOREIGN KEY</tt> constraint declares that a row of the table references a particular column of another table, or of the same table, as we see in this example. It's a static type error to reference a foreign key column that has no <tt>PRIMARY KEY</tt> or <tt>UNIQUE</tt> constraint.</li>
109 </ol> 120 </ol>
110 121
111 sum.urp 122 sum.urp
112 123
113 <p>Metaprogramming is one of the most important facilities of Ur. This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.</p> 124 <p>Metaprogramming is one of the most important facilities of Ur. This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.</p>
119 <p>The unary <tt>$</tt> operator is used to build a record <tt>Type</tt> from a <tt>{Type}</tt> (that is, the kind of records of types). The library function <tt>mapU</tt> takes in a type <i>t</i> of kind <t>K</t> and a <tt>{Unit}</tt> <i>r</i>, and it builds a <tt>{K}</tt> as long as <i>r</i>, where every field is assigned value <i>t</i>.</p> 130 <p>The unary <tt>$</tt> operator is used to build a record <tt>Type</tt> from a <tt>{Type}</tt> (that is, the kind of records of types). The library function <tt>mapU</tt> takes in a type <i>t</i> of kind <t>K</t> and a <tt>{Unit}</tt> <i>r</i>, and it builds a <tt>{K}</tt> as long as <i>r</i>, where every field is assigned value <i>t</i>.</p>
120 131
121 <p>Another library function <tt>foldUR</tt> is defined at the level of expressions, while <tt>mapU</tt> is a type-level function. <tt>foldUR</tt> takes 7 arguments, some of them types and some values. Type arguments are distinguished by being written within brackets. The arguments to <tt>foldUR</tt> respectively tell us: 132 <p>Another library function <tt>foldUR</tt> is defined at the level of expressions, while <tt>mapU</tt> is a type-level function. <tt>foldUR</tt> takes 7 arguments, some of them types and some values. Type arguments are distinguished by being written within brackets. The arguments to <tt>foldUR</tt> respectively tell us:
122 133
123 <ol> 134 <ol>
124 <li> The type we will assign to each record field</li> 135 <li>The type we will assign to each record field</li>
125 <li> The type of the final and all intermediate results of the fold, expressed as a function over the portion of the <tt>{Unit}</tt> that has been traversed so far</li> 136 <li>The type of the final and all intermediate results of the fold, expressed as a function over the portion of the <tt>{Unit}</tt> that has been traversed so far</li>
126 <li> A function that updates the accumulator based on the current record field name, the rest of the input record type, the current record field value, and the current accumulator</li> 137 <li>A function that updates the accumulator based on the current record field name, the rest of the input record type, the current record field value, and the current accumulator</li>
127 <li> The initial accumulator value</li> 138 <li>The initial accumulator value</li>
128 <li> The input record type</li> 139 <li>The input record type</li>
129 <li> A folder for that type</li> 140 <li>A folder for that type</li>
130 <li> The input record value</li> 141 <li>The input record value</li>
131 </ol> 142 </ol>
132 143
133 An unusual part of the third argument is the syntax <tt>[t1 ~ t2]</tt> within a multi-argument <tt>fn</tt>. This syntax denotes a proof that row types <tt>t1</tt> and <tt>t2</tt> have no field names in common. The proof is not named, because it is applied automatically as needed. Indeed, the proof appears unused in this case, though it is actually needed to ensure the validity of some inferred types, as well as to unify with the type of <tt>foldUR</tt>.</p> 144 An unusual part of the third argument is the syntax <tt>[t1 ~ t2]</tt> within a multi-argument <tt>fn</tt>. This syntax denotes a proof that row types <tt>t1</tt> and <tt>t2</tt> have no field names in common. The proof is not named, because it is applied automatically as needed. Indeed, the proof appears unused in this case, though it is actually needed to ensure the validity of some inferred types, as well as to unify with the type of <tt>foldUR</tt>.</p>
134 145
135 <p>The general syntax for constant row types is <tt>[Name1 = t1, ..., NameN = tN]</tt>, and there is a shorthand version <tt>[Name1, ..., NameN]</tt> for records of <tt>Unit</tt>s.</p> 146 <p>The general syntax for constant row types is <tt>[Name1 = t1, ..., NameN = tN]</tt>, and there is a shorthand version <tt>[Name1, ..., NameN]</tt> for records of <tt>Unit</tt>s.</p>
156 <p>This example pulls together much of what we have seen so far. It involves a generic "admin interface" builder. That is, we have the <tt>Crud.Make</tt> functor, which takes in a description of a table and outputs a sub-application for viewing and editing that table.</p> 167 <p>This example pulls together much of what we have seen so far. It involves a generic "admin interface" builder. That is, we have the <tt>Crud.Make</tt> functor, which takes in a description of a table and outputs a sub-application for viewing and editing that table.</p>
157 168
158 <p>The signature of <tt>Crud.Make</tt> is based around a type function <tt>colMeta</tt>, which describes which supporting values we need for each column. This function is declared with the keyword <tt>con</tt>, which stands for "constructor," the general class of "compile-time things" that includes types. An argument to <tt>colMeta</tt> has kind <tt>(Type * Type)</tt>, which means that it must be a type-level tuple. The first type is how the column is represented in SQL, and the second is how we represent it in HTML forms. In order, the components of the resulting record give: 169 <p>The signature of <tt>Crud.Make</tt> is based around a type function <tt>colMeta</tt>, which describes which supporting values we need for each column. This function is declared with the keyword <tt>con</tt>, which stands for "constructor," the general class of "compile-time things" that includes types. An argument to <tt>colMeta</tt> has kind <tt>(Type * Type)</tt>, which means that it must be a type-level tuple. The first type is how the column is represented in SQL, and the second is how we represent it in HTML forms. In order, the components of the resulting record give:
159 170
160 <ol> 171 <ol>
161 <li> A display name</li> 172 <li>A display name</li>
162 <li> A way of pretty-printing values of the column</li> 173 <li>A way of pretty-printing values of the column</li>
163 <li> A way of generating an HTML form widget to input this column</li> 174 <li>A way of generating an HTML form widget to input this column</li>
164 <li> A way of generating an HTML form widget with an initial value specified</li> 175 <li>A way of generating an HTML form widget with an initial value specified</li>
165 <li> A way of parsing values of the column from strings</li> 176 <li>A way of parsing values of the column from strings</li>
166 <li> A type class witness, showing that the SQL representation can really be included in SQL</li> 177 <li>A type class witness, showing that the SQL representation can really be included in SQL</li>
167 </ol></p> 178 </ol></p>
168 179
169 <p>The function <tt>colsMeta</tt> lifts <tt>colMeta</tt> over type-level records of type pairs. The <tt>Crud</tt> module also defines reasonable default <tt>colMeta</tt> values for some primitive types.</p> 180 <p>The function <tt>colsMeta</tt> lifts <tt>colMeta</tt> over type-level records of type pairs. The <tt>Crud</tt> module also defines reasonable default <tt>colMeta</tt> values for some primitive types.</p>
170 181
171 <p>The functor signature tells us (in order) that an input must contain: 182 <p>The functor signature tells us (in order) that an input must contain:
172 183
173 <ol> 184 <ol>
174 <li> A type pair record <tt>cols</tt></li> 185 <li>A type pair record <tt>cols</tt></li>
175 <li> A proof that <tt>cols</tt> does not contain a field named <tt>Id</tt></li> 186 <li>A proof that <tt>cols</tt> does not contain a field named <tt>Id</tt></li>
176 <li> A SQL table <tt>tab</tt> with an <tt>Id</tt> field of type <tt>int</tt> and other fields whose names and types are read off of <tt>cols</tt></li> 187 <li>A SQL table <tt>tab</tt> with an <tt>Id</tt> field of type <tt>int</tt> and other fields whose names and types are read off of <tt>cols</tt></li>
177 <li> A display title for the admin interface</li> 188 <li>A display title for the admin interface</li>
178 <li> A record of meta-data for the columns</li> 189 <li>A record of meta-data for the columns</li>
179 </ol></p> 190 </ol></p>
180 191
181 <p>Looking at <tt>crud1.ur</tt>, we see that a use of the functor is almost trivial. Only the value components of the argument structure must be provided. The column row type is inferred, and the disjointness constraint is proved automatically.</p> 192 <p>Looking at <tt>crud1.ur</tt>, we see that a use of the functor is almost trivial. Only the value components of the argument structure must be provided. The column row type is inferred, and the disjointness constraint is proved automatically.</p>
182 193
183 <p>We won't go into detail on the implementation of <tt>Crud.Make</tt>. The types of the functions used there can be found in the signatures of the built-in <tt>Basis</tt> module and the <tt>Top</tt> module from the standard library. The signature of the first and the signature and implementation of the second can be found in the <tt>lib/ur</tt> directory of the Ur/Web distribution.</p> 194 <p>We won't go into detail on the implementation of <tt>Crud.Make</tt>. The types of the functions used there can be found in the signatures of the built-in <tt>Basis</tt> module and the <tt>Top</tt> module from the standard library. The signature of the first and the signature and implementation of the second can be found in the <tt>lib/ur</tt> directory of the Ur/Web distribution.</p>
224 235
225 <p>The signature of the functor is the same as for <tt>Crud</tt>. We change the definition of <tt>colMeta</tt> to reflect the different kinds of column metadata that we need. Each column is still described by a pair of types, and the first element of each pair still gives the SQL type for a column. Now, however, the second type in a pair gives a type of <i>local state</i> to be used in a reactive widget for inputing that column.</p> 236 <p>The signature of the functor is the same as for <tt>Crud</tt>. We change the definition of <tt>colMeta</tt> to reflect the different kinds of column metadata that we need. Each column is still described by a pair of types, and the first element of each pair still gives the SQL type for a column. Now, however, the second type in a pair gives a type of <i>local state</i> to be used in a reactive widget for inputing that column.</p>
226 237
227 <p>The first three fields of a <tt>colMeta</tt> record are the same as for <tt>Crud</tt>. The rest of the fields are:</p> 238 <p>The first three fields of a <tt>colMeta</tt> record are the same as for <tt>Crud</tt>. The rest of the fields are:</p>
228 <ol> 239 <ol>
229 <li> <tt>NewState</tt>, which allocates some new widget local state</li> 240 <li><tt>NewState</tt>, which allocates some new widget local state</li>
230 <li> <tt>Widget</tt>, which produces a reactive widget from some state</li> 241 <li><tt>Widget</tt>, which produces a reactive widget from some state</li>
231 <li> <tt>ReadState</tt>, which reads the current value of some state to determine which SQL value it encodes</li> 242 <li><tt>ReadState</tt>, which reads the current value of some state to determine which SQL value it encodes</li>
232 </ol> 243 </ol>
233 244
234 <p><tt>BatchFun.Make</tt> handles the plumbing of allocating the local state, using it to create widgets, and reading the state values when the user clicks "Batch it."</p> 245 <p><tt>BatchFun.Make</tt> handles the plumbing of allocating the local state, using it to create widgets, and reading the state values when the user clicks "Batch it."</p>
235 246
236 <p><tt>batchG.ur</tt> contains an example instantiation, which is just as easy to write as in the <tt>Crud1</tt> example.</p> 247 <p><tt>batchG.ur</tt> contains an example instantiation, which is just as easy to write as in the <tt>Crud1</tt> example.</p>