summaryrefslogtreecommitdiff
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 11:59:48 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 11:59:48 -0400
commit833f4d2e0474ec3ff772107b52711289c4b648cf (patch)
tree9623809c43673edac7f48bb26d0be992f2c4377d /demo
parente0f9a9d921e6e505c86ef3e798690784f7abd511 (diff)
Counter demo
Diffstat (limited to 'demo')
-rw-r--r--demo/counter.ur7
-rw-r--r--demo/counter.urp2
-rw-r--r--demo/counter.urs1
-rw-r--r--demo/prose8
4 files changed, 16 insertions, 2 deletions
diff --git a/demo/counter.ur b/demo/counter.ur
new file mode 100644
index 00000000..b11fc936
--- /dev/null
+++ b/demo/counter.ur
@@ -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
diff --git a/demo/counter.urp b/demo/counter.urp
new file mode 100644
index 00000000..d22312c9
--- /dev/null
+++ b/demo/counter.urp
@@ -0,0 +1,2 @@
+
+counter
diff --git a/demo/counter.urs b/demo/counter.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/counter.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/prose b/demo/prose
index 7f9f6bb0..8fedc557 100644
--- a/demo/prose
+++ b/demo/prose
@@ -44,12 +44,16 @@ rec.urp
<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>