483 Subsequently we give a brief overview of important operations on |
483 Subsequently we give a brief overview of important operations on |
484 basic ML data types. |
484 basic ML data types. |
485 *} |
485 *} |
486 |
486 |
487 |
487 |
|
488 subsection {* Characters *} |
|
489 |
|
490 text %mlref {* |
|
491 \begin{mldecls} |
|
492 @{index_ML_type char} \\ |
|
493 \end{mldecls} |
|
494 |
|
495 \begin{description} |
|
496 |
|
497 \item @{ML_type char} is not used. The smallest textual unit in |
|
498 Isabelle is a ``symbol'' (see \secref{sec:symbols}). |
|
499 |
|
500 \end{description} |
|
501 *} |
|
502 |
|
503 |
488 subsection {* Integers *} |
504 subsection {* Integers *} |
489 |
505 |
490 text %mlref {* |
506 text %mlref {* |
491 \begin{mldecls} |
507 \begin{mldecls} |
492 @{index_ML_type int} \\ |
508 @{index_ML_type int} \\ |
493 \end{mldecls} |
509 \end{mldecls} |
494 |
510 |
495 \begin{description} |
511 \begin{description} |
496 |
512 |
497 \item @{ML_type int} always represents regular mathematical |
513 \item @{ML_type int} represents regular mathematical integers, which |
498 integers, which are \emph{unbounded}. Overflow never happens in |
514 are \emph{unbounded}. Overflow never happens in |
499 practice.\footnote{The size limit for integer bit patterns in memory |
515 practice.\footnote{The size limit for integer bit patterns in memory |
500 is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.} |
516 is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.} |
501 This works uniformly for all supported ML platforms (Poly/ML and |
517 This works uniformly for all supported ML platforms (Poly/ML and |
502 SML/NJ). |
518 SML/NJ). |
503 |
519 |
532 structure @{ML_struct Option} are alien to Isabelle/ML. The |
548 structure @{ML_struct Option} are alien to Isabelle/ML. The |
533 operations shown above are defined in @{"file" |
549 operations shown above are defined in @{"file" |
534 "~~/src/Pure/General/basics.ML"}, among others. *} |
550 "~~/src/Pure/General/basics.ML"}, among others. *} |
535 |
551 |
536 |
552 |
|
553 subsection {* Lists *} |
|
554 |
|
555 text {* Lists are ubiquitous in ML as simple and light-weight |
|
556 ``collections'' for many everyday programming tasks. Isabelle/ML |
|
557 provides some important refinements over the predefined operations |
|
558 in SML97. *} |
|
559 |
|
560 text %mlref {* |
|
561 \begin{mldecls} |
|
562 @{index_ML cons: "'a -> 'a list -> 'a list"} \\ |
|
563 \end{mldecls} |
|
564 |
|
565 \begin{description} |
|
566 |
|
567 \item @{ML cons}~@{text "x xs"} evaluates to @{text "x :: xs"}. |
|
568 |
|
569 Tupled infix operators are a historical accident in Standard ML. |
|
570 The curried @{ML cons} amends this, but it should be only used when |
|
571 partial application is required. |
|
572 |
|
573 \end{description} |
|
574 *} |
|
575 |
|
576 |
|
577 subsubsection {* Canonical iteration *} |
|
578 |
|
579 text {* A function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be understood as update |
|
580 on a configuration of type @{text "\<beta>"} that is parametrized by |
|
581 arguments of type @{text "\<alpha>"}. Given @{text "a: \<alpha>"} the partial |
|
582 application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates homogeneously on @{text |
|
583 "\<beta>"}. This can be iterated naturally over a list of parameters |
|
584 @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1; \<dots>; f a\<^bsub>n\<^esub>\<^bsub>\<^esub>"} (where the |
|
585 semicolon represents left-to-right composition). The latter |
|
586 expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}. It can be applied |
|
587 to an initial configuration @{text "b: \<beta>"} to start the iteration |
|
588 over the given list of arguments: each @{text "a"} in @{text "a\<^sub>1, \<dots>, |
|
589 a\<^sub>n"} is applied consecutively by updating a cumulative |
|
590 configuration. |
|
591 |
|
592 The @{text fold} combinator in Isabelle/ML lifts a function @{text |
|
593 "f"} as above to its iterated version over a list of arguments. |
|
594 Lifting can be repeated, e.g.\ @{text "(fold \<circ> fold) f"} iterates |
|
595 over a list of lists as expected. |
|
596 |
|
597 The variant @{text "fold_rev"} works inside-out over the list of |
|
598 arguments, such that @{text "fold_rev f \<equiv> fold f \<circ> rev"} holds. |
|
599 |
|
600 The @{text "fold_map"} combinator essentially performs @{text |
|
601 "fold"} and @{text "map"} simultaneously: each application of @{text |
|
602 "f"} produces an updated configuration together with a side-result; |
|
603 the iteration collects all such side-results as a separate list. |
|
604 *} |
|
605 |
|
606 text %mlref {* |
|
607 \begin{mldecls} |
|
608 @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ |
|
609 @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ |
|
610 @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\ |
|
611 \end{mldecls} |
|
612 |
|
613 \begin{description} |
|
614 |
|
615 \item @{ML fold}~@{text f} lifts the parametrized update function |
|
616 @{text "f"} to a list of parameters. |
|
617 |
|
618 \item @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text |
|
619 "f"}, but works inside-out. |
|
620 |
|
621 \item @{ML fold_map}~@{text "f"} lifts the parametrized update |
|
622 function @{text "f"} (with side-result) to a list of parameters and |
|
623 cumulative side-results. |
|
624 |
|
625 \end{description} |
|
626 |
|
627 \begin{warn} |
|
628 The literature on functional programming provides a multitude of |
|
629 combinators called @{text "foldl"}, @{text "foldr"} etc. SML97 |
|
630 provides its own variations as @{ML List.foldl} and @{ML |
|
631 List.foldr}, while the classic Isabelle library still has the |
|
632 slightly more convenient historic @{ML Library.foldl} and @{ML |
|
633 Library.foldr}. To avoid further confusion, all of this should be |
|
634 ignored, and @{ML fold} (or @{ML fold_rev}) used exclusively. |
|
635 \end{warn} |
|
636 *} |
|
637 |
|
638 text %mlex {* Using canonical @{ML fold} together with canonical @{ML |
|
639 cons}, or similar standard operations, alternates the orientation of |
|
640 data. The is quite natural and should not altered forcible by |
|
641 inserting extra applications @{ML rev}. The alternative @{ML |
|
642 fold_rev} can be used in the relatively few situations, where |
|
643 alternation should be prevented. |
|
644 *} |
|
645 |
|
646 ML {* |
|
647 val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]; |
|
648 |
|
649 val list1 = fold cons items []; |
|
650 val list2 = fold_rev cons items []; |
|
651 *} |
|
652 |
|
653 |
537 subsection {* Unsynchronized references *} |
654 subsection {* Unsynchronized references *} |
538 |
655 |
539 text %mlref {* |
656 text %mlref {* |
540 \begin{mldecls} |
657 \begin{mldecls} |
541 @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\ |
658 @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\ |