annotate doc/intro.ur @ 1510:4aa3b6d962c8

Copy some project front-page text to the tutorial intro
author Adam Chlipala <adam@chlipala.net>
date Sun, 17 Jul 2011 14:37:45 -0400
parents d236dbf1b3e3
children e717e2b56b21
rev   line source
adam@1500 1 (* Chapter 1: Introduction *)
adam@1494 2
adam@1497 3 (* begin hide *)
adam@1497 4 val show_string = mkShow (fn s => "\"" ^ s ^ "\"")
adam@1497 5 (* end *)
adam@1495 6
adam@1497 7 (* This tutorial by <a href="http://adam.chlipala.net/">Adam Chlipala</a> is licensed under a <a href="http://creativecommons.org/licenses/by-nc-nd/3.0/">Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License</a>. *)
adam@1493 8
adam@1510 9 (* This is a tutorial for the <a href="http://www.impredicative.com/ur/">Ur/Web</a> programming language. The <a href="http://www.impredicative.com/ur/">official project web site</a> is your starting point for information, like a reference manual and a pointer to download the latest code release. In this tutorial, we'll just focus on introducing the language features.<br>
adam@1510 10 <br>
adam@1510 11 Briefly, <b>Ur</b> is a programming language in the tradition of <a target="_top" href="http://en.wikipedia.org/wiki/ML_(programming_language)">ML</a> and <a target="_top" href="http://en.wikipedia.org/wiki/Haskell_(programming_language)">Haskell</a>, but featuring a significantly richer type system. Ur is <a target="_top" href="http://en.wikipedia.org/wiki/Functional_programming">functional</a>, <a target="_top" href="http://en.wikipedia.org/wiki/Purely_functional">pure</a>, <a target="_top" href="http://en.wikipedia.org/wiki/Statically-typed">statically-typed</a>, and <a target="_top" href="http://en.wikipedia.org/wiki/Strict_programming_language">strict</a>. Ur supports a powerful kind of <b>metaprogramming</b> based on <b>row types</b>.<br>
adam@1510 12 <br>
adam@1510 13 <b>Ur/Web</b> is Ur plus a special standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases, with mixed server-side and client-side applications generated from source code in one language.<br>
adam@1510 14 <br>
adam@1510 15 Ur inherits its foundation from ML and Haskell, then going further to add fancier stuff. This first chapter of the tutorial reviews the key ML and Haskell features, giving their syntax in Ur. I do assume reading familiarity with ML and Haskell and won't dwell too much on explaining the imported features. *)
adam@1497 16
adam@1497 17 (* * Basics *)
adam@1497 18
adam@1501 19 (* Let's start with features shared with both ML and Haskell. First, we have the basic numeric, string, and Boolean stuff. (In the following examples, <tt>==</tt> is used to indicate the result of evaluating an expression. It's not valid Ur syntax!) *)
adam@1493 20
adam@1493 21 (* begin eval *)
adam@1497 22 1 + 1
adam@1493 23 (* end *)
adam@1493 24
adam@1497 25 (* begin eval *)
adam@1497 26 1.2 + 3.4
adam@1497 27 (* end *)
adam@1496 28
adam@1497 29 (* begin eval *)
adam@1497 30 "Hello " ^ "world!"
adam@1497 31 (* end *)
adam@1497 32
adam@1497 33 (* begin eval *)
adam@1497 34 1 + 1 < 6
adam@1497 35 (* end *)
adam@1497 36
adam@1497 37 (* begin eval *)
adam@1497 38 0.0 < -3.2
adam@1497 39 (* end *)
adam@1497 40
adam@1497 41 (* begin eval *)
adam@1497 42 "Hello" = "Goodbye" || (1 * 2 <> 8 && True <> False)
adam@1497 43 (* end *)
adam@1497 44
adam@1497 45 (* We also have function definitions with type inference for parameter and return types. *)
adam@1497 46
adam@1497 47 fun double n = 2 * n
adam@1497 48
adam@1497 49 (* begin eval *)
adam@1497 50 double 8
adam@1497 51 (* end *)
adam@1497 52
adam@1497 53 fun fact n = if n = 0 then 1 else n * fact (n - 1)
adam@1497 54
adam@1497 55 (* begin eval *)
adam@1497 56 fact 5
adam@1497 57 (* end *)
adam@1497 58
adam@1502 59 fun isEven n = n = 0 || isOdd (n - 1)
adam@1502 60 and isOdd n = n = 1 || isEven (n - 1)
adam@1502 61
adam@1502 62 (* begin eval *)
adam@1502 63 isEven 32
adam@1502 64 (* end *)
adam@1502 65
adam@1502 66
adam@1497 67 (* Of course we have anonymous functions, too. *)
adam@1497 68
adam@1497 69 val inc = fn x => x + 1
adam@1497 70
adam@1497 71 (* begin eval *)
adam@1497 72 inc 3
adam@1497 73 (* end *)
adam@1497 74
adam@1497 75 (* Then there's parametric polymorphism. Unlike in ML and Haskell, polymorphic functions in Ur/Web often require full type annotations. That is because more advanced features (which we'll get to in the next chapter) make Ur type inference undecidable. *)
adam@1497 76
adam@1497 77 fun id [a] (x : a) : a = x
adam@1497 78
adam@1497 79 (* begin eval *)
adam@1497 80 id "hi"
adam@1497 81 (* end *)
adam@1497 82
adam@1497 83 fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x)
adam@1497 84
adam@1497 85 (* begin eval *)
adam@1497 86 compose inc inc 3
adam@1497 87 (* end *)
adam@1498 88
adam@1502 89 (* The <tt>option</tt> type family is like ML's <tt>option</tt> or Haskell's <tt>Maybe</tt>. We also have a <tt>case</tt> expression form lifted directly from ML. Note that, while Ur follows most syntactic conventions of ML, one key difference is that type family names appear before their arguments, as in Haskell. *)
adam@1498 90
adam@1498 91 fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
adam@1498 92
adam@1498 93 (* begin hide *)
adam@1498 94 fun show_option [t] (_ : show t) : show (option t) =
adam@1498 95 mkShow (fn x => case x of
adam@1498 96 None => "None"
adam@1498 97 | Some x => "Some(" ^ show x ^ ")")
adam@1498 98 (* end *)
adam@1498 99
adam@1498 100 (* begin eval *)
adam@1498 101 predecessor 6
adam@1498 102 (* end *)
adam@1498 103
adam@1498 104 (* begin eval *)
adam@1498 105 predecessor 0
adam@1498 106 (* end *)
adam@1499 107
adam@1499 108 (* Naturally, there are lists, too! *)
adam@1499 109
adam@1499 110 val numbers : list int = 1 :: 2 :: 3 :: []
adam@1499 111 val strings : list string = "a" :: "bc" :: []
adam@1499 112
adam@1499 113 fun length [a] (ls : list a) : int =
adam@1499 114 case ls of
adam@1499 115 [] => 0
adam@1499 116 | _ :: ls' => 1 + length ls'
adam@1499 117
adam@1499 118 (* begin eval *)
adam@1499 119 length numbers
adam@1499 120 (* end *)
adam@1499 121
adam@1499 122 (* begin eval *)
adam@1499 123 length strings
adam@1499 124 (* end *)
adam@1500 125
adam@1502 126 (* And lists make a good setting for demonstrating higher-order functions and local functions. (This example also introduces one idiosyncrasy of Ur, which is that <tt>map</tt> is a keyword, so we name our "map" function <tt>mp</tt>.) *)
adam@1500 127
adam@1500 128 (* begin hide *)
adam@1500 129 fun show_list [t] (_ : show t) : show (list t) =
adam@1500 130 mkShow (let
adam@1500 131 fun shower (ls : list t) =
adam@1500 132 case ls of
adam@1500 133 [] => "[]"
adam@1500 134 | x :: ls' => show x ^ " :: " ^ shower ls'
adam@1500 135 in
adam@1500 136 shower
adam@1500 137 end)
adam@1500 138 (* end *)
adam@1500 139
adam@1500 140 fun mp [a] [b] (f : a -> b) : list a -> list b =
adam@1500 141 let
adam@1500 142 fun loop (ls : list a) =
adam@1500 143 case ls of
adam@1500 144 [] => []
adam@1500 145 | x :: ls' => f x :: loop ls'
adam@1500 146 in
adam@1500 147 loop
adam@1500 148 end
adam@1500 149
adam@1500 150 (* begin eval *)
adam@1500 151 mp inc numbers
adam@1500 152 (* end *)
adam@1500 153
adam@1500 154 (* begin eval *)
adam@1500 155 mp (fn s => s ^ "!") strings
adam@1500 156 (* end *)
adam@1500 157
adam@1500 158 (* We can define our own polymorphic datatypes and write higher-order functions over them. *)
adam@1500 159
adam@1500 160 datatype tree a = Leaf of a | Node of tree a * tree a
adam@1500 161
adam@1500 162 (* begin hide *)
adam@1500 163 fun show_tree [t] (_ : show t) : show (tree t) =
adam@1500 164 mkShow (let
adam@1500 165 fun shower (t : tree t) =
adam@1500 166 case t of
adam@1500 167 Leaf x => "Leaf(" ^ show x ^ ")"
adam@1500 168 | Node (t1, t2) => "Node(" ^ shower t1 ^ ", " ^ shower t2 ^ ")"
adam@1500 169 in
adam@1500 170 shower
adam@1500 171 end)
adam@1500 172 (* end *)
adam@1500 173
adam@1500 174 fun size [a] (t : tree a) : int =
adam@1500 175 case t of
adam@1500 176 Leaf _ => 1
adam@1500 177 | Node (t1, t2) => size t1 + size t2
adam@1500 178
adam@1500 179 (* begin eval *)
adam@1500 180 size (Node (Leaf 0, Leaf 1))
adam@1500 181 (* end *)
adam@1500 182
adam@1500 183 (* begin eval *)
adam@1500 184 size (Node (Leaf 1.2, Node (Leaf 3.4, Leaf 4.5)))
adam@1500 185 (* end *)
adam@1500 186
adam@1500 187 fun tmap [a] [b] (f : a -> b) : tree a -> tree b =
adam@1500 188 let
adam@1500 189 fun loop (t : tree a) : tree b =
adam@1500 190 case t of
adam@1500 191 Leaf x => Leaf (f x)
adam@1500 192 | Node (t1, t2) => Node (loop t1, loop t2)
adam@1500 193 in
adam@1500 194 loop
adam@1500 195 end
adam@1500 196
adam@1500 197 (* begin eval *)
adam@1500 198 tmap inc (Node (Leaf 0, Leaf 1))
adam@1500 199 (* end *)
adam@1500 200
adam@1501 201 (* We also have anonymous record types, as in Standard ML. The next chapter will show that there is quite a lot more going on here with records than in SML or OCaml, but we'll stick to the basics in this chapter. We will add one tantalizing hint of what's to come by demonstrating the record concatention operator <tt>++</tt> and the record field removal operator <tt>--</tt>. *)
adam@1500 202
adam@1500 203 val x = { A = 0, B = 1.2, C = "hi", D = True }
adam@1500 204
adam@1500 205 (* begin eval *)
adam@1500 206 x.A
adam@1500 207 (* end *)
adam@1500 208
adam@1500 209 (* begin eval *)
adam@1500 210 x.C
adam@1500 211 (* end *)
adam@1500 212
adam@1500 213 type myRecord = { A : int, B : float, C : string, D : bool }
adam@1500 214
adam@1500 215 fun getA (r : myRecord) = r.A
adam@1500 216
adam@1500 217 (* begin eval *)
adam@1500 218 getA x
adam@1500 219 (* end *)
adam@1500 220
adam@1500 221 (* begin eval *)
adam@1500 222 getA (x -- #A ++ {A = 4})
adam@1500 223 (* end *)
adam@1500 224
adam@1500 225 val y = { A = "uhoh", B = 2.3, C = "bye", D = False }
adam@1500 226
adam@1500 227 (* begin eval *)
adam@1500 228 getA (y -- #A ++ {A = 5})
adam@1500 229 (* end *)
adam@1501 230
adam@1501 231
adam@1501 232 (* * Borrowed from ML *)
adam@1501 233
adam@1502 234 (* Ur includes an ML-style <b>module system</b>. The most basic use case involves packaging abstract types with their "methods." *)
adam@1501 235
adam@1501 236 signature COUNTER = sig
adam@1501 237 type t
adam@1501 238 val zero : t
adam@1501 239 val increment : t -> t
adam@1501 240 val toInt : t -> int
adam@1501 241 end
adam@1501 242
adam@1501 243 structure Counter : COUNTER = struct
adam@1501 244 type t = int
adam@1502 245 val zero = 0
adam@1501 246 val increment = plus 1
adam@1501 247 fun toInt x = x
adam@1501 248 end
adam@1501 249
adam@1501 250 (* begin eval *)
adam@1501 251 Counter.toInt (Counter.increment Counter.zero)
adam@1501 252 (* end *)
adam@1501 253
adam@1502 254 (* We may package not just abstract types, but also abstract type families. Here we see our first use of the <tt>con</tt> keyword, which stands for <b>constructor</b>. Constructors are a generalization of types to include other "compile-time things"; for instance, basic type families, which are assigned the <b>kind</b> <tt>Type -> Type</tt>. Kinds are to constructors as types are to normal values. We also see how to write the type of a polymorphic function, using the <tt>:::</tt> syntax for type variable binding. This <tt>:::</tt> differs from the <tt>::</tt> used with the <tt>con</tt> keyword because it marks a type parameter as implicit, so that it need not be supplied explicitly at call sites. Such an option is the only one available in ML and Haskell, but, in the next chapter, we'll meet cases where it is appropriate to use explicit constructor parameters. *)
adam@1501 255
adam@1501 256 signature STACK = sig
adam@1501 257 con t :: Type -> Type
adam@1501 258 val empty : a ::: Type -> t a
adam@1501 259 val push : a ::: Type -> t a -> a -> t a
adam@1501 260 val pop : a ::: Type -> t a -> option a
adam@1501 261 end
adam@1501 262
adam@1501 263 structure Stack : STACK = struct
adam@1501 264 con t = list
adam@1501 265 val empty [a] = []
adam@1501 266 fun push [a] (t : t a) (x : a) = x :: t
adam@1501 267 fun pop [a] (t : t a) = case t of
adam@1501 268 [] => None
adam@1501 269 | x :: _ => Some x
adam@1501 270 end
adam@1501 271
adam@1501 272 (* begin eval *)
adam@1501 273 Stack.pop (Stack.push (Stack.push Stack.empty "A") "B")
adam@1501 274 (* end *)
adam@1501 275
adam@1501 276 (* Ur also inherits the ML concept of <b>functors</b>, which are functions from modules to modules. *)
adam@1501 277
adam@1501 278 datatype order = Less | Equal | Greater
adam@1501 279
adam@1501 280 signature COMPARABLE = sig
adam@1501 281 type t
adam@1501 282 val compare : t -> t -> order
adam@1501 283 end
adam@1501 284
adam@1501 285 signature DICTIONARY = sig
adam@1501 286 type key
adam@1501 287 con t :: Type -> Type
adam@1501 288 val empty : a ::: Type -> t a
adam@1501 289 val insert : a ::: Type -> t a -> key -> a -> t a
adam@1501 290 val lookup : a ::: Type -> t a -> key -> option a
adam@1501 291 end
adam@1501 292
adam@1501 293 functor BinarySearchTree(M : COMPARABLE) : DICTIONARY where type key = M.t = struct
adam@1501 294 type key = M.t
adam@1501 295 datatype t a = Leaf | Node of t a * key * a * t a
adam@1501 296
adam@1501 297 val empty [a] = Leaf
adam@1501 298
adam@1501 299 fun insert [a] (t : t a) (k : key) (v : a) : t a =
adam@1501 300 case t of
adam@1501 301 Leaf => Node (Leaf, k, v, Leaf)
adam@1501 302 | Node (left, k', v', right) =>
adam@1502 303 case M.compare k k' of
adam@1501 304 Equal => Node (left, k, v, right)
adam@1501 305 | Less => Node (insert left k v, k', v', right)
adam@1501 306 | Greater => Node (left, k', v', insert right k v)
adam@1501 307
adam@1501 308 fun lookup [a] (t : t a) (k : key) : option a =
adam@1501 309 case t of
adam@1501 310 Leaf => None
adam@1501 311 | Node (left, k', v, right) =>
adam@1502 312 case M.compare k k' of
adam@1501 313 Equal => Some v
adam@1501 314 | Less => lookup left k
adam@1501 315 | Greater => lookup right k
adam@1501 316 end
adam@1501 317
adam@1501 318 structure IntTree = BinarySearchTree(struct
adam@1501 319 type t = int
adam@1501 320 fun compare n1 n2 =
adam@1501 321 if n1 = n2 then
adam@1501 322 Equal
adam@1501 323 else if n1 < n2 then
adam@1501 324 Less
adam@1501 325 else
adam@1501 326 Greater
adam@1501 327 end)
adam@1501 328
adam@1501 329 (* begin eval *)
adam@1501 330 IntTree.lookup (IntTree.insert (IntTree.insert IntTree.empty 0 "A") 1 "B") 1
adam@1501 331 (* end *)
adam@1501 332
adam@1501 333 (* It is sometimes handy to rebind modules to shorter names. *)
adam@1501 334
adam@1501 335 structure IT = IntTree
adam@1501 336
adam@1501 337 (* begin eval *)
adam@1501 338 IT.lookup (IT.insert (IT.insert IT.empty 0 "A") 1 "B") 0
adam@1501 339 (* end *)
adam@1501 340
adam@1501 341 (* One can even use the <tt>open</tt> command to import a module's namespace wholesale, though this can make it harder for someone reading code to tell which identifiers come from which modules. *)
adam@1501 342
adam@1501 343 open IT
adam@1501 344
adam@1501 345 (* begin eval *)
adam@1501 346 lookup (insert (insert empty 0 "A") 1 "B") 2
adam@1501 347 (* end *)
adam@1502 348
adam@1502 349 (* Ur adopts OCaml's approach to splitting projects across source files. When a project contains files <tt>foo.ur</tt> and <tt>foo.urs</tt>, these are taken as defining a module named <tt>Foo</tt> whose signature is drawn from <tt>foo.urs</tt> and whose implementation is drawn from <tt>foo.ur</tt>. If <tt>foo.ur</tt> exists without <tt>foo.urs</tt>, then module <tt>Foo</tt> is defined without an explicit signature, so that it is assigned its <b>principal signature</b>, which exposes all typing details without abstraction. *)
adam@1502 350
adam@1502 351
adam@1502 352 (* * Borrowed from Haskell *)
adam@1502 353
adam@1502 354 (* Ur includes a take on <b>type classes</b>. For instance, here is a generic "max" function that relies on a type class <tt>ord</tt>. Notice that the type class membership witness is treated like an ordinary function parameter, though we don't assign it a name here, because type inference figures out where it should be used. The more advanced examples of the next chapter will include cases where we manipulate type class witnesses explicitly. *)
adam@1502 355
adam@1502 356 fun max [a] (_ : ord a) (x : a) (y : a) : a =
adam@1502 357 if x < y then
adam@1502 358 y
adam@1502 359 else
adam@1502 360 x
adam@1502 361
adam@1502 362 (* begin eval *)
adam@1502 363 max 1 2
adam@1502 364 (* end *)
adam@1502 365
adam@1502 366 (* begin eval *)
adam@1502 367 max "ABC" "ABA"
adam@1502 368 (* end *)
adam@1502 369
adam@1502 370 (* The idiomatic way to define a new type class is to stash it inside a module, like in this example: *)
adam@1502 371
adam@1502 372 signature DOUBLE = sig
adam@1502 373 class double
adam@1502 374 val double : a ::: Type -> double a -> a -> a
adam@1502 375 val mkDouble : a ::: Type -> (a -> a) -> double a
adam@1502 376
adam@1502 377 val double_int : double int
adam@1502 378 val double_string : double string
adam@1502 379 end
adam@1502 380
adam@1502 381 structure Double : DOUBLE = struct
adam@1502 382 class double a = a -> a
adam@1502 383
adam@1502 384 fun double [a] (f : double a) (x : a) : a = f x
adam@1502 385 fun mkDouble [a] (f : a -> a) : double a = f
adam@1502 386
adam@1502 387 val double_int = mkDouble (times 2)
adam@1502 388 val double_string = mkDouble (fn s => s ^ s)
adam@1502 389 end
adam@1502 390
adam@1502 391 open Double
adam@1502 392
adam@1502 393 (* begin eval *)
adam@1502 394 double 13
adam@1502 395 (* end *)
adam@1502 396
adam@1502 397 (* begin eval *)
adam@1502 398 double "ho"
adam@1502 399 (* end *)
adam@1502 400
adam@1502 401 val double_float = mkDouble (times 2.0)
adam@1502 402
adam@1502 403 (* begin eval *)
adam@1502 404 double 2.3
adam@1502 405 (* end *)
adam@1502 406
adam@1502 407 (* That example had a mix of instances defined with a class and instances defined outside its module. Its possible to create <b>closed type classes</b> simply by omitting from the module an instance creation function like <tt>mkDouble</tt>. This way, only the instances you decide on may be allowed, which enables you to enforce program-wide invariants over instances. *)
adam@1502 408
adam@1502 409 signature OK_TYPE = sig
adam@1502 410 class ok
adam@1502 411 val importantOperation : a ::: Type -> ok a -> a -> string
adam@1502 412 val ok_int : ok int
adam@1502 413 val ok_float : ok float
adam@1502 414 end
adam@1502 415
adam@1502 416 structure OkType : OK_TYPE = struct
adam@1502 417 class ok a = unit
adam@1502 418 fun importantOperation [a] (_ : ok a) (_ : a) = "You found an OK value!"
adam@1502 419 val ok_int = ()
adam@1502 420 val ok_float = ()
adam@1502 421 end
adam@1502 422
adam@1502 423 open OkType
adam@1502 424
adam@1502 425 (* begin eval *)
adam@1502 426 importantOperation 13
adam@1502 427 (* end *)
adam@1502 428
adam@1502 429 (* Like Haskell, Ur supports the more general notion of <b>constructor classes</b>, whose instances may be parameterized over constructors with kinds beside <tt>Type</tt>. Also like in Haskell, the flagship constructor class is <tt>monad</tt>. Ur/Web's counterpart of Haskell's <tt>IO</tt> monad is <tt>transaction</tt>, which indicates the tight coupling with transactional execution in server-side code. Just as in Haskell, <tt>transaction</tt> must be used to create side-effecting actions, since Ur is purely functional (but has eager evaluation). Here is a quick example transaction, showcasing Ur's variation on Haskell <tt>do</tt> notation. *)
adam@1502 430
adam@1502 431 val readBack : transaction int =
adam@1502 432 src <- source 0;
adam@1502 433 set src 1;
adam@1502 434 n <- get src;
adam@1502 435 return (n + 1)
adam@1502 436
adam@1502 437 (* We get ahead of ourselves a bit here, as this example uses functions associated with client-side code to create and manipulate a mutable data source. *)