Mercurial > urweb

annotate doc/intro.ur @ 2195:18e6fb487880

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