From 833f4d2e0474ec3ff772107b52711289c4b648cf Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Oct 2008 11:59:48 -0400 Subject: Counter demo --- demo/prose | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'demo/prose') diff --git a/demo/prose b/demo/prose index 7f9f6bb0..8fedc557 100644 --- a/demo/prose +++ b/demo/prose @@ -44,12 +44,16 @@ rec.urp

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.

-- cgit v1.2.3