adam@1500: (* Chapter 1: Introduction *)
adam@1494:
adam@1497: (* begin hide *)
adam@1497: val show_string = mkShow (fn s => "\"" ^ s ^ "\"")
adam@1497: (* end *)
adam@1495:
adam@1497: (* This tutorial by Adam Chlipala is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License. *)
adam@1493:
adam@1497: (* This is a tutorial for the Ur/Web programming language. The official project web site 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:
adam@1497: (* 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:
adam@1497: (* * Basics *)
adam@1497:
adam@1501: (* 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:
adam@1493: (* begin eval *)
adam@1497: 1 + 1
adam@1493: (* end *)
adam@1493:
adam@1497: (* begin eval *)
adam@1497: 1.2 + 3.4
adam@1497: (* end *)
adam@1496:
adam@1497: (* begin eval *)
adam@1497: "Hello " ^ "world!"
adam@1497: (* end *)
adam@1497:
adam@1497: (* begin eval *)
adam@1497: 1 + 1 < 6
adam@1497: (* end *)
adam@1497:
adam@1497: (* begin eval *)
adam@1497: 0.0 < -3.2
adam@1497: (* end *)
adam@1497:
adam@1497: (* begin eval *)
adam@1497: "Hello" = "Goodbye" || (1 * 2 <> 8 && True <> False)
adam@1497: (* end *)
adam@1497:
adam@1497: (* We also have function definitions with type inference for parameter and return types. *)
adam@1497:
adam@1497: fun double n = 2 * n
adam@1497:
adam@1497: (* begin eval *)
adam@1497: double 8
adam@1497: (* end *)
adam@1497:
adam@1497: fun fact n = if n = 0 then 1 else n * fact (n - 1)
adam@1497:
adam@1497: (* begin eval *)
adam@1497: fact 5
adam@1497: (* end *)
adam@1497:
adam@1497: (* Of course we have anonymous functions, too. *)
adam@1497:
adam@1497: val inc = fn x => x + 1
adam@1497:
adam@1497: (* begin eval *)
adam@1497: inc 3
adam@1497: (* end *)
adam@1497:
adam@1497: (* 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:
adam@1497: fun id [a] (x : a) : a = x
adam@1497:
adam@1497: (* begin eval *)
adam@1497: id "hi"
adam@1497: (* end *)
adam@1497:
adam@1497: fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x)
adam@1497:
adam@1497: (* begin eval *)
adam@1497: compose inc inc 3
adam@1497: (* end *)
adam@1498:
adam@1501: (* 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:
adam@1498: fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
adam@1498:
adam@1498: (* begin hide *)
adam@1498: fun show_option [t] (_ : show t) : show (option t) =
adam@1498: mkShow (fn x => case x of
adam@1498: None => "None"
adam@1498: | Some x => "Some(" ^ show x ^ ")")
adam@1498: (* end *)
adam@1498:
adam@1498: (* begin eval *)
adam@1498: predecessor 6
adam@1498: (* end *)
adam@1498:
adam@1498: (* begin eval *)
adam@1498: predecessor 0
adam@1498: (* end *)
adam@1499:
adam@1499: (* Naturally, there are lists, too! *)
adam@1499:
adam@1499: val numbers : list int = 1 :: 2 :: 3 :: []
adam@1499: val strings : list string = "a" :: "bc" :: []
adam@1499:
adam@1499: fun length [a] (ls : list a) : int =
adam@1499: case ls of
adam@1499: [] => 0
adam@1499: | _ :: ls' => 1 + length ls'
adam@1499:
adam@1499: (* begin eval *)
adam@1499: length numbers
adam@1499: (* end *)
adam@1499:
adam@1499: (* begin eval *)
adam@1499: length strings
adam@1499: (* end *)
adam@1500:
adam@1501: (* 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:
adam@1500: (* begin hide *)
adam@1500: fun show_list [t] (_ : show t) : show (list t) =
adam@1500: mkShow (let
adam@1500: fun shower (ls : list t) =
adam@1500: case ls of
adam@1500: [] => "[]"
adam@1500: | x :: ls' => show x ^ " :: " ^ shower ls'
adam@1500: in
adam@1500: shower
adam@1500: end)
adam@1500: (* end *)
adam@1500:
adam@1500: fun mp [a] [b] (f : a -> b) : list a -> list b =
adam@1500: let
adam@1500: fun loop (ls : list a) =
adam@1500: case ls of
adam@1500: [] => []
adam@1500: | x :: ls' => f x :: loop ls'
adam@1500: in
adam@1500: loop
adam@1500: end
adam@1500:
adam@1500: (* begin eval *)
adam@1500: mp inc numbers
adam@1500: (* end *)
adam@1500:
adam@1500: (* begin eval *)
adam@1500: mp (fn s => s ^ "!") strings
adam@1500: (* end *)
adam@1500:
adam@1500: (* We can define our own polymorphic datatypes and write higher-order functions over them. *)
adam@1500:
adam@1500: datatype tree a = Leaf of a | Node of tree a * tree a
adam@1500:
adam@1500: (* begin hide *)
adam@1500: fun show_tree [t] (_ : show t) : show (tree t) =
adam@1500: mkShow (let
adam@1500: fun shower (t : tree t) =
adam@1500: case t of
adam@1500: Leaf x => "Leaf(" ^ show x ^ ")"
adam@1500: | Node (t1, t2) => "Node(" ^ shower t1 ^ ", " ^ shower t2 ^ ")"
adam@1500: in
adam@1500: shower
adam@1500: end)
adam@1500: (* end *)
adam@1500:
adam@1500: fun size [a] (t : tree a) : int =
adam@1500: case t of
adam@1500: Leaf _ => 1
adam@1500: | Node (t1, t2) => size t1 + size t2
adam@1500:
adam@1500: (* begin eval *)
adam@1500: size (Node (Leaf 0, Leaf 1))
adam@1500: (* end *)
adam@1500:
adam@1500: (* begin eval *)
adam@1500: size (Node (Leaf 1.2, Node (Leaf 3.4, Leaf 4.5)))
adam@1500: (* end *)
adam@1500:
adam@1500: fun tmap [a] [b] (f : a -> b) : tree a -> tree b =
adam@1500: let
adam@1500: fun loop (t : tree a) : tree b =
adam@1500: case t of
adam@1500: Leaf x => Leaf (f x)
adam@1500: | Node (t1, t2) => Node (loop t1, loop t2)
adam@1500: in
adam@1500: loop
adam@1500: end
adam@1500:
adam@1500: (* begin eval *)
adam@1500: tmap inc (Node (Leaf 0, Leaf 1))
adam@1500: (* end *)
adam@1500:
adam@1501: (* 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:
adam@1500: val x = { A = 0, B = 1.2, C = "hi", D = True }
adam@1500:
adam@1500: (* begin eval *)
adam@1500: x.A
adam@1500: (* end *)
adam@1500:
adam@1500: (* begin eval *)
adam@1500: x.C
adam@1500: (* end *)
adam@1500:
adam@1500: type myRecord = { A : int, B : float, C : string, D : bool }
adam@1500:
adam@1500: fun getA (r : myRecord) = r.A
adam@1500:
adam@1500: (* begin eval *)
adam@1500: getA x
adam@1500: (* end *)
adam@1500:
adam@1500: (* begin eval *)
adam@1500: getA (x -- #A ++ {A = 4})
adam@1500: (* end *)
adam@1500:
adam@1500: val y = { A = "uhoh", B = 2.3, C = "bye", D = False }
adam@1500:
adam@1500: (* begin eval *)
adam@1500: getA (y -- #A ++ {A = 5})
adam@1500: (* end *)
adam@1501:
adam@1501:
adam@1501: (* * Borrowed from ML *)
adam@1501:
adam@1501: (* Ur includes an ML-style module system. The most basic use case involves packaging abstract types with their "methods." *)
adam@1501:
adam@1501: signature COUNTER = sig
adam@1501: type t
adam@1501: val zero : t
adam@1501: val increment : t -> t
adam@1501: val toInt : t -> int
adam@1501: end
adam@1501:
adam@1501: structure Counter : COUNTER = struct
adam@1501: type t = int
adam@1501: val zero = 9
adam@1501: val increment = plus 1
adam@1501: fun toInt x = x
adam@1501: end
adam@1501:
adam@1501: (* begin eval *)
adam@1501: Counter.toInt (Counter.increment Counter.zero)
adam@1501: (* end *)
adam@1501:
adam@1501: (* We may package not just abstract types, but also abstract type families. Here we see our first use of the con keyword, which stands for constructor. Constructors are a generalization of types to include other "compile-time things"; for instance, type families, which are assigned the kind Type -> Type. Kinds are to constructors as types are to normal values. We also see how to write the type of a polymorphic function, using the ::: syntax for type variable binding. This ::: differs from the :: used with the con 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:
adam@1501: signature STACK = sig
adam@1501: con t :: Type -> Type
adam@1501: val empty : a ::: Type -> t a
adam@1501: val push : a ::: Type -> t a -> a -> t a
adam@1501: val pop : a ::: Type -> t a -> option a
adam@1501: end
adam@1501:
adam@1501: structure Stack : STACK = struct
adam@1501: con t = list
adam@1501: val empty [a] = []
adam@1501: fun push [a] (t : t a) (x : a) = x :: t
adam@1501: fun pop [a] (t : t a) = case t of
adam@1501: [] => None
adam@1501: | x :: _ => Some x
adam@1501: end
adam@1501:
adam@1501: (* begin eval *)
adam@1501: Stack.pop (Stack.push (Stack.push Stack.empty "A") "B")
adam@1501: (* end *)
adam@1501:
adam@1501: (* Ur also inherits the ML concept of functors, which are functions from modules to modules. *)
adam@1501:
adam@1501: datatype order = Less | Equal | Greater
adam@1501:
adam@1501: signature COMPARABLE = sig
adam@1501: type t
adam@1501: val compare : t -> t -> order
adam@1501: end
adam@1501:
adam@1501: signature DICTIONARY = sig
adam@1501: type key
adam@1501: con t :: Type -> Type
adam@1501: val empty : a ::: Type -> t a
adam@1501: val insert : a ::: Type -> t a -> key -> a -> t a
adam@1501: val lookup : a ::: Type -> t a -> key -> option a
adam@1501: end
adam@1501:
adam@1501: functor BinarySearchTree(M : COMPARABLE) : DICTIONARY where type key = M.t = struct
adam@1501: type key = M.t
adam@1501: datatype t a = Leaf | Node of t a * key * a * t a
adam@1501:
adam@1501: val empty [a] = Leaf
adam@1501:
adam@1501: fun insert [a] (t : t a) (k : key) (v : a) : t a =
adam@1501: case t of
adam@1501: Leaf => Node (Leaf, k, v, Leaf)
adam@1501: | Node (left, k', v', right) =>
adam@1501: case M.compare k' k of
adam@1501: Equal => Node (left, k, v, right)
adam@1501: | Less => Node (insert left k v, k', v', right)
adam@1501: | Greater => Node (left, k', v', insert right k v)
adam@1501:
adam@1501: fun lookup [a] (t : t a) (k : key) : option a =
adam@1501: case t of
adam@1501: Leaf => None
adam@1501: | Node (left, k', v, right) =>
adam@1501: case M.compare k' k of
adam@1501: Equal => Some v
adam@1501: | Less => lookup left k
adam@1501: | Greater => lookup right k
adam@1501: end
adam@1501:
adam@1501: structure IntTree = BinarySearchTree(struct
adam@1501: type t = int
adam@1501: fun compare n1 n2 =
adam@1501: if n1 = n2 then
adam@1501: Equal
adam@1501: else if n1 < n2 then
adam@1501: Less
adam@1501: else
adam@1501: Greater
adam@1501: end)
adam@1501:
adam@1501: (* begin eval *)
adam@1501: IntTree.lookup (IntTree.insert (IntTree.insert IntTree.empty 0 "A") 1 "B") 1
adam@1501: (* end *)
adam@1501:
adam@1501: (* It is sometimes handy to rebind modules to shorter names. *)
adam@1501:
adam@1501: structure IT = IntTree
adam@1501:
adam@1501: (* begin eval *)
adam@1501: IT.lookup (IT.insert (IT.insert IT.empty 0 "A") 1 "B") 0
adam@1501: (* end *)
adam@1501:
adam@1501: (* One can even use the open 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:
adam@1501: open IT
adam@1501:
adam@1501: (* begin eval *)
adam@1501: lookup (insert (insert empty 0 "A") 1 "B") 2
adam@1501: (* end *)