adamc@643:

Ur/Web 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). Ur 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 Standard ML, with a few Haskell-isms added, and kinder, gentler versions added of many features from dependently-typed languages like the logic behind Coq. 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.

adamc@404: adamc@404:

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: adamc@404:

./configure
adamc@404: make
adamc@404: sudo make install
adamc@404: urweb -demo /Demo demo

adamc@404: adamc@404:

The -demo /Demo flag says that we want to build a demo application that expects its URIs to begin with /Demo. The final argument demo gives the path to a directory housing demo files. One of the files in that directory is prose, a file describing the different demo pieces with HTML. Some lines of prose have the form foo.urp, naming particular project files (with the extension .urp) in that directory.

adamc@404: adamc@404:

These project files can also be built separately. For example, you could run adamc@404: adamc@404:

urweb demo/hello

adamc@404: adamc@498: to build the "Hello World" demo application. Whether building the pieces separately or all at once with the -demo flag, a standalone web server executable is generated. The -demo command line will generate demo/demo.exe, and the other command line will generate demo/hello.exe. Either can be run with no arguments to start a single-threaded server accepting requests on port 8080. Pass the flag -h to see which options are available.

adamc@404: adamc@404:

The -demo version also generates some HTML in a subdirectory out 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 DIR is the location of an Ur/Web source distribution. adamc@404: adamc@404:

Alias /demo/ "DIR/demo/out/"
adamc@404: 
adamc@404: ProxyPass /Demo/ http://localhost:8080/
adamc@404: ProxyPassReverse /Demo/ http://localhost:8080/

adamc@404: adamc@409:

Building the demo also generates a demo.sql file, giving the SQL commands to run to define all of the tables and sequences that the applications expect to see. The file demo.urp contains a database line with the PostgreSQL database that the demo web server will try to connect to.

adamc@409: adamc@404:

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.

adamc@380: adamc@380: hello.urp adamc@380: adamc@405:

We must, of course, begin with "Hello World."

adamc@405: adamc@405:

The project file justs list one filename prefix, hello. This causes both hello.urs and hello.ur to be pulled into the project. .urs files are like OCaml .mli files, and .ur files are like OCaml .ml files. That is, .urs files provide interfaces, and .ur files provide implementations. .urs files may be omitted for .ur files, in which case most permissive interfaces are inferred.

adamc@405: adamc@503:

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. hello.urs tells us that we only export a function named main, taking no arguments and running a transaction that results in an HTML page. transaction is a monad in the spirit of the Haskell IO monad, with the intent that every operation performable in transaction 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.

adamc@405: adamc@405:

Looking at hello.ur, 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 /Demo/Hello/main. That is, we take the demo-wide prefix /Demo and add a suffix that indicates we want to call the main function in the Hello module. This path convention generalizes to arbitrary levels of nested module definitions and functor applications (which we will see later).

adamc@380: adamc@380: link.urp adamc@380: adamc@406:

In link.ur, 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.

adamc@406: adamc@407: rec.urp adamc@407: adamc@407:

Crafting webs of interlinked pages is easy, using recursion.

adamc@407: adamc@416: counter.urp adamc@416: adamc@416:

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.

adamc@416: adamc@416:

In the implementation of Counter.counter, we see the notation {[...]}, which uses type classes to inject values of different types (int in this case) into XML. It's probably worth stating explicitly that XML fragments are not strings, so that the type-checker will enforce that our final piece of XML is valid.

adamc@416: adamc@406: form.urp adamc@406: adamc@406:

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.

adamc@406: adamc@455: nested.urp adamc@455: adamc@455:

Here is an implementation of the tiny challenge problem from this web framework comparison. Using nested function definitions, it is easy to persist state across clicks.

adamc@455: adamc@465: cookie.urp adamc@465: adamc@465:

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.

adamc@465: adamc@465:

After setting the cookie, try browsing back to this demo from the main index. The data you entered should still be there.

adamc@465: adamc@403: listShop.urp adamc@403: adamc@408:

This example shows off algebraic datatypes, parametric polymorphism, and functors.

adamc@408: adamc@408:

The List module defines a list datatype, much in the style of SML, but with type parameters written more in Haskell style. The types of List.length and List.rev indicate that they are polymorphic. Types like t ::: Type -> ... indicate polymorphism, with the triple colon denoting that the value of this type parameter should be inferred 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 declared explicitly in Ur, while instantiations may be inferred at uses.

adamc@408: adamc@408:

The ListFun module defines a functor for building list editing sub-applications. An argument to the functor Make 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.

adamc@408: adamc@408:

The ListShop modules ties everything together by instantiating ListFun.Make with structures for integers and strings. show and read can be used for marshaling and unmarshaling in both cases because they are type-class-generic.

adamc@410: adamc@410: sql.urp adamc@410: adamc@410:

We see a simple example of accessing a SQL database. The project file specifies the database to connect to.

adamc@410: adamc@410:

A table 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).

adamc@410: adamc@410:

The list function implements an HTML table view of all rows in the SQL table. The queryX 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.

adamc@410: adamc@410:

Other functions demonstrate use of the dml 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.

adamc@410: adamc@410:

adamc@413: adamc@420: ref.urp adamc@420: adamc@420:

This example shows how to mix the module system with SQL to implement a kind of "abstract data type." The functor RefFun.Make 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 ref, along with operations for working with refs via transactions. In the functor implementation, we see that ref is implemented as int, treated as primary keys of a SQL table.

adamc@420: adamc@420:

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.

adamc@420: adamc@643:

Note that, in ref.ur, the inj components of functor arguments are omitted. Since these arguments are type class witnesses, the compiler infers them automatically based on the choices of data.

adamc@643: adamc@501: tree.urp adamc@501: adamc@501:

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.

adamc@501: adamc@643:

The signature of TreeFun.Make tells us that, to instantiate the functor, we must provide

adamc@643:

A primary key type key
SQL field names id (for primary keys) and parent (for parent links)
A type-level record cols of field names besides id and parent
"Proofs" that id is distinct from parent and that neither of id and parent appears in cols
Witnesses that both key and option key belong to the type class sql_injectable, which indicates that they are fair game to use with SQL
An SQL table tab, containing a field id of type key, a field parent of type option key, and every field of cols

adamc@643: adamc@413: sum.urp adamc@413: adamc@413:

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.

adamc@413: adamc@413:

Ur's support for analysis of types is based around extensible records, or row types. In the definition of the sum function, we see the type parameter fs assigned the kind {Unit}, which stands for records of types of kind Unit. The Unit kind has only one inhabitant, (). The kind Type is for "normal" types.

adamc@413: adamc@643:

The sum function also takes an argument fl of type folder fs. 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.

adamc@413: adamc@643:

The unary $ operator is used to build a record Type from a {Type} (that is, the kind of records of types). The library function mapU takes in a type t of kind K and a {Unit} r, and it builds a {K} as long as r, where every field is assigned value t.

adamc@643: adamc@643:

Another library function foldUR is defined at the level of expressions, while mapU is a type-level function. foldUR takes 7 arguments, some of them types and some values. Type arguments are distinguished by being written within brackets. The arguments to foldUR respectively tell us: adamc@413: adamc@413:

The type we will assign to each record field
The type of the final and all intermediate results of the fold, expressed as a function over the portion of the {Unit} that has been traversed so far
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
The initial accumulator value
The input record type
A folder for that type
The input record value

adamc@413: adamc@413: An unusual part of the third argument is the syntax [t1 ~ t2] within a multi-argument fn. This syntax denotes a proof that row types t1 and t2 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 foldUR.

adamc@413: adamc@413:

The general syntax for constant row types is [Name1 = t1, ..., NameN = tN], and there is a shorthand version [Name1, ..., NameN] for records of Units.

adamc@413: adamc@643:

With sum defined, it is easy to make some sample calls. The form of the code for main does not make it apparent, but the compiler must "reverse engineer" the appropriate {Unit} from the {Type} available from the context at each call to sum. The compiler also infers a folder for each call, guessing at the desired permutations by examining the orders in which field names are written in the code.

adamc@417: adamc@417: tcSum.urp adamc@417: adamc@417:

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.

adamc@418: adamc@418: metaform1.urp adamc@418: adamc@420:

We can use metaprogramming with row types to build HTML forms (and their handlers) generically. The functor Metaform.Make takes in a unit row fs and a value-level record names assigning string names to the fields of fs. The functor implementation builds a form handler with a library function foldURX2, which runs over two value-level records in parallel, building an XML fragment.

adamc@420: adamc@643:

The form itself is generated using the more primitive foldUR. We see the type xml form [] (mapU string cols) 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 mapU string cols. The useMore 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. adamc@643:

The functor use in Metaform1 is trivial. The compiler infers the values of the structure members fs and fl from the type of the value provided for names.

adamc@420: adamc@418: metaform2.urp adamc@419: adamc@420:

This example showcases code reuse by applying the same functor as in the last example. The Metaform2 module mixes pages from the functor with some new pages of its own.

adamc@421: adamc@421: crud1.urp adamc@421: adamc@421:

This example pulls together much of what we have seen so far. It involves a generic "admin interface" builder. That is, we have the Crud.Make functor, which takes in a description of a table and outputs a sub-application for viewing and editing that table.

adamc@421: adamc@421:

The signature of Crud.Make is based around a type function colMeta, which describes which supporting values we need for each column. This function is declared with the keyword con, which stands for "constructor," the general class of "compile-time things" that includes types. An argument to colMeta has kind (Type * Type), 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: adamc@421:

A display name
A way of pretty-printing values of the column
A way of generating an HTML form widget to input this column
A way of generating an HTML form widget with an initial value specified
A way of parsing values of the column from strings
A type class witness, showing that the SQL representation can really be included in SQL

adamc@421: adamc@421:

The function colsMeta lifts colMeta over type-level records of type pairs. The Crud module also defines reasonable default colMeta values for some primitive types.

adamc@421: adamc@421:

The functor signature tells us (in order) that an input must contain: adamc@421: adamc@421:

A type pair record cols
A proof that cols does not contain a field named Id
A SQL table tab with an Id field of type int and other fields whose names and types are read off of cols
A display title for the admin interface
A record of meta-data for the columns

adamc@421: adamc@421:

Looking at crud1.ur, 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.

adamc@421: adamc@643:

We won't go into detail on the implementation of Crud.Make. The types of the functions used there can be found in the signatures of the built-in Basis module and the Top module from the standard library. The signature of the first and the signature and implementation of the second can be found in the lib/ur directory of the Ur/Web distribution.

adamc@422: adamc@422: crud2.urp adamc@422: adamc@422:

This example shows another application of Crud.Make. We mix one standard column with one customized column. We write an underscore for the Inject field of meta-data, since the type class facility can infer that witness.

adamc@644: adamc@644: alert.urp adamc@644: adamc@644:

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.

adamc@644: adamc@644:

Here's an example of a button that, when clicked, opens an alert dialog on the client.

adamc@645: adamc@645: react.urp adamc@645: adamc@645:

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.

adamc@645: adamc@645:

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 dyn, whose signal attribute specifies one of these pure functions over mutable sources. A source containing data of type t has type source t and is created with the source operation within the transaction monad. Functions over sources are represented in the monad signal. Like in Haskell, we overload monad notations, so that the same return and bind operators can be used to write signals and transactions. The signal function coerces a source to a signal.