|
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@406
|
47 form.urp
|
|
adamc@406
|
48
|
|
adamc@406
|
49 <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
|
50
|
|
adamc@406
|
51 <p>In the implementation of <tt>handler</tt>, we see the notation <tt>{[...]}</tt>, which uses type classes to inject values of different types (<tt>string</tt> and <tt>bool</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@403
|
52
|
|
adamc@403
|
53 listShop.urp
|
|
adamc@403
|
54
|
|
adamc@408
|
55 <p>This example shows off algebraic datatypes, parametric polymorphism, and functors.</p>
|
|
adamc@408
|
56
|
|
adamc@408
|
57 <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
|
58
|
|
adamc@408
|
59 <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
|
60
|
|
adamc@408
|
61 <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
|
62
|
|
adamc@410
|
63 sql.urp
|
|
adamc@410
|
64
|
|
adamc@410
|
65 <p>We see a simple example of accessing a SQL database. The project file specifies the database to connect to.</p>
|
|
adamc@410
|
66
|
|
adamc@410
|
67 <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
|
68
|
|
adamc@410
|
69 <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
|
70
|
|
adamc@410
|
71 <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
|
72
|
|
adamc@410
|
73 <p>
|
|
adamc@413
|
74
|
|
adamc@413
|
75 sum.urp
|
|
adamc@413
|
76
|
|
adamc@413
|
77 <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
|
78
|
|
adamc@413
|
79 <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
|
80
|
|
adamc@413
|
81 <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
|
82
|
|
adamc@413
|
83 <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
|
84
|
|
adamc@413
|
85 <ol>
|
|
adamc@413
|
86 <li> The type we will assign to each record field</li>
|
|
adamc@413
|
87 <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
|
88 <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
|
89 <li> The initial accumulator value</li>
|
|
adamc@413
|
90 <li> The input record type</li>
|
|
adamc@413
|
91 <li> The input record value</li>
|
|
adamc@413
|
92 </ol>
|
|
adamc@413
|
93
|
|
adamc@413
|
94 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
|
95
|
|
adamc@413
|
96 <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
|
97
|
|
adamc@413
|
98 <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>
|
