Mercurial > urweb

annotate doc/intro.ur @ 2110:9e9c915f554c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A new MonoReduce optimization for lifting 'let' out of field projection; JavaScript compilation for exponentiation
author Adam Chlipala <adam@chlipala.net>
date Sun, 01 Feb 2015 12:29:14 -0500
parents 2d9f831d45c9
children 544199d8b14a
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@1511 9 (* This is a tutorial for the <a href="http://www.impredicative.com/ur/">Ur/Web</a> programming language.<br>
adam@1510 10 <br>
adam@1513 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><a target="_top" href="http://en.wikipedia.org/wiki/Metaprogramming">metaprogramming</a></b> based on <b><a target=_"top" href="http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.6387">row types</a></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@1511 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.<br>
adam@1511 16 <br>
adam@1511 17 For information on compiling applications (and for some full example applications), see the intro page of <a href="http://www.impredicative.com/ur/demo/">the online demo</a>, with further detail available in <a href="http://www.impredicative.com/ur/manual.pdf">the reference manual</a>. *)
adam@1497 18
adam@1497 19 (* * Basics *)
adam@1497 20
adam@1501 21 (* 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 22
adam@1493 23 (* begin eval *)
adam@1497 24 1 + 1
adam@1493 25 (* end *)
adam@1493 26
adam@1497 27 (* begin eval *)
adam@1497 28 1.2 + 3.4
adam@1497 29 (* end *)
adam@1496 30
adam@1497 31 (* begin eval *)
adam@1497 32 "Hello " ^ "world!"
adam@1497 33 (* end *)
adam@1497 34
adam@1497 35 (* begin eval *)
adam@1497 36 1 + 1 < 6
adam@1497 37 (* end *)
adam@1497 38
adam@1497 39 (* begin eval *)
adam@1497 40 0.0 < -3.2
adam@1497 41 (* end *)
adam@1497 42
adam@1497 43 (* begin eval *)
adam@1497 44 "Hello" = "Goodbye" || (1 * 2 <> 8 && True <> False)
adam@1497 45 (* end *)
adam@1497 46
adam@1497 47 (* We also have function definitions with type inference for parameter and return types. *)
adam@1497 48
adam@1497 49 fun double n = 2 * n
adam@1497 50
adam@1497 51 (* begin eval *)
adam@1497 52 double 8
adam@1497 53 (* end *)
adam@1497 54
adam@1497 55 fun fact n = if n = 0 then 1 else n * fact (n - 1)
adam@1497 56
adam@1497 57 (* begin eval *)
adam@1497 58 fact 5
adam@1497 59 (* end *)
adam@1497 60
adam@1502 61 fun isEven n = n = 0 || isOdd (n - 1)
adam@1502 62 and isOdd n = n = 1 || isEven (n - 1)
adam@1502 63
adam@1502 64 (* begin eval *)
adam@1502 65 isEven 32
adam@1502 66 (* end *)
adam@1502 67
adam@1502 68
adam@1497 69 (* Of course we have anonymous functions, too. *)
adam@1497 70
adam@1497 71 val inc = fn x => x + 1
adam@1497 72
adam@1497 73 (* begin eval *)
adam@1497 74 inc 3
adam@1497 75 (* end *)
adam@1497 76
adam@1497 77 (* 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 78
adam@1497 79 fun id [a] (x : a) : a = x
adam@1497 80
adam@1497 81 (* begin eval *)
adam@1497 82 id "hi"
adam@1497 83 (* end *)
adam@1497 84
adam@1497 85 fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x)
adam@1497 86
adam@1497 87 (* begin eval *)
adam@1497 88 compose inc inc 3
adam@1497 89 (* end *)
adam@1498 90
adam@1502 91 (* 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 92
adam@1498 93 fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
adam@1498 94
adam@1498 95 (* begin hide *)
adam@1498 96 fun show_option [t] (_ : show t) : show (option t) =
adam@1498 97 mkShow (fn x => case x of
adam@1498 98 None => "None"
adam@1498 99 | Some x => "Some(" ^ show x ^ ")")
adam@1498 100 (* end *)
adam@1498 101
adam@1498 102 (* begin eval *)
adam@1498 103 predecessor 6
adam@1498 104 (* end *)
adam@1498 105
adam@1498 106 (* begin eval *)
adam@1498 107 predecessor 0
adam@1498 108 (* end *)
adam@1499 109
adam@1499 110 (* Naturally, there are lists, too! *)
adam@1499 111
adam@1499 112 val numbers : list int = 1 :: 2 :: 3 :: []
adam@1499 113 val strings : list string = "a" :: "bc" :: []
adam@1499 114
adam@1499 115 fun length [a] (ls : list a) : int =
adam@1499 116 case ls of
adam@1499 117 [] => 0
adam@1499 118 | _ :: ls' => 1 + length ls'
adam@1499 119
adam@1499 120 (* begin eval *)
adam@1499 121 length numbers
adam@1499 122 (* end *)
adam@1499 123
adam@1499 124 (* begin eval *)
adam@1499 125 length strings
adam@1499 126 (* end *)
adam@1500 127
adam@1502 128 (* 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 129
adam@1500 130 (* begin hide *)
adam@1500 131 fun show_list [t] (_ : show t) : show (list t) =
adam@1500 132 mkShow (let
adam@1500 133 fun shower (ls : list t) =
adam@1500 134 case ls of
adam@1500 135 [] => "[]"
adam@1500 136 | x :: ls' => show x ^ " :: " ^ shower ls'
adam@1500 137 in
adam@1500 138 shower
adam@1500 139 end)
adam@1500 140 (* end *)
adam@1500 141
adam@1500 142 fun mp [a] [b] (f : a -> b) : list a -> list b =
adam@1500 143 let
adam@1500 144 fun loop (ls : list a) =
adam@1500 145 case ls of
adam@1500 146 [] => []
adam@1500 147 | x :: ls' => f x :: loop ls'
adam@1500 148 in
adam@1500 149 loop
adam@1500 150 end
adam@1500 151
adam@1500 152 (* begin eval *)
adam@1500 153 mp inc numbers
adam@1500 154 (* end *)
adam@1500 155
adam@1500 156 (* begin eval *)
adam@1500 157 mp (fn s => s ^ "!") strings
adam@1500 158 (* end *)
adam@1500 159
adam@1500 160 (* We can define our own polymorphic datatypes and write higher-order functions over them. *)
adam@1500 161
adam@1500 162 datatype tree a = Leaf of a | Node of tree a * tree a
adam@1500 163
adam@1500 164 (* begin hide *)
adam@1500 165 fun show_tree [t] (_ : show t) : show (tree t) =
adam@1500 166 mkShow (let
adam@1500 167 fun shower (t : tree t) =
adam@1500 168 case t of
adam@1500 169 Leaf x => "Leaf(" ^ show x ^ ")"
adam@1500 170 | Node (t1, t2) => "Node(" ^ shower t1 ^ ", " ^ shower t2 ^ ")"
adam@1500 171 in
adam@1500 172 shower
adam@1500 173 end)
adam@1500 174 (* end *)
adam@1500 175
adam@1500 176 fun size [a] (t : tree a) : int =
adam@1500 177 case t of
adam@1500 178 Leaf _ => 1
adam@1500 179 | Node (t1, t2) => size t1 + size t2
adam@1500 180
adam@1500 181 (* begin eval *)
adam@1500 182 size (Node (Leaf 0, Leaf 1))
adam@1500 183 (* end *)
adam@1500 184
adam@1500 185 (* begin eval *)
adam@1500 186 size (Node (Leaf 1.2, Node (Leaf 3.4, Leaf 4.5)))
adam@1500 187 (* end *)
adam@1500 188
adam@1500 189 fun tmap [a] [b] (f : a -> b) : tree a -> tree b =
adam@1500 190 let
adam@1500 191 fun loop (t : tree a) : tree b =
adam@1500 192 case t of
adam@1500 193 Leaf x => Leaf (f x)
adam@1500 194 | Node (t1, t2) => Node (loop t1, loop t2)
adam@1500 195 in
adam@1500 196 loop
adam@1500 197 end
adam@1500 198
adam@1500 199 (* begin eval *)
adam@1500 200 tmap inc (Node (Leaf 0, Leaf 1))
adam@1500 201 (* end *)
adam@1500 202
adam@1501 203 (* 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 204
adam@1500 205 val x = { A = 0, B = 1.2, C = "hi", D = True }
adam@1500 206
adam@1500 207 (* begin eval *)
adam@1500 208 x.A
adam@1500 209 (* end *)
adam@1500 210
adam@1500 211 (* begin eval *)
adam@1500 212 x.C
adam@1500 213 (* end *)
adam@1500 214
adam@1500 215 type myRecord = { A : int, B : float, C : string, D : bool }
adam@1500 216
adam@1500 217 fun getA (r : myRecord) = r.A
adam@1500 218
adam@1500 219 (* begin eval *)
adam@1500 220 getA x
adam@1500 221 (* end *)
adam@1500 222
adam@1500 223 (* begin eval *)
adam@1500 224 getA (x -- #A ++ {A = 4})
adam@1500 225 (* end *)
adam@1500 226
adam@1500 227 val y = { A = "uhoh", B = 2.3, C = "bye", D = False }
adam@1500 228
adam@1500 229 (* begin eval *)
adam@1500 230 getA (y -- #A ++ {A = 5})
adam@1500 231 (* end *)
adam@1501 232
adam@1501 233
adam@1501 234 (* * Borrowed from ML *)
adam@1501 235
adam@1502 236 (* Ur includes an ML-style <b>module system</b>. The most basic use case involves packaging abstract types with their "methods." *)
adam@1501 237
adam@1501 238 signature COUNTER = sig
adam@1501 239 type t
adam@1501 240 val zero : t
adam@1501 241 val increment : t -> t
adam@1501 242 val toInt : t -> int
adam@1501 243 end
adam@1501 244
adam@1501 245 structure Counter : COUNTER = struct
adam@1501 246 type t = int
adam@1502 247 val zero = 0
adam@1501 248 val increment = plus 1
adam@1501 249 fun toInt x = x
adam@1501 250 end
adam@1501 251
adam@1501 252 (* begin eval *)
adam@1501 253 Counter.toInt (Counter.increment Counter.zero)
adam@1501 254 (* end *)
adam@1501 255
adam@1502 256 (* 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 257
adam@1501 258 signature STACK = sig
adam@1501 259 con t :: Type -> Type
adam@1501 260 val empty : a ::: Type -> t a
adam@1501 261 val push : a ::: Type -> t a -> a -> t a
adam@1525 262 val peek : a ::: Type -> t a -> option a
adam@1525 263 val pop : a ::: Type -> t a -> option (t a)
adam@1501 264 end
adam@1501 265
adam@1501 266 structure Stack : STACK = struct
adam@1501 267 con t = list
adam@1501 268 val empty [a] = []
adam@1501 269 fun push [a] (t : t a) (x : a) = x :: t
adam@1525 270 fun peek [a] (t : t a) = case t of
adam@1525 271 [] => None
adam@1525 272 | x :: _ => Some x
adam@1501 273 fun pop [a] (t : t a) = case t of
adam@1525 274 [] => None
adam@1525 275 | _ :: t' => Some t'
adam@1501 276 end
adam@1501 277
adam@1501 278 (* begin eval *)
adam@1525 279 Stack.peek (Stack.push (Stack.push Stack.empty "A") "B")
adam@1501 280 (* end *)
adam@1501 281
adam@1501 282 (* Ur also inherits the ML concept of <b>functors</b>, which are functions from modules to modules. *)
adam@1501 283
adam@1501 284 datatype order = Less | Equal | Greater
adam@1501 285
adam@1501 286 signature COMPARABLE = sig
adam@1501 287 type t
adam@1501 288 val compare : t -> t -> order
adam@1501 289 end
adam@1501 290
adam@1501 291 signature DICTIONARY = sig
adam@1501 292 type key
adam@1501 293 con t :: Type -> Type
adam@1501 294 val empty : a ::: Type -> t a
adam@1501 295 val insert : a ::: Type -> t a -> key -> a -> t a
adam@1501 296 val lookup : a ::: Type -> t a -> key -> option a
adam@1501 297 end
adam@1501 298
adam@1501 299 functor BinarySearchTree(M : COMPARABLE) : DICTIONARY where type key = M.t = struct
adam@1501 300 type key = M.t
adam@1501 301 datatype t a = Leaf | Node of t a * key * a * t a
adam@1501 302
adam@1501 303 val empty [a] = Leaf
adam@1501 304
adam@1501 305 fun insert [a] (t : t a) (k : key) (v : a) : t a =
adam@1501 306 case t of
adam@1501 307 Leaf => Node (Leaf, k, v, Leaf)
adam@1501 308 | Node (left, k', v', right) =>
adam@1502 309 case M.compare k k' of
adam@1501 310 Equal => Node (left, k, v, right)
adam@1501 311 | Less => Node (insert left k v, k', v', right)
adam@1501 312 | Greater => Node (left, k', v', insert right k v)
adam@1501 313
adam@1501 314 fun lookup [a] (t : t a) (k : key) : option a =
adam@1501 315 case t of
adam@1501 316 Leaf => None
adam@1501 317 | Node (left, k', v, right) =>
adam@1502 318 case M.compare k k' of
adam@1501 319 Equal => Some v
adam@1501 320 | Less => lookup left k
adam@1501 321 | Greater => lookup right k
adam@1501 322 end
adam@1501 323
adam@1501 324 structure IntTree = BinarySearchTree(struct
adam@1501 325 type t = int
adam@1501 326 fun compare n1 n2 =
adam@1501 327 if n1 = n2 then
adam@1501 328 Equal
adam@1501 329 else if n1 < n2 then
adam@1501 330 Less
adam@1501 331 else
adam@1501 332 Greater
adam@1501 333 end)
adam@1501 334
adam@1501 335 (* begin eval *)
adam@1501 336 IntTree.lookup (IntTree.insert (IntTree.insert IntTree.empty 0 "A") 1 "B") 1
adam@1501 337 (* end *)
adam@1501 338
adam@1501 339 (* It is sometimes handy to rebind modules to shorter names. *)
adam@1501 340
adam@1501 341 structure IT = IntTree
adam@1501 342
adam@1501 343 (* begin eval *)
adam@1501 344 IT.lookup (IT.insert (IT.insert IT.empty 0 "A") 1 "B") 0
adam@1501 345 (* end *)
adam@1501 346
adam@1501 347 (* 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 348
adam@1501 349 open IT
adam@1501 350
adam@1501 351 (* begin eval *)
adam@1501 352 lookup (insert (insert empty 0 "A") 1 "B") 2
adam@1501 353 (* end *)
adam@1502 354
adam@1502 355 (* 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 356
adam@1502 357
adam@1502 358 (* * Borrowed from Haskell *)
adam@1502 359
adam@1502 360 (* 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 361
adam@1502 362 fun max [a] (_ : ord a) (x : a) (y : a) : a =
adam@1502 363 if x < y then
adam@1502 364 y
adam@1502 365 else
adam@1502 366 x
adam@1502 367
adam@1502 368 (* begin eval *)
adam@1502 369 max 1 2
adam@1502 370 (* end *)
adam@1502 371
adam@1502 372 (* begin eval *)
adam@1502 373 max "ABC" "ABA"
adam@1502 374 (* end *)
adam@1502 375
adam@1502 376 (* The idiomatic way to define a new type class is to stash it inside a module, like in this example: *)
adam@1502 377
adam@1502 378 signature DOUBLE = sig
adam@1502 379 class double
adam@1502 380 val double : a ::: Type -> double a -> a -> a
adam@1502 381 val mkDouble : a ::: Type -> (a -> a) -> double a
adam@1502 382
adam@1502 383 val double_int : double int
adam@1502 384 val double_string : double string
adam@1502 385 end
adam@1502 386
adam@1502 387 structure Double : DOUBLE = struct
adam@1814 388 con double a = a -> a
adam@1502 389
adam@1502 390 fun double [a] (f : double a) (x : a) : a = f x
adam@1502 391 fun mkDouble [a] (f : a -> a) : double a = f
adam@1502 392
adam@1502 393 val double_int = mkDouble (times 2)
adam@1502 394 val double_string = mkDouble (fn s => s ^ s)
adam@1502 395 end
adam@1502 396
adam@1502 397 open Double
adam@1502 398
adam@1502 399 (* begin eval *)
adam@1502 400 double 13
adam@1502 401 (* end *)
adam@1502 402
adam@1502 403 (* begin eval *)
adam@1502 404 double "ho"
adam@1502 405 (* end *)
adam@1502 406
adam@1502 407 val double_float = mkDouble (times 2.0)
adam@1502 408
adam@1502 409 (* begin eval *)
adam@1502 410 double 2.3
adam@1502 411 (* end *)
adam@1502 412
adam@1502 413 (* 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 414
adam@1502 415 signature OK_TYPE = sig
adam@1502 416 class ok
adam@1502 417 val importantOperation : a ::: Type -> ok a -> a -> string
adam@1502 418 val ok_int : ok int
adam@1502 419 val ok_float : ok float
adam@1502 420 end
adam@1502 421
adam@1502 422 structure OkType : OK_TYPE = struct
adam@1814 423 con ok a = unit
adam@1502 424 fun importantOperation [a] (_ : ok a) (_ : a) = "You found an OK value!"
adam@1502 425 val ok_int = ()
adam@1502 426 val ok_float = ()
adam@1502 427 end
adam@1502 428
adam@1502 429 open OkType
adam@1502 430
adam@1502 431 (* begin eval *)
adam@1502 432 importantOperation 13
adam@1502 433 (* end *)
adam@1502 434
adam@1502 435 (* 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 436
adam@1502 437 val readBack : transaction int =
adam@1502 438 src <- source 0;
adam@1502 439 set src 1;
adam@1502 440 n <- get src;
adam@1502 441 return (n + 1)
adam@1502 442
adam@1502 443 (* 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. *)