isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:8fda6b452f28
+:6dfe6975bda0
 *}
 section {* Combinators\label{sec:combinators} *}
 text {*
-Perhaps one of the most puzzling aspect for a beginner when reading
+For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
-existing Isabelle code special purpose combinators. At first they
+the combinators. At first they seem to greatly obstruct the
-seem to obstruct the comprehension of the code, but after getting familiar
+comprehension of the code, but after getting familiar with them, they
-with them they actually ease the understanding and also the programming.
+actually ease the understanding and also the programming.
 \begin{readmore}
 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
 and @{ML_file "Pure/General/basics.ML"}.
 \end{readmore}
 The simplest combinator is @{ML I} which is just the identity function.
 *}
 ML{*fun I x = x*}
-text {* Another combinator is @{ML K}, defined as *}
+text {* Another simple combinator is @{ML K}, defined as *}
 ML{*fun K x = fn _ => x*}
 text {*
 It ``wraps'' a function around the argument @{text "x"}. However, this
-function ignores its argument.
+function ignores its argument. So @{ML K} defines a constant function
+returning @{text x}.
-The next combinator is reverse application, @{ML "(op |>)"}, defined as
+The next combinator is reverse application, @{ML "|>"}, defined as
 *}
 ML{*fun x |> f = f x*}
 text {* While just syntactic sugar for the usual function application,
 which increments the argument @{text x} by 5. It does this by first incrementing
 the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
 the first component of the pair (Line 4) and finally incrementing the first
 component by 4 (Line 5). This kind of cascading manipulations of values is quite
 common when dealing with theories (for example by adding a definition, followed by
-lemmas and so on). Writing the function @{ML inc_by_five} using the reverse
+lemmas and so on). It should also be familiar to anyone who has used Haskell's
+do-notation. Writing the function @{ML inc_by_five} using the reverse
 application is much clearer than writing
 *}
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 val y3 = fst y2
 val y4 = y3 + 4
 in y4 end*}
 text {*
+Another reason why the let-bindings in the code above are better to be
+avoided: it is more than easy to get the intermediate values wrong!
 (FIXME: give a real world example involving theories)
-Similarly, the combinator @{ML "(op #>)"} is the reverse function
+Similarly, the combinator @{ML "#>"} is the reverse function
 composition. It can be used to define functions as follows
 *}
 ML{*val inc_by_six =
 (fn x => x + 1)
 #> (fn x => x + 2)
 #> (fn x => x + 3)*}
 text {*
 which is the function composed of first the increment-by-one function and then
-increment-by-two, followed by increment-by-three. Applying 6 to this function
+increment-by-two, followed by increment-by-three.
-yields
+The remaining combinators described in this section add convenience for the
-@{ML_response [display,gray] "inc_by_six 6" "12"}
+``waterfall method'' of writing functions. The combinator @{ML tap} allows
+one to get hold of an intermediate result (to do some side-calculations for
-as expected.
+instance). The function
-The remaining combinators add convenience for the ``waterfall method''
+*}
-of writing functions. The combinator @{ML tap} allows one to get
-hold of an intermediate result (to do some side-calculations for instance).
+ML %linenumbers{*fun inc_by_three x =
-The function *}
-ML{*fun inc_by_three x =
 x |> (fn x => x + 1)
 |> tap (fn x => tracing (makestring x))
 |> (fn x => x + 2)*}
 text {* increments the argument first by one and then by two. In the middle,
 however, it uses @{ML tap} for printing the ``plus-one'' intermediate
-result inside the tracing buffer.
+result inside the tracing buffer (Line 3). The function @{ML tap} can only
+be used for side-calculations, because any value that is computed cannot
-The combinator @{ML "(op `)"} is similar, but applies a function to the value
+be merged back into the ``main waterfall''. To do this, the next combinator
-and returns the result together with the original value (as pair). For example
+can be used.
-the following function takes @{text x} as argument, and then first
-increments @{text x}, but also keeps @{text x}. The intermediate result is
+The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
-therefore the pair @{ML "(x + 1,x)" for x}. The function then increments the
+and returns the result together with the value (as a pair). For example
-right-hand component of the pair.
+the function
 *}
 ML{*fun inc_as_pair x =
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))*}
 text {*
-The combinators @{ML "(op |>>)"} and @{ML "(op ||>)"} are defined for
+takes @{text x} as argument, and then first
+increments @{text x}, but also keeps @{text x}. The intermediate result is
+therefore the pair @{ML "(x + 1, x)" for x}. The function then increments the
+right-hand component of the pair. So finally the result will be
+@{ML "(x + 1, x + 1)" for x}.
+The combinators @{ML "|>>"} and @{ML "||>"} are defined for
 functions manipulating pairs. The first applies the function to
 the first component of the pair, defined as:
 *}
 ML{*fun (x, y) |>> f = (f x, y)*}
 *}
 ML{*fun (x, y) ||> f = (x, f y)*}
 text {*
+With the combinator @{ML "|->"} you can re-combine the elements from a pair.
+This combinator is defined as
+*}
+ML{*fun (x, y) |-> f = f x y*}
+text {* and can be used to write the following version of the @{text double} function *}
+ML{*fun double x =
+x |>  (fn x => (x, x))
+|-> (fn x => fn y => x + y)*}
+text {*
+Recall that @{ML "|>"} is the reverse function applications. The related
+reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"},
+@{ML "|>>"} and @{ML "||>"} described above have related combinators for function
+composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. In this
+way, the function @{text double} can also be written as
+*}
+ML{*val double =
+(fn x => (x, x))
+#-> (fn x => fn y => x + y)*}
+text {*
 (FIXME: find a good exercise for combinators)
 *}
 end

changeset 82	6dfe6975bda0
parent 81	8fda6b452f28
child 84	624279d187e1