--- a/CookBook/FirstSteps.thy Mon Jan 26 16:09:02 2009 +0000
+++ b/CookBook/FirstSteps.thy Tue Jan 27 05:41:14 2009 +0000
@@ -510,10 +510,10 @@
section {* Combinators\label{sec:combinators} *}
text {*
- Perhaps one of the most puzzling aspect for a beginner when reading
- existing Isabelle code special purpose combinators. At first they
- seem to obstruct the comprehension of the code, but after getting familiar
- with them they actually ease the understanding and also the programming.
+ For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
+ the combinators. At first they seem to greatly obstruct the
+ comprehension of the code, but after getting familiar with them, they
+ 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"}
@@ -525,15 +525,16 @@
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*}
@@ -554,7 +555,8 @@
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
*}
@@ -575,9 +577,13 @@
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
*}
@@ -588,33 +594,30 @@
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
- yields
-
- @{ML_response [display,gray] "inc_by_six 6" "12"}
-
- as expected.
+ increment-by-two, followed by increment-by-three.
- 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).
- The function *}
+ The remaining combinators described in this section 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). The function
-ML{*fun inc_by_three x =
+ *}
+
+ML %linenumbers{*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
+ be merged back into the ``main waterfall''. To do this, the next combinator
+ can be used.
- The combinator @{ML "(op `)"} is similar, but applies a function to the value
- and returns the result together with the original value (as pair). For example
- the following function 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.
+ The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
+ and returns the result together with the value (as a pair). For example
+ the function
*}
ML{*fun inc_as_pair x =
@@ -622,7 +625,13 @@
|> (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:
*}
@@ -636,6 +645,35 @@
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)
*}