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 *)
|