Mercurial > urweb

annotate doc/intro.ur @ 1501:841b08995259

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Module system tutorial
author Adam Chlipala <adam@chlipala.net>
date Sat, 16 Jul 2011 11:48:11 -0400
parents 483cc0602565
children 2f9b7382dd1d
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@1497 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 where to download the latest code release. In this tutorial, we'll just focus on introducing the language features. *)
adam@1497 10
adam@1497 11 (* Ur/Web contains a web-indendent 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. *)
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@1497 55 (* Of course we have anonymous functions, too. *)
adam@1497 56
adam@1497 57 val inc = fn x => x + 1
adam@1497 58
adam@1497 59 (* begin eval *)
adam@1497 60 inc 3
adam@1497 61 (* end *)
adam@1497 62
adam@1497 63 (* 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 64
adam@1497 65 fun id [a] (x : a) : a = x
adam@1497 66
adam@1497 67 (* begin eval *)
adam@1497 68 id "hi"
adam@1497 69 (* end *)
adam@1497 70
adam@1497 71 fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x)
adam@1497 72
adam@1497 73 (* begin eval *)
adam@1497 74 compose inc inc 3
adam@1497 75 (* end *)
adam@1498 76
adam@1501 77 (* 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 families appear before their arguments, as in Haskell. *)
adam@1498 78
adam@1498 79 fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
adam@1498 80
adam@1498 81 (* begin hide *)
adam@1498 82 fun show_option [t] (_ : show t) : show (option t) =
adam@1498 83 mkShow (fn x => case x of
adam@1498 84 None => "None"
adam@1498 85 | Some x => "Some(" ^ show x ^ ")")
adam@1498 86 (* end *)
adam@1498 87
adam@1498 88 (* begin eval *)
adam@1498 89 predecessor 6
adam@1498 90 (* end *)
adam@1498 91
adam@1498 92 (* begin eval *)
adam@1498 93 predecessor 0
adam@1498 94 (* end *)
adam@1499 95
adam@1499 96 (* Naturally, there are lists, too! *)
adam@1499 97
adam@1499 98 val numbers : list int = 1 :: 2 :: 3 :: []
adam@1499 99 val strings : list string = "a" :: "bc" :: []
adam@1499 100
adam@1499 101 fun length [a] (ls : list a) : int =
adam@1499 102 case ls of
adam@1499 103 [] => 0
adam@1499 104 | _ :: ls' => 1 + length ls'
adam@1499 105
adam@1499 106 (* begin eval *)
adam@1499 107 length numbers
adam@1499 108 (* end *)
adam@1499 109
adam@1499 110 (* begin eval *)
adam@1499 111 length strings
adam@1499 112 (* end *)
adam@1500 113
adam@1501 114 (* 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 115
adam@1500 116 (* begin hide *)
adam@1500 117 fun show_list [t] (_ : show t) : show (list t) =
adam@1500 118 mkShow (let
adam@1500 119 fun shower (ls : list t) =
adam@1500 120 case ls of
adam@1500 121 [] => "[]"
adam@1500 122 | x :: ls' => show x ^ " :: " ^ shower ls'
adam@1500 123 in
adam@1500 124 shower
adam@1500 125 end)
adam@1500 126 (* end *)
adam@1500 127
adam@1500 128 fun mp [a] [b] (f : a -> b) : list a -> list b =
adam@1500 129 let
adam@1500 130 fun loop (ls : list a) =
adam@1500 131 case ls of
adam@1500 132 [] => []
adam@1500 133 | x :: ls' => f x :: loop ls'
adam@1500 134 in
adam@1500 135 loop
adam@1500 136 end
adam@1500 137
adam@1500 138 (* begin eval *)
adam@1500 139 mp inc numbers
adam@1500 140 (* end *)
adam@1500 141
adam@1500 142 (* begin eval *)
adam@1500 143 mp (fn s => s ^ "!") strings
adam@1500 144 (* end *)
adam@1500 145
adam@1500 146 (* We can define our own polymorphic datatypes and write higher-order functions over them. *)
adam@1500 147
adam@1500 148 datatype tree a = Leaf of a | Node of tree a * tree a
adam@1500 149
adam@1500 150 (* begin hide *)
adam@1500 151 fun show_tree [t] (_ : show t) : show (tree t) =
adam@1500 152 mkShow (let
adam@1500 153 fun shower (t : tree t) =
adam@1500 154 case t of
adam@1500 155 Leaf x => "Leaf(" ^ show x ^ ")"
adam@1500 156 | Node (t1, t2) => "Node(" ^ shower t1 ^ ", " ^ shower t2 ^ ")"
adam@1500 157 in
adam@1500 158 shower
adam@1500 159 end)
adam@1500 160 (* end *)
adam@1500 161
adam@1500 162 fun size [a] (t : tree a) : int =
adam@1500 163 case t of
adam@1500 164 Leaf _ => 1
adam@1500 165 | Node (t1, t2) => size t1 + size t2
adam@1500 166
adam@1500 167 (* begin eval *)
adam@1500 168 size (Node (Leaf 0, Leaf 1))
adam@1500 169 (* end *)
adam@1500 170
adam@1500 171 (* begin eval *)
adam@1500 172 size (Node (Leaf 1.2, Node (Leaf 3.4, Leaf 4.5)))
adam@1500 173 (* end *)
adam@1500 174
adam@1500 175 fun tmap [a] [b] (f : a -> b) : tree a -> tree b =
adam@1500 176 let
adam@1500 177 fun loop (t : tree a) : tree b =
adam@1500 178 case t of
adam@1500 179 Leaf x => Leaf (f x)
adam@1500 180 | Node (t1, t2) => Node (loop t1, loop t2)
adam@1500 181 in
adam@1500 182 loop
adam@1500 183 end
adam@1500 184
adam@1500 185 (* begin eval *)
adam@1500 186 tmap inc (Node (Leaf 0, Leaf 1))
adam@1500 187 (* end *)
adam@1500 188
adam@1501 189 (* 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 190
adam@1500 191 val x = { A = 0, B = 1.2, C = "hi", D = True }
adam@1500 192
adam@1500 193 (* begin eval *)
adam@1500 194 x.A
adam@1500 195 (* end *)
adam@1500 196
adam@1500 197 (* begin eval *)
adam@1500 198 x.C
adam@1500 199 (* end *)
adam@1500 200
adam@1500 201 type myRecord = { A : int, B : float, C : string, D : bool }
adam@1500 202
adam@1500 203 fun getA (r : myRecord) = r.A
adam@1500 204
adam@1500 205 (* begin eval *)
adam@1500 206 getA x
adam@1500 207 (* end *)
adam@1500 208
adam@1500 209 (* begin eval *)
adam@1500 210 getA (x -- #A ++ {A = 4})
adam@1500 211 (* end *)
adam@1500 212
adam@1500 213 val y = { A = "uhoh", B = 2.3, C = "bye", D = False }
adam@1500 214
adam@1500 215 (* begin eval *)
adam@1500 216 getA (y -- #A ++ {A = 5})
adam@1500 217 (* end *)
adam@1501 218
adam@1501 219
adam@1501 220 (* * Borrowed from ML *)
adam@1501 221
adam@1501 222 (* Ur includes an ML-style module system. The most basic use case involves packaging abstract types with their "methods." *)
adam@1501 223
adam@1501 224 signature COUNTER = sig
adam@1501 225 type t
adam@1501 226 val zero : t
adam@1501 227 val increment : t -> t
adam@1501 228 val toInt : t -> int
adam@1501 229 end
adam@1501 230
adam@1501 231 structure Counter : COUNTER = struct
adam@1501 232 type t = int
adam@1501 233 val zero = 9
adam@1501 234 val increment = plus 1
adam@1501 235 fun toInt x = x
adam@1501 236 end
adam@1501 237
adam@1501 238 (* begin eval *)
adam@1501 239 Counter.toInt (Counter.increment Counter.zero)
adam@1501 240 (* end *)
adam@1501 241
adam@1501 242 (* 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, type families, which are assigned the kind <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 243
adam@1501 244 signature STACK = sig
adam@1501 245 con t :: Type -> Type
adam@1501 246 val empty : a ::: Type -> t a
adam@1501 247 val push : a ::: Type -> t a -> a -> t a
adam@1501 248 val pop : a ::: Type -> t a -> option a
adam@1501 249 end
adam@1501 250
adam@1501 251 structure Stack : STACK = struct
adam@1501 252 con t = list
adam@1501 253 val empty [a] = []
adam@1501 254 fun push [a] (t : t a) (x : a) = x :: t
adam@1501 255 fun pop [a] (t : t a) = case t of
adam@1501 256 [] => None
adam@1501 257 | x :: _ => Some x
adam@1501 258 end
adam@1501 259
adam@1501 260 (* begin eval *)
adam@1501 261 Stack.pop (Stack.push (Stack.push Stack.empty "A") "B")
adam@1501 262 (* end *)
adam@1501 263
adam@1501 264 (* Ur also inherits the ML concept of <b>functors</b>, which are functions from modules to modules. *)
adam@1501 265
adam@1501 266 datatype order = Less | Equal | Greater
adam@1501 267
adam@1501 268 signature COMPARABLE = sig
adam@1501 269 type t
adam@1501 270 val compare : t -> t -> order
adam@1501 271 end
adam@1501 272
adam@1501 273 signature DICTIONARY = sig
adam@1501 274 type key
adam@1501 275 con t :: Type -> Type
adam@1501 276 val empty : a ::: Type -> t a
adam@1501 277 val insert : a ::: Type -> t a -> key -> a -> t a
adam@1501 278 val lookup : a ::: Type -> t a -> key -> option a
adam@1501 279 end
adam@1501 280
adam@1501 281 functor BinarySearchTree(M : COMPARABLE) : DICTIONARY where type key = M.t = struct
adam@1501 282 type key = M.t
adam@1501 283 datatype t a = Leaf | Node of t a * key * a * t a
adam@1501 284
adam@1501 285 val empty [a] = Leaf
adam@1501 286
adam@1501 287 fun insert [a] (t : t a) (k : key) (v : a) : t a =
adam@1501 288 case t of
adam@1501 289 Leaf => Node (Leaf, k, v, Leaf)
adam@1501 290 | Node (left, k', v', right) =>
adam@1501 291 case M.compare k' k of
adam@1501 292 Equal => Node (left, k, v, right)
adam@1501 293 | Less => Node (insert left k v, k', v', right)
adam@1501 294 | Greater => Node (left, k', v', insert right k v)
adam@1501 295
adam@1501 296 fun lookup [a] (t : t a) (k : key) : option a =
adam@1501 297 case t of
adam@1501 298 Leaf => None
adam@1501 299 | Node (left, k', v, right) =>
adam@1501 300 case M.compare k' k of
adam@1501 301 Equal => Some v
adam@1501 302 | Less => lookup left k
adam@1501 303 | Greater => lookup right k
adam@1501 304 end
adam@1501 305
adam@1501 306 structure IntTree = BinarySearchTree(struct
adam@1501 307 type t = int
adam@1501 308 fun compare n1 n2 =
adam@1501 309 if n1 = n2 then
adam@1501 310 Equal
adam@1501 311 else if n1 < n2 then
adam@1501 312 Less
adam@1501 313 else
adam@1501 314 Greater
adam@1501 315 end)
adam@1501 316
adam@1501 317 (* begin eval *)
adam@1501 318 IntTree.lookup (IntTree.insert (IntTree.insert IntTree.empty 0 "A") 1 "B") 1
adam@1501 319 (* end *)
adam@1501 320
adam@1501 321 (* It is sometimes handy to rebind modules to shorter names. *)
adam@1501 322
adam@1501 323 structure IT = IntTree
adam@1501 324
adam@1501 325 (* begin eval *)
adam@1501 326 IT.lookup (IT.insert (IT.insert IT.empty 0 "A") 1 "B") 0
adam@1501 327 (* end *)
adam@1501 328
adam@1501 329 (* 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 330
adam@1501 331 open IT
adam@1501 332
adam@1501 333 (* begin eval *)
adam@1501 334 lookup (insert (insert empty 0 "A") 1 "B") 2
adam@1501 335 (* end *)