Mercurial > urweb

annotate doc/intro.ur @ 1508:d236dbf1b3e3

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