annotate demo/prose @ 829:20fe00fd81da

Substring functions; fix a nasty MonoReduce pattern match substitution bug
author Adam Chlipala <adamc@hcoop.net>
date Sat, 30 May 2009 13:29:00 -0400
parents c884a42599f3
children 305bc0a431de
rev   line source
adamc@643 1 <p><b>Ur/Web</b> is a domain-specific language for programming web applications backed by SQL databases. It is (strongly) statically-typed (like ML and Haskell) and purely functional (like Haskell). <b>Ur</b> is the base language, and the web-specific features of Ur/Web (mostly) come only in the form of special rules for parsing and optimization. The Ur core looks a lot like <a href="http://sml.sourceforge.net/">Standard ML</a>, with a few <a href="http://www.haskell.org/">Haskell</a>-isms added, and kinder, gentler versions added of many features from dependently-typed languages like the logic behind <a href="http://coq.inria.fr/">Coq</a>. The type system is much more expressive than in ML and Haskell, such that well-typed web applications cannot "go wrong," not just in handling single HTTP requests, but across their entire lifetimes of interacting with HTTP clients. Beyond that, Ur is unusual in using ideas from dependent typing to enable very effective metaprogramming, or programming with explicit analysis of type structure. Many common web application components can be built by Ur/Web functions that operate on types, where it seems impossible to achieve similar code re-use in more established statically-typed languages.</p>
adamc@404 2
adamc@404 3 <p>This demo is built automatically from Ur/Web sources and supporting files. If you unpack the Ur/Web source distribution, then the following steps will build you a local version of this demo:
adamc@404 4
adamc@404 5 <blockquote><pre>./configure
adamc@404 6 make
adamc@404 7 sudo make install
adamc@404 8 urweb -demo /Demo demo</pre></blockquote></p>
adamc@404 9
adamc@404 10 <p>The <tt>-demo /Demo</tt> flag says that we want to build a demo application that expects its URIs to begin with <tt>/Demo</tt>. The final argument <tt>demo</tt> gives the path to a directory housing demo files. One of the files in that directory is <tt>prose</tt>, a file describing the different demo pieces with HTML. Some lines of <tt>prose</tt> have the form <tt><i>foo</i>.urp</tt>, naming particular project files (with the extension <tt>.urp</tt>) in that directory.</p>
adamc@404 11
adamc@404 12 <p>These project files can also be built separately. For example, you could run
adamc@404 13
adamc@404 14 <blockquote><pre>urweb demo/hello</pre></blockquote>
adamc@404 15
adamc@498 16 to build the "Hello World" demo application. Whether building the pieces separately or all at once with the <tt>-demo</tt> flag, a standalone web server executable is generated. The <tt>-demo</tt> command line will generate <tt>demo/demo.exe</tt>, and the other command line will generate <tt>demo/hello.exe</tt>. Either can be run with no arguments to start a single-threaded server accepting requests on port 8080. Pass the flag <tt>-h</tt> to see which options are available.</p>
adamc@404 17
adamc@404 18 <p>The <tt>-demo</tt> version also generates some HTML in a subdirectory <tt>out</tt> of the demo directory. It is easy to set Apache up to serve these HTML files, and to proxy out to the Ur/Web web server for dynamic page requests. This configuration works for me, where <tt>DIR</tt> is the location of an Ur/Web source distribution.
adamc@404 19
adamc@404 20 <blockquote><pre>Alias /demo/ "DIR/demo/out/"
adamc@404 21
adamc@404 22 ProxyPass /Demo/ http://localhost:8080/
adamc@404 23 ProxyPassReverse /Demo/ http://localhost:8080/</pre></blockquote></p>
adamc@404 24
adamc@409 25 <p>Building the demo also generates a <tt>demo.sql</tt> file, giving the SQL commands to run to define all of the tables and sequences that the applications expect to see. The file <tt>demo.urp</tt> contains a <tt>database</tt> line with the PostgreSQL database that the demo web server will try to connect to.</p>
adamc@409 26
adamc@404 27 <p>The rest of the demo focuses on the individual applications. Follow the links in the lefthand frame to visit the applications, commentary, and syntax-highlighted source code. (An Emacs mode is behind the syntax highlighting.) I recommend visiting the applications in the order listed, since that is the order in which new concepts are introduced.</p>
adamc@380 28
adamc@380 29 hello.urp
adamc@380 30
adamc@405 31 <p>We must, of course, begin with "Hello World."</p>
adamc@405 32
adamc@405 33 <p>The project file justs list one filename prefix, <tt>hello</tt>. This causes both <tt>hello.urs</tt> and <tt>hello.ur</tt> to be pulled into the project. <tt>.urs</tt> files are like <a href="http://caml.inria.fr/ocaml/">OCaml</a> <tt>.mli</tt> files, and <tt>.ur</tt> files are like OCaml <tt>.ml</tt> files. That is, <tt>.urs</tt> files provide interfaces, and <tt>.ur</tt> files provide implementations. <tt>.urs</tt> files may be omitted for <tt>.ur</tt> files, in which case most permissive interfaces are inferred.</p>
adamc@405 34
adamc@503 35 <p>Ur/Web features a module system very similar to those found in SML and OCaml. Like in OCaml, interface files are treated as module system signatures, and they are ascribed to structures built from implementation files. <tt>hello.urs</tt> tells us that we only export a function named <tt>main</tt>, taking no arguments and running a transaction that results in an HTML page. <tt>transaction</tt> is a monad in the spirit of the Haskell IO monad, with the intent that every operation performable in <tt>transaction</tt> can be undone. By design, Ur/Web does not provide a less constrained way of running side-effecting actions. This particular example application will employ no side effects, but the compiler requires that all pages be generated by transactions.</p>
adamc@405 36
adamc@405 37 <p>Looking at <tt>hello.ur</tt>, we see an SML-looking function definition that returns a fragment of XML, written with special syntax. This fragment is returned to browsers that request the URI <tt>/Demo/Hello/main</tt>. That is, we take the demo-wide prefix <tt>/Demo</tt> and add a suffix that indicates we want to call the <tt>main</tt> function in the <tt>Hello</tt> module. This path convention generalizes to arbitrary levels of nested module definitions and functor applications (which we will see later).</p>
adamc@380 38
adamc@380 39 link.urp
adamc@380 40
adamc@406 41 <p>In <tt>link.ur</tt>, we see how easy it is to link to another page. The Ur/Web compiler guarantees that all links are valid. We just write some Ur/Web code inside an "antiquote" in our XML, denoting a transaction that will produce the new page if the link is clicked.</p>
adamc@406 42
adamc@407 43 rec.urp
adamc@407 44
adamc@407 45 <p>Crafting webs of interlinked pages is easy, using recursion.</p>
adamc@407 46
adamc@416 47 counter.urp
adamc@416 48
adamc@416 49 <p>It is also easy to pass state around via functions, in the style commonly associated with "continuation-based" web servers. As is usual for such systems, all state is stored on the client side. In this case, it is encoded in URLs.</p>
adamc@416 50
adamc@416 51 <p>In the implementation of <tt>Counter.counter</tt>, we see the notation <tt>{[...]}</tt>, which uses type classes to inject values of different types (<tt>int</tt> in this case) into XML. It's probably worth stating explicitly that XML fragments <i>are not strings</i>, so that the type-checker will enforce that our final piece of XML is valid.</p>
adamc@416 52
adamc@406 53 form.urp
adamc@406 54
adamc@406 55 <p>Here we see a basic form. The type system tracks which form inputs we include, and it enforces that the form handler function expects a record containing exactly those fields, with exactly the proper types.</p>
adamc@406 56
adamc@455 57 nested.urp
adamc@455 58
adamc@455 59 <p>Here is an implementation of the tiny challenge problem from <a href="http://www.accursoft.co.uk/web/">this web framework comparison</a>. Using nested function definitions, it is easy to persist state across clicks.</p>
adamc@455 60
adamc@465 61 cookie.urp
adamc@465 62
adamc@465 63 <p>Often, it is useful to associate persistent data with particular web clients. Ur/Web includes an easy facility for using type-safe cookies. This example shows how to use a form to set a named cookie.</p>
adamc@465 64
adamc@465 65 <p>After setting the cookie, try browsing back to this demo from the main index. The data you entered should still be there.</p>
adamc@465 66
adamc@774 67 url.urp
adamc@774 68
adamc@774 69 <p>Up to this point, we haven't included a single URL in our source code. This may be very surprising to programmers used to working with traditional web frameworks! In Ur/Web, we avoid writing URLs explicitly wherever possible. To link to an external web page, we rely on an abstract type <tt>url</tt>. Strings can't be treated implicitly as URLs; rather, they must be "blessed" explicitly. This helps avoid some classes of code injection attacks.</p>
adamc@774 70
adamc@774 71 <p>Further, each Ur/Web application enforces a global condition on which strings are allowed as URLs. The <tt>.urp</tt> file for this demo shows an example that specifies particular rules about which URLs are allowed. You can try entering a variety of URLs on the form on the front page. Only those satisfying the <tt>allow url</tt>/<tt>deny url</tt> conditions should be permitted.</p>
adamc@774 72
adamc@775 73 css.urp
adamc@775 74
adamc@775 75 <p>Ur/Web supports a structured approach to Cascading Style Sheets, where each style is a first-class value within a module. This demo shows the importing of an external style sheet with one style. By default, like other Ur/Web entities, the name of the style would be <tt>Css_quote</tt>. We use the <tt>rewrite</tt> directive in the <tt>.urp</tt> file to specify an alternate name for a particular canonical module path. The external style sheet contains a definition of a style with the alternate name that we give.</p>
adamc@775 76
adamc@776 77 upload.urp
adamc@776 78
adamc@776 79 <p>HTTP file upload is made convenient, via the abstract types <tt>blob</tt> and <tt>file</tt> in the standard library. A <tt>blob</tt> is a binary sequence, and a <tt>file</tt> combines a <tt>blob</tt> with MIME type information. An <tt>upload</tt> form input can be used to accept <tt>file</tt>s from the user.</p>
adamc@776 80
adamc@776 81 <p>In the <tt>.urp</tt> file for this example, we give a whitelist of MIME types to be accepted. The application will echo back to the user any file he uploads as one of those types. You can try submitting other kinds of files to verify that they are rejected.</p>
adamc@776 82
adamc@780 83 subforms.urp
adamc@780 84
adamc@780 85 <p>In the examples so far, the number of inputs per form has been constant. Often it is useful to have a varying set of form inputs. Ur/Web provides the <tt>&lt;subforms&gt;</tt> and <tt>&lt;entry&gt;</tt> tags for grouping a list of forms with the same field names and types into a single, list-valued composite form. This demo shows those tags in action, in a simple form echoing application that lets the user add and remove inputs.</p>
adamc@780 86
adamc@403 87 listShop.urp
adamc@403 88
adamc@408 89 <p>This example shows off algebraic datatypes, parametric polymorphism, and functors.</p>
adamc@408 90
adamc@408 91 <p>The <tt>List</tt> module defines a list datatype, much in the style of SML, but with type parameters written more in Haskell style. The types of <tt>List.length</tt> and <tt>List.rev</tt> indicate that they are polymorphic. Types like <tt>t ::: Type -> ...</tt> indicate polymorphism, with the triple colon denoting that the value of this type parameter should be <i>inferred</i> at uses. A double colon would mean that the type argument must be provided explicitly at uses. In contrast to ML and Haskell, all polymorphism must be <i>declared</i> explicitly in Ur, while instantiations may be inferred at uses.</p>
adamc@408 92
adamc@408 93 <p>The <tt>ListFun</tt> module defines a functor for building list editing sub-applications. An argument to the functor <tt>Make</tt> must give the type to be stored in the lists, along with marshaling and unmarshaling functions. In return, the functor returns an entry point function.</p>
adamc@408 94
adamc@408 95 <p>The <tt>ListShop</tt> modules ties everything together by instantiating <tt>ListFun.Make</tt> with structures for integers and strings. <tt>show</tt> and <tt>read</tt> can be used for marshaling and unmarshaling in both cases because they are type-class-generic.</p>
adamc@410 96
adamc@410 97 sql.urp
adamc@410 98
adamc@410 99 <p>We see a simple example of accessing a SQL database. The project file specifies the database to connect to.</p>
adamc@410 100
adamc@410 101 <p>A <tt>table</tt> declaration declares a SQL table with rows of a particular record type. We can use embedded SQL syntax in a way that leads to all of our queries and updates being type-checked. Indeed, Ur/Web makes strong guarantees that it is impossible to execute invalid SQL queries or make bad assumptions about the types of tables for marshaling and unmarshaling (which happen implicitly).</p>
adamc@410 102
adamc@410 103 <p>The <tt>list</tt> function implements an HTML table view of all rows in the SQL table. The <tt>queryX</tt> function takes two arguments: a SQL query and a function for generating XML fragments from query result rows. The query is run, and the fragments for the rows are concatenated together.</p>
adamc@410 104
adamc@410 105 <p>Other functions demonstrate use of the <tt>dml</tt> function, for building a transaction from a SQL DML command. It is easy to insert antiquoted Ur code into queries and DML commands, and the type-checker catches mistakes in the types of the expressions that we insert.</p>
adamc@410 106
adamc@410 107 <p>
adamc@413 108
adamc@420 109 ref.urp
adamc@420 110
adamc@420 111 <p>This example shows how to mix the module system with SQL to implement a kind of "abstract data type." The functor <tt>RefFun.Make</tt> takes in a type belonging to the type class of those types that may be included in SQL. The functor output includes an abstract type <tt>ref</tt>, along with operations for working with <tt>ref</tt>s via transactions. In the functor implementation, we see that <tt>ref</tt> is implemented as <tt>int</tt>, treated as primary keys of a SQL table.</p>
adamc@420 112
adamc@420 113 <p>The functor creates a new encapsulated SQL sequence and table on each call. These local relations show up in the automatically-generated SQL file that should be run to prepare the database for use, but they are invisible from client code. We could change the functor to create different SQL relations, without needing to change client code.</p>
adamc@420 114
adamc@643 115 <p>Note that, in <tt>ref.ur</tt>, the <tt>inj</tt> components of functor arguments are omitted. Since these arguments are type class witnesses, the compiler infers them automatically based on the choices of <tt>data</tt>.</p>
adamc@643 116
adamc@501 117 tree.urp
adamc@501 118
adamc@501 119 <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>
adamc@501 120
adamc@643 121 <p>The signature of <tt>TreeFun.Make</tt> tells us that, to instantiate the functor, we must provide</p>
adamc@643 122 <ol>
adamc@773 123 <li>A primary key type <tt>key</tt></li>
adamc@773 124 <li>SQL field names <tt>id</tt> (for primary keys) and <tt>parent</tt> (for parent links)</li>
adamc@773 125 <li>A type-level record <tt>cols</tt> of field names besides <tt>id</tt> and <tt>parent</tt></li>
adamc@773 126 <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>
adamc@773 127 <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>
adamc@773 128 <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>
adamc@773 129 </ol>
adamc@773 130
adamc@773 131 constraints.urp
adamc@773 132
adamc@773 133 <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>
adamc@773 134
adamc@773 135 <ol>
adamc@773 136 <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>
adamc@773 137 <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>
adamc@773 138 <li>The <tt>CHECK</tt> constraint declares a boolean assertion that must hold for every row of the table.</li>
adamc@773 139 <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>
adamc@643 140 </ol>
adamc@643 141
adamc@777 142 outer.urp
adamc@777 143
adamc@777 144 <p>SQL outer joins are no problem, as this demo shows. Unlike with SQL, here we have static type inference determining for us which columns may become nullable as a result of an outer join, and the compiler will reject programs that make the wrong assumptions about that process. The details of that nullification don't appear in this example, where the magic of type classes determines both the post-join type of each field and the right pretty-printing and parsing function for each of those types.</p>
adamc@777 145
adamc@778 146 view.urp
adamc@778 147
adamc@778 148 <p>SQL views are also supported with a special declaration form, analogous to <tt>table</tt>. A multi-parameter type class <tt>fieldsOf</tt> is used to characterize places where both tables and views are allowed. For instance, the polymorphic function <tt>list</tt> shown here lists the contents of any table or view containing just a single <tt>int</tt> column named <tt>A</tt>.</p>
adamc@778 149
adamc@779 150 cookieSec.urp
adamc@779 151
adamc@779 152 <p>Ur/Web guarantees that compiled applications are immune to certain kinds of <a href="http://www.owasp.org/index.php/Top_10_2007-A5">cross site request forgery</a>. For instance, a "phisher" might send many e-mails linking to a form that he has set up to look like your web site. The form is connected to your web site, where it might, say, transfer money from your bank account to the phisher's account. The phisher doesn't know your username, but, if that username is stored in a cookie, it will be sent automatically by your browser. Ur/Web automatically signs cookie values cryptographically, with the signature included as a POST parameter and not part of a cookie, to prevent such attacks.</p>
adamc@779 153
adamc@779 154 <p>This demo shows a simple mock-up of a situation where such an attack is often possible with traditional web frameworks. You can set an arbitrary username for yourself in a cookie, and you can modify the database in a way that depends on the current cookie value. Try getting the latter action to succeed without first setting your desired username in the cookie. This should be roughly as impossible as cracking the particular cryptographic hash function that is used.</p>
adamc@779 155
adamc@413 156 sum.urp
adamc@413 157
adamc@413 158 <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>
adamc@413 159
adamc@413 160 <p>Ur's support for analysis of types is based around extensible records, or <i>row types</i>. In the definition of the <tt>sum</tt> function, we see the type parameter <tt>fs</tt> assigned the <i>kind</i> <tt>{Unit}</tt>, which stands for records of types of kind <tt>Unit</tt>. The <tt>Unit</tt> kind has only one inhabitant, <tt>()</tt>. The kind <tt>Type</tt> is for "normal" types.</p>
adamc@413 161
adamc@643 162 <p>The <tt>sum</tt> function also takes an argument <tt>fl</tt> of type <tt>folder fs</tt>. Folders represent permutations of the elements of type-level records. We can use a folder to iterate over a type-level record in the order indicated by the permutation.</p>
adamc@413 163
adamc@643 164 <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>
adamc@643 165
adamc@643 166 <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:
adamc@413 167
adamc@413 168 <ol>
adamc@773 169 <li>The type we will assign to each record field</li>
adamc@773 170 <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>
adamc@773 171 <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>
adamc@773 172 <li>The initial accumulator value</li>
adamc@773 173 <li>The input record type</li>
adamc@773 174 <li>A folder for that type</li>
adamc@773 175 <li>The input record value</li>
adamc@413 176 </ol>
adamc@413 177
adamc@413 178 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>
adamc@413 179
adamc@413 180 <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>
adamc@413 181
adamc@643 182 <p>With <tt>sum</tt> defined, it is easy to make some sample calls. The form of the code for <tt>main</tt> does not make it apparent, but the compiler must "reverse engineer" the appropriate <tt>{Unit}</tt> from the <tt>{Type}</tt> available from the context at each call to <tt>sum</tt>. The compiler also infers a <tt>folder</tt> for each call, guessing at the desired permutations by examining the orders in which field names are written in the code.</p>
adamc@417 183
adamc@417 184 tcSum.urp
adamc@417 185
adamc@417 186 <p>It's easy to adapt the last example to use type classes, such that we can sum the fields of records based on any numeric type.</p>
adamc@418 187
adamc@418 188 metaform1.urp
adamc@418 189
adamc@420 190 <p>We can use metaprogramming with row types to build HTML forms (and their handlers) generically. The functor <tt>Metaform.Make</tt> takes in a unit row <tt>fs</tt> and a value-level record <tt>names</tt> assigning string names to the fields of <tt>fs</tt>. The functor implementation builds a form handler with a library function <tt>foldURX2</tt>, which runs over two value-level records in parallel, building an XML fragment.</p>
adamc@420 191
adamc@643 192 <p>The form itself is generated using the more primitive <tt>foldUR</tt>. We see the type <tt>xml form [] (mapU string cols)</tt> as the result of the fold. This is the type of XML fragments that are suitable for inclusion in forms, require no form fields to be defined on entry, and themselves define form fields whose names and types are given by <tt>mapU string cols</tt>. The <tt>useMore</tt> function "weakens" the type of an XML fragment, so that it "pretends" to require additional fields as input. This weakening is necessary to accommodate the general typing rule for concatenating bits of XML.</tt>
adamc@643 193 <p>The functor use in <tt>Metaform1</tt> is trivial. The compiler infers the values of the structure members <tt>fs</tt> and <tt>fl</tt> from the type of the value provided for <tt>names</tt>.</p>
adamc@420 194
adamc@418 195 metaform2.urp
adamc@419 196
adamc@420 197 <p>This example showcases code reuse by applying the same functor as in the last example. The <tt>Metaform2</tt> module mixes pages from the functor with some new pages of its own.</p>
adamc@421 198
adamc@421 199 crud1.urp
adamc@421 200
adamc@421 201 <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>
adamc@421 202
adamc@421 203 <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:
adamc@421 204
adamc@421 205 <ol>
adamc@773 206 <li>A display name</li>
adamc@773 207 <li>A way of pretty-printing values of the column</li>
adamc@773 208 <li>A way of generating an HTML form widget to input this column</li>
adamc@773 209 <li>A way of generating an HTML form widget with an initial value specified</li>
adamc@773 210 <li>A way of parsing values of the column from strings</li>
adamc@773 211 <li>A type class witness, showing that the SQL representation can really be included in SQL</li>
adamc@421 212 </ol></p>
adamc@421 213
adamc@421 214 <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>
adamc@421 215
adamc@421 216 <p>The functor signature tells us (in order) that an input must contain:
adamc@421 217
adamc@421 218 <ol>
adamc@773 219 <li>A type pair record <tt>cols</tt></li>
adamc@773 220 <li>A proof that <tt>cols</tt> does not contain a field named <tt>Id</tt></li>
adamc@773 221 <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>
adamc@773 222 <li>A display title for the admin interface</li>
adamc@773 223 <li>A record of meta-data for the columns</li>
adamc@421 224 </ol></p>
adamc@421 225
adamc@421 226 <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>
adamc@421 227
adamc@643 228 <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>
adamc@422 229
adamc@422 230 crud2.urp
adamc@422 231
adamc@422 232 <p>This example shows another application of <tt>Crud.Make</tt>. We mix one standard column with one customized column. We write an underscore for the <tt>Inject</tt> field of meta-data, since the type class facility can infer that witness.</p>
adamc@644 233
adamc@781 234 crud3.urp
adamc@781 235
adamc@781 236 <p>One thing that is unclear from the previous examples is how to provide more complex, multi-input widgets for taking input meant for particular fields. The signature of <tt>Crud.Make</tt> forces every widget to define exactly one input. The <tt>&lt;subform&gt;</tt> tag, the simpler cousin of the <tt>&lt;subforms&gt;</tt> tag that we saw earlier, provides a fix for this problem. Via <tt>&lt;subform&gt;</tt>, an arbitrary form can be turned into a single record-valued input.</p>
adamc@781 237
adamc@781 238 <p>We use that possibility here to define a silly widget for a <tt>string</tt> column, which concatenates the values entered into two different textboxes.</p>
adamc@781 239
adamc@644 240 alert.urp
adamc@644 241
adamc@644 242 <p>Ur/Web makes it easy to write code whose execution should be distributed between the web server and client web browsers. Server-side code is compiled to efficient native code, and client-side code is compiled to JavaScript. Ur/Web programmers don't need to worry about these details, because the language and standard library provide a uniform ML-like interface for the whole process.</p>
adamc@644 243
adamc@644 244 <p>Here's an example of a button that, when clicked, opens an alert dialog on the client.</p>
adamc@645 245
adamc@645 246 react.urp
adamc@645 247
adamc@645 248 <p>Most client-side JavaScript programs modify page contents imperatively, but Ur/Web is based on functional-reactive programming instead. Programs allocate data sources and then describe the page as a pure function of those data sources. When the sources change, the page changes automatically.</p>
adamc@645 249
adamc@645 250 <p>Here's an example where a button modifies a data source that affects some text on the page. The affected portion of the page is indicated with the pseudo-HTML tag <tt>dyn</tt>, whose <tt>signal</tt> attribute specifies one of these pure functions over mutable sources. A source containing data of type <tt>t</tt> has type <tt>source t</tt> and is created with the <tt>source</tt> operation within the <tt>transaction</tt> monad. Functions over sources are represented in the monad <tt>signal</tt>. Like in Haskell, we overload monad notations, so that the same return and bind operators can be used to write signals and transactions. The <tt>signal</tt> function coerces a source to a signal.</p>
adamc@647 251
adamc@647 252 listEdit.urp
adamc@647 253
adamc@647 254 <p>This is a more involved functional-reactive example, involving recursive data structures that contain sources. We build a list editor similar to the one from the <tt>ListShop</tt> example, but with all editing happening on the client side.</p>
adamc@647 255
adamc@647 256 <p>The central data structure is the <tt>rlist</tt>, a list whose individual elements are sources, enabling fine-grained mutation. Every rlist is either nil or is a cons cell made up of a source for a string data element, another source to serve as a scratchpad for GUI-based edits to the data element, and a final source that stores the remainder of the list.</p>
adamc@647 257
adamc@647 258 <p>The main program provides operations to append to a list and to edit the data stored at any cell of the list. Append is implemented by maintaining a source <tt>head</tt>, which points to the first list element; and a source <tt>tailP</tt>, which points to a <tt>source rlist</tt> where we should place the next appended node.</p>
adamc@648 259
adamc@648 260 increment.urp
adamc@648 261
adamc@648 262 <p>Here's an example where client-side code needs to run more code on the server. We maintain a (server-side) SQL sequence. When the user clicks a button, an AJAX request increments the remote sequence and gets the new value.</p>
adamc@649 263
adamc@651 264 noisy.urp
adamc@651 265
adamc@651 266 <p>This example shows how easy it is to make the flow of control "ping pong" back and forth between the client and the server. Clicking a button triggers three queries to the server, with an alert generated after each query.</p>
adamc@651 267
adamc@649 268 batch.urp
adamc@649 269
adamc@649 270 <p>This example shows more of what is possible with mixed client/server code. The application is an editor for a simple database table, where additions of new rows can be batched in the client, before a button is clicked to trigger a mass addition.</p>
adamc@650 271
adamc@650 272 batchG.urp
adamc@650 273
adamc@650 274 <p>We can redo the last example with a generic component, like we did in the <tt>Crud</tt> examples. The module <tt>BatchFun</tt> is analogous to the <tt>Crud</tt> module. It contains a functor that builds a batching editor, when given a suitable description of a table.</p>
adamc@650 275
adamc@650 276 <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>
adamc@650 277
adamc@650 278 <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>
adamc@650 279 <ol>
adamc@773 280 <li><tt>NewState</tt>, which allocates some new widget local state</li>
adamc@773 281 <li><tt>Widget</tt>, which produces a reactive widget from some state</li>
adamc@773 282 <li><tt>ReadState</tt>, which reads the current value of some state to determine which SQL value it encodes</li>
adamc@650 283 </ol>
adamc@650 284
adamc@650 285 <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>
adamc@650 286
adamc@650 287 <p><tt>batchG.ur</tt> contains an example instantiation, which is just as easy to write as in the <tt>Crud1</tt> example.</p>
adamc@697 288
adamc@697 289 threads.urp
adamc@697 290
adamc@697 291 <p>Ur/Web makes it easy to write multi-threaded client-side code. This example demonstrates two threads writing to a page at once.</p>
adamc@697 292
adamc@697 293 <p>First, we define a useful component for sections of pages that can have lines of text added to them dynamically. This is the <tt>Buffer</tt> module. It contains an abstract type of writable regions, along with functions to create a region, retrieve a signal representing its HTML rendering, and add a new line to it.</p>
adamc@697 294
adamc@697 295 <p>The entry point to the main module <tt>Threads</tt> begins by creating a buffer. The function <tt>loop</tt> implements writing to that buffer periodically, incrementing a counter each time. The arguments to <tt>loop</tt> specify a prefix for the messages and the number of milliseconds to wait between writes.</p>
adamc@697 296
adamc@697 297 <p>We specify some client-side code to run on page load using the <tt>onload</tt> attribute of <tt>&lt;body&gt;</tt>. The <tt>onload</tt> code in this example spawns two separate threads running the <tt>loop</tt> code with different prefixes, update intervals, and starting counters.</p>
adamc@697 298
adamc@697 299 <p>Old hands at concurrent programming may be worried at the lack of synchronization in this program. Ur/Web uses <i>cooperative multi-threading</i>, not the more common <i>preemptive</i> multi-threading. Only one thread runs at a time, and only particular function calls can trigger context switches. In this example, <tt>sleep</tt> is the only such function that appears.</p>
adamc@698 300
adamc@698 301 roundTrip.urp
adamc@698 302
adamc@698 303 <p>So far, we've seen examples of client-side code triggering the execution of server-side code. Such remote calls only happen in response to client-side events. It is often useful to allow a client to trigger events on other clients, and Ur/Web facilitates this with a simple asynchronous message-passing facility. The current example introduces the basics of message-passing with a trivial use case, and the next example shows a more realistic case where several clients can communicate.</p>
adamc@698 304
adamc@698 305 <p>We are going to provide a silly service where a client can send messages to the server, which the server then echoes back to the client. The SQL table <tt>channels</tt> stores a mapping from client IDs to message channels. The abstract type <tt>client</tt> holds unique client IDs, which Ur/Web generates automatically as needed. A <tt>channel <i>T</i></tt> is a channel to which messages of type <tt><i>T</i></tt> can be sent. Every channel belongs to a single client; anyone can send to a channel, but only the channel's owner can read the messages. Every client is associated with a particular open page on a particular web browser somewhere. Since web browsing sessions are ephemeral, clients and their channels are garbage-collected automatically as the web server loses contact with browsers. When a client is garbage-collected, any database row mentioning it or one of its channels is deleted. It's also possible to include <tt>option client</tt>s (and likewise for channels) in databases, in which case such columns are merely nulled out when they refer to dead clients.</p>
adamc@698 306
adamc@698 307 <p>The <tt>main</tt> function begins by retrieving the current client ID, allocating a new channel, and associating that channel with the current client in the database. Next, we allocate a buffer and return the page, which in its <tt>onload</tt> attribute starts two loops running in parallel. In contrast to in the last example, here we only use <tt>spawn</tt> with the call to the first loop, since every client-side event handler is implicitly started in a new thread.</tt>
adamc@698 308
adamc@698 309 <p>The first loop, <tt>receiver</tt>, repeatedly reads messages from the channel and writes them to the buffer. The second loop, <tt>sender</tt>, periodically sends messages to the channel. Client code can't send messages directly. Instead, we must use server-side functions to do the sending. Clients aren't trusted to pass channels to the server, so our server-side function <tt>writeBack</tt> instead keys off of the client ID, looking up the corresponding channel in the database.</p>
adamc@699 310
adamc@699 311 chat.urp
adamc@699 312
adamc@699 313 <p>This example provides a simple anonymous online chatting system, with multiple named channels.</p>
adamc@699 314
adamc@699 315 <p>First, we build another useful component. Recall that each channel has an owning client, who has the exclusive ability to read messages sent to it. On top of that functionality, we can build a kind of broadcast channel that accepts multiple subscribers. The <tt>Broadcast</tt> module contains a functor with such an implementation. We instantiate the functor with the type of data we want to send over the channel. The functor output gives us an abstract type of "topics," which are subscribable IDs. When a client subscribes to a topic, it is handed a channel that it can use to read new messages on that topic. We also have an operation to count the number of subscribers to a topic. This number shouldn't be treated as too precise, since some clients that have surfed away from the application may still be considered subscribed until a timeout period elapses.</p>
adamc@699 316
adamc@699 317 <p>The main <tt>Chat</tt> application includes some standard management of a table of named channels. All of the interesting client-server work is done with the <tt>recv</tt> function and with the functions provided by <tt>Broadcast</tt>.</p>