# HG changeset patch # User Adam Chlipala # Date 1224777588 14400 # Node ID 679b2fbbd4d04961eb7e29066f17c65d0acf745e # Parent 777317e8b2aeef945c9ea4061c44c2c31a8e5c99 Counter demo diff -r 777317e8b2ae -r 679b2fbbd4d0 demo/counter.ur --- /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 + Current counter: {[n]}
+ Increment
+ Decrement + + +fun main () = counter 0 diff -r 777317e8b2ae -r 679b2fbbd4d0 demo/counter.urp --- /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 diff -r 777317e8b2ae -r 679b2fbbd4d0 demo/counter.urs --- /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 diff -r 777317e8b2ae -r 679b2fbbd4d0 demo/prose --- 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 @@

Crafting webs of interlinked pages is easy, using recursion.

+counter.urp + +

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.

+ +

In the implementation of Counter.counter, we see the notation {[...]}, which uses type classes to inject values of different types (int in this case) into XML. It's probably worth stating explicitly that XML fragments are not strings, so that the type-checker will enforce that our final piece of XML is valid.

+ form.urp

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.

-

In the implementation of handler, we see the notation {[...]}, which uses type classes to inject values of different types (string and bool in this case) into XML. It's probably worth stating explicitly that XML fragments are not strings, so that the type-checker will enforce that our final piece of XML is valid.

- listShop.urp

This example shows off algebraic datatypes, parametric polymorphism, and functors.