Mercurial > urweb
comparison demo/prose @ 410:c5a3d223f157
Sql demo
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 21 Oct 2008 18:44:52 -0400 |
| parents | 81d9f42bb641 |
| children | 6a0e54400805 |
comparison
equal
deleted
inserted
replaced
| 409:81d9f42bb641 | 410:c5a3d223f157 |
|---|---|
| 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> | 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> |
| 58 | 58 |
| 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> | 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> |
| 60 | 60 |
| 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> | 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> |
| 62 | |
| 63 sql.urp | |
| 64 | |
| 65 <p>We see a simple example of accessing a SQL database. The project file specifies the database to connect to.</p> | |
| 66 | |
| 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> | |
| 68 | |
| 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> | |
| 70 | |
| 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> | |
| 72 | |
| 73 <p> |