From db7cd221444afce64803e66594d56dc8e7a0843c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 10 Mar 2009 10:44:26 -0400 Subject: Avoid any JavaScript when pages don't need it; update demo prose --- demo/prose | 29 ++++++++++++++++++++++------- 1 file changed, 22 insertions(+), 7 deletions(-) (limited to 'demo/prose') diff --git a/demo/prose b/demo/prose index 29c12c38..e7de3471 100644 --- a/demo/prose +++ b/demo/prose @@ -1,4 +1,4 @@ -

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 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.

+

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.

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: @@ -92,19 +92,33 @@ ref.urp

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.

+

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.

+ tree.urp

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.

+

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

+
    +
  1. A primary key type key
    2. +
  2. SQL field names id (for primary keys) and parent (for parent links)
    3. +
  3. A type-level record cols of field names besides id and parent
    4. +
  4. "Proofs" that id is distinct from parent and that neither of id and parent appears in cols
    5. +
  5. 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
    6. +
  6. An SQL table tab, containing a field id of type key, a field parent of type option key, and every field of cols
    7. +
+ sum.urp

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.

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.

-

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

+

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.

+ +

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.

-

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

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:

  1. The type we will assign to each record field
    2. @@ -112,6 +126,7 @@ sum.urp
  2. 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
  3. The initial accumulator value
  4. The input record type
    5. +
  5. A folder for that type
  6. The input record value
@@ -119,7 +134,7 @@ An unusual part of the third argument is the syntax [t1 ~ t2] within a

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

-

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.

+

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.

tcSum.urp @@ -129,8 +144,8 @@ metaform1.urp

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.

-

The form itself is generated using the more primitive foldUR. We see the type xml form [] (mapUT 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 mapUT 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. -

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

+

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. +

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.

metaform2.urp @@ -165,7 +180,7 @@ crud1.urp

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.

-

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 directory of the Ur/Web distribution.

+

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.

crud2.urp -- cgit v1.2.3