annotate doc/intro.ur @ 1498:8c32c7191bf0

Make 'static' protocol handle unlimited retry
author Adam Chlipala <adam@chlipala.net>
date Fri, 15 Jul 2011 18:55:58 -0400
parents 0b639858200b
children 92c929793d0f
rev   line source
adam@1494 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@1498 77 (* The "option" type family is like ML's "option" or Haskell's "maybe." 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 *)