Mercurial > urweb

annotate doc/intro.ur @ 1500:483cc0602565

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish tutorial section about common ML/Haskell features
author Adam Chlipala <adam@chlipala.net>
date Fri, 15 Jul 2011 19:21:09 -0400
parents 92c929793d0f
children 841b08995259
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@1497 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, "==" 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@1499 77 (* The "option" type family is like ML's "option" or Haskell's "maybe." We also have a "case" 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@1500 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 "map" is a keyword, so we name our "map" function "mp.") *)
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@1500 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 "++" and the record field removal operator "--". *)
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 *)