515 comprehension of the code, but after getting familiar with them, they |
515 comprehension of the code, but after getting familiar with them, they |
516 actually ease the understanding and also the programming. |
516 actually ease the understanding and also the programming. |
517 |
517 |
518 \begin{readmore} |
518 \begin{readmore} |
519 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} |
519 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} |
520 and @{ML_file "Pure/General/basics.ML"}. |
520 and @{ML_file "Pure/General/basics.ML"}. The section ?? in the implementation manual |
|
521 contains also information about combinators. |
521 \end{readmore} |
522 \end{readmore} |
522 |
523 |
523 The simplest combinator is @{ML I} which is just the identity function. |
524 The simplest combinator is @{ML I}, which is just the identity function. |
524 *} |
525 *} |
525 |
526 |
526 ML{*fun I x = x*} |
527 ML{*fun I x = x*} |
527 |
528 |
528 text {* Another simple combinator is @{ML K}, defined as *} |
529 text {* Another simple combinator is @{ML K}, defined as *} |
529 |
530 |
530 ML{*fun K x = fn _ => x*} |
531 ML{*fun K x = fn _ => x*} |
531 |
532 |
532 text {* |
533 text {* |
533 It ``wraps'' a function around the argument @{text "x"}. However, this |
534 @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this |
534 function ignores its argument. So @{ML K} defines a constant function |
535 function ignores its argument. So @{ML K} defines a constant function |
535 returning @{text x}. |
536 returning @{text x}. |
536 |
537 |
537 The next combinator is reverse application, @{ML "|>"}, defined as |
538 The next combinator is reverse application, @{ML "|>"}, defined as |
538 *} |
539 *} |
576 val y4 = y3 + 4 |
577 val y4 = y3 + 4 |
577 in y4 end*} |
578 in y4 end*} |
578 |
579 |
579 text {* |
580 text {* |
580 Another reason why the let-bindings in the code above are better to be |
581 Another reason why the let-bindings in the code above are better to be |
581 avoided: it is more than easy to get the intermediate values wrong! |
582 avoided: it is more than easy to get the intermediate values wrong, not to |
|
583 mention the nightmares the maintenance of this code causes! |
582 |
584 |
583 |
585 |
584 (FIXME: give a real world example involving theories) |
586 (FIXME: give a real world example involving theories) |
585 |
587 |
586 Similarly, the combinator @{ML "#>"} is the reverse function |
588 Similarly, the combinator @{ML "#>"} is the reverse function |
592 #> (fn x => x + 2) |
594 #> (fn x => x + 2) |
593 #> (fn x => x + 3)*} |
595 #> (fn x => x + 3)*} |
594 |
596 |
595 text {* |
597 text {* |
596 which is the function composed of first the increment-by-one function and then |
598 which is the function composed of first the increment-by-one function and then |
597 increment-by-two, followed by increment-by-three. |
599 increment-by-two, followed by increment-by-three. Again, the reverse function |
|
600 composition allows one to read the code top-down. |
598 |
601 |
599 The remaining combinators described in this section add convenience for the |
602 The remaining combinators described in this section add convenience for the |
600 ``waterfall method'' of writing functions. The combinator @{ML tap} allows |
603 ``waterfall method'' of writing functions. The combinator @{ML tap} allows |
601 one to get hold of an intermediate result (to do some side-calculations for |
604 one to get hold of an intermediate result (to do some side-calculations for |
602 instance). The function |
605 instance). The function |
606 ML %linenumbers{*fun inc_by_three x = |
609 ML %linenumbers{*fun inc_by_three x = |
607 x |> (fn x => x + 1) |
610 x |> (fn x => x + 1) |
608 |> tap (fn x => tracing (makestring x)) |
611 |> tap (fn x => tracing (makestring x)) |
609 |> (fn x => x + 2)*} |
612 |> (fn x => x + 2)*} |
610 |
613 |
611 text {* increments the argument first by one and then by two. In the middle, |
614 text {* increments the argument first by one and then by two. In the middle (Line 3), |
612 however, it uses @{ML tap} for printing the ``plus-one'' intermediate |
615 however, it uses @{ML tap} for printing the ``plus-one'' intermediate |
613 result inside the tracing buffer (Line 3). The function @{ML tap} can only |
616 result inside the tracing buffer. The function @{ML tap} can only |
614 be used for side-calculations, because any value that is computed cannot |
617 be used for side-calculations, because any value that is computed cannot |
615 be merged back into the ``main waterfall''. To do this, the next combinator |
618 be merged back into the ``main waterfall''. To do this, the next combinator |
616 can be used. |
619 can be used. |
617 |
620 |
618 The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value |
621 The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value |
659 |
662 |
660 text {* |
663 text {* |
661 Recall that @{ML "|>"} is the reverse function applications. The related |
664 Recall that @{ML "|>"} is the reverse function applications. The related |
662 reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"}, |
665 reverse function composition is @{ML "#>"}. In fact all combinators @{ML "|->"}, |
663 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function |
666 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function |
664 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. In this |
667 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "|->"}, |
665 way, the function @{text double} can also be written as |
668 the function @{text double} can also be written as |
666 *} |
669 *} |
667 |
670 |
668 ML{*val double = |
671 ML{*val double = |
669 (fn x => (x, x)) |
672 (fn x => (x, x)) |
670 #-> (fn x => fn y => x + y)*} |
673 #-> (fn x => fn y => x + y)*} |