Mercurial > urweb

comparison demo/prose @ 643:aa2290c32ce2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Avoid any JavaScript when pages don't need it; update demo prose
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Mar 2009 10:44:26 -0400
parents d2dfdf90b9b6
children 8e17e6b615bd
comparison
equal deleted inserted replaced
642:4a125bbc602d 643:aa2290c32ce2
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 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> 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>
2 2
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: 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:
4 4
5 <blockquote><pre>./configure 5 <blockquote><pre>./configure
6 make 6 make
90 90
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> 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>
92 92
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> 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>
94 94
95 <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>
96
95 tree.urp 97 tree.urp
96 98
97 <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> 99 <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>
100
101 <p>The signature of <tt>TreeFun.Make</tt> tells us that, to instantiate the functor, we must provide</p>
102 <ol>
103 <li> A primary key type <tt>key</tt></li>
104 <li> SQL field names <tt>id</tt> (for primary keys) and <tt>parent</tt> (for parent links)</li>
105 <li> A type-level record <tt>cols</tt> of field names besides <tt>id</tt> and <tt>parent</tt></li>
106 <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>
107 <li> Witnesses that both <tt>key</tt> and <tt>option key</tt> belong to the type class <tt>sql_injectable</tt>, which indicates that they are fair game to use with SQL</li>
108 <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>
109 </ol>
98 110
99 sum.urp 111 sum.urp
100 112
101 <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> 113 <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>
102 114
103 <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> 115 <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>
104 116
105 <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> 117 <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>
106 118
107 <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: 119 <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>
120
121 <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:
108 122
109 <ol> 123 <ol>
110 <li> The type we will assign to each record field</li> 124 <li> The type we will assign to each record field</li>
111 <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> 125 <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>
112 <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> 126 <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>
113 <li> The initial accumulator value</li> 127 <li> The initial accumulator value</li>
114 <li> The input record type</li> 128 <li> The input record type</li>
129 <li> A folder for that type</li>
115 <li> The input record value</li> 130 <li> The input record value</li>
116 </ol> 131 </ol>
117 132
118 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> 133 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>
119 134
120 <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> 135 <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>
121 136
122 <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> 137 <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>
123 138
124 tcSum.urp 139 tcSum.urp
125 140
126 <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> 141 <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>
127 142
128 metaform1.urp 143 metaform1.urp
129 144
130 <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> 145 <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>
131 146
132 <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> 147 <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>
133 <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> 148 <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>
134 149
135 metaform2.urp 150 metaform2.urp
136 151
137 <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> 152 <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>
138 153
163 <li> A record of meta-data for the columns</li> 178 <li> A record of meta-data for the columns</li>
164 </ol></p> 179 </ol></p>
165 180
166 <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> 181 <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>
167 182
168 <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> 183 <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>
169 184
170 crud2.urp 185 crud2.urp
171 186
172 <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> 187 <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>