annotate demo/prose @ 469:b393c2fc80f8

About to begin optimization of recursive transaction functions
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 17:09:53 -0500
parents ddd363e856ff
children 20fab0e96217
rev   line source
adamc@404 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, type inference, 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 is 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 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@404 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 a single argument, an integer specifying how many request handler pthreads to spawn. The server accepts requests on port 8080.</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@405 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 interface 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@403 67 listShop.urp
adamc@403 68
adamc@408 69 <p>This example shows off algebraic datatypes, parametric polymorphism, and functors.</p>
adamc@408 70
adamc@408 71 <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 72
adamc@408 73 <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 74
adamc@408 75 <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 76
adamc@410 77 sql.urp
adamc@410 78
adamc@410 79 <p>We see a simple example of accessing a SQL database. The project file specifies the database to connect to.</p>
adamc@410 80
adamc@410 81 <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 82
adamc@410 83 <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 84
adamc@410 85 <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 86
adamc@410 87 <p>
adamc@413 88
adamc@420 89 ref.urp
adamc@420 90
adamc@420 91 <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 92
adamc@420 93 <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 94
adamc@413 95 sum.urp
adamc@413 96
adamc@413 97 <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 98
adamc@413 99 <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 100
adamc@413 101 <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>mapUT</tt> takes in a <tt>Type</tt> <i>t</i> and a <tt>{Unit}</tt> <i>r</i>, and it builds a <tt>{Type}</tt> as long as <i>r</i>, where every field is assigned value <i>t</i>.</p>
adamc@413 102
adamc@413 103 <p>Another library function <tt>foldUR</tt> is defined at the level of expressions, while <tt>mapUT</tt> is a type-level function. <tt>foldUR</tt> takes 6 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 104
adamc@413 105 <ol>
adamc@413 106 <li> The type we will assign to each record field</li>
adamc@413 107 <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@413 108 <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@413 109 <li> The initial accumulator value</li>
adamc@413 110 <li> The input record type</li>
adamc@413 111 <li> The input record value</li>
adamc@413 112 </ol>
adamc@413 113
adamc@413 114 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 115
adamc@413 116 <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 117
adamc@413 118 <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>.</p>
adamc@417 119
adamc@417 120 tcSum.urp
adamc@417 121
adamc@417 122 <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 123
adamc@418 124 metaform1.urp
adamc@418 125
adamc@420 126 <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 127
adamc@420 128 <p>The form itself is generated using the more primitive <tt>foldUR</tt>. We see the type <tt>xml form [] (mapUT 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>mapUT 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@420 129 <p>The functor use in <tt>Metaform1</tt> is trivial. The compiler infers the value of the structure member <tt>fs</tt> from the type of the value provided for <tt>names</tt>.</p>
adamc@420 130
adamc@418 131 metaform2.urp
adamc@419 132
adamc@420 133 <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 134
adamc@421 135 crud1.urp
adamc@421 136
adamc@421 137 <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 138
adamc@421 139 <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 140
adamc@421 141 <ol>
adamc@421 142 <li> A display name</li>
adamc@421 143 <li> A way of pretty-printing values of the column</li>
adamc@421 144 <li> A way of generating an HTML form widget to input this column</li>
adamc@421 145 <li> A way of generating an HTML form widget with an initial value specified</li>
adamc@421 146 <li> A way of parsing values of the column from strings</li>
adamc@421 147 <li> A type class witness, showing that the SQL representation can really be included in SQL</li>
adamc@421 148 </ol></p>
adamc@421 149
adamc@421 150 <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 151
adamc@421 152 <p>The functor signature tells us (in order) that an input must contain:
adamc@421 153
adamc@421 154 <ol>
adamc@421 155 <li> A type pair record <tt>cols</tt></li>
adamc@421 156 <li> A proof that <tt>cols</tt> does not contain a field named <tt>Id</tt></li>
adamc@421 157 <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@421 158 <li> A display title for the admin interface</li>
adamc@421 159 <li> A record of meta-data for the columns</li>
adamc@421 160 </ol></p>
adamc@421 161
adamc@421 162 <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 163
adamc@421 164 <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</tt> directory of the Ur/Web distribution.</p>
adamc@422 165
adamc@422 166 crud2.urp
adamc@422 167
adamc@422 168 <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>