changeset 416:679b2fbbd4d0

Counter demo
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 11:59:48 -0400 (2008-10-23)
parents 777317e8b2ae
children e0e9e9eca1cb
files demo/counter.ur demo/counter.urp demo/counter.urs demo/prose
diffstat 4 files changed, 16 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/counter.ur	Thu Oct 23 11:59:48 2008 -0400
@@ -0,0 +1,7 @@
+fun counter n = return <xml><body>
+  Current counter: {[n]}<br/>
+  <a link={counter (n + 1)}>Increment</a><br/>
+  <a link={counter (n - 1)}>Decrement</a>
+</body></xml>
+
+fun main () = counter 0
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/counter.urp	Thu Oct 23 11:59:48 2008 -0400
@@ -0,0 +1,2 @@
+
+counter
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/counter.urs	Thu Oct 23 11:59:48 2008 -0400
@@ -0,0 +1,1 @@
+val main : unit -> transaction page
--- a/demo/prose	Thu Oct 23 11:38:31 2008 -0400
+++ b/demo/prose	Thu Oct 23 11:59:48 2008 -0400
@@ -44,12 +44,16 @@
 
 <p>Crafting webs of interlinked pages is easy, using recursion.</p>
 
+counter.urp
+
+<p>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.</p>
+
+<p>In the implementation of <tt>Counter.counter</tt>, we see the notation <tt>{[...]}</tt>, which uses type classes to inject values of different types (<tt>int</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>
+
 form.urp
 
 <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>
 
-<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>
-
 listShop.urp
 
 <p>This example shows off algebraic datatypes, parametric polymorphism, and functors.</p>