From 29bfb2f27733a76306314dd4d85d3623d2a56bef Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 21 Oct 2008 17:44:03 -0400 Subject: ListShop prose --- demo/prose | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'demo') diff --git a/demo/prose b/demo/prose index a22e1968..8f55f8dc 100644 --- a/demo/prose +++ b/demo/prose @@ -50,4 +50,10 @@ form.urp listShop.urp -

This is my other favorite.

+

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

+ +

The List module defines a list datatype, much in the style of SML, but with type parameters written more in Haskell style. The types of List.length and List.rev indicate that they are polymorphic. Types like t ::: Type -> ... indicate polymorphism, with the triple colon denoting that the value of this type parameter should be inferred 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 declared explicitly in Ur, while instantiations may be inferred at uses.

+ +

The ListFun module defines a functor for building list editing sub-applications. An argument to the functor Make 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.

+ +

The ListShop modules ties everything together by instantiating ListFun.Make with structures for integers and strings. show and read can be used for marshaling and unmarshaling in both cases because they are type-class-generic.

-- cgit v1.2.3