src/Doc/Implementation/ML.thy

update for release;

theory "ML"
imports Base
begin

chapter {* Isabelle/ML *}

text {* Isabelle/ML is best understood as a certain culture based on
  Standard ML.  Thus it is not a new programming language, but a
  certain way to use SML at an advanced level within the Isabelle
  environment.  This covers a variety of aspects that are geared
  towards an efficient and robust platform for applications of formal
  logic with fully foundational proof construction --- according to
  the well-known \emph{LCF principle}.  There is specific
  infrastructure with library modules to address the needs of this
  difficult task.  For example, the raw parallel programming model of
  Poly/ML is presented as considerably more abstract concept of
  \emph{future values}, which is then used to augment the inference
  kernel, proof interpreter, and theory loader accordingly.

  The main aspects of Isabelle/ML are introduced below.  These
  first-hand explanations should help to understand how proper
  Isabelle/ML is to be read and written, and to get access to the
  wealth of experience that is expressed in the source text and its
  history of changes.\footnote{See
  @{url "http://isabelle.in.tum.de/repos/isabelle"} for the full
  Mercurial history.  There are symbolic tags to refer to official
  Isabelle releases, as opposed to arbitrary \emph{tip} versions that
  merely reflect snapshots that are never really up-to-date.}  *}


section {* Style and orthography *}

text {* The sources of Isabelle/Isar are optimized for
  \emph{readability} and \emph{maintainability}.  The main purpose is
  to tell an informed reader what is really going on and how things
  really work.  This is a non-trivial aim, but it is supported by a
  certain style of writing Isabelle/ML that has emerged from long
  years of system development.\footnote{See also the interesting style
  guide for OCaml
  @{url "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"}
  which shares many of our means and ends.}

  The main principle behind any coding style is \emph{consistency}.
  For a single author of a small program this merely means ``choose
  your style and stick to it''.  A complex project like Isabelle, with
  long years of development and different contributors, requires more
  standardization.  A coding style that is changed every few years or
  with every new contributor is no style at all, because consistency
  is quickly lost.  Global consistency is hard to achieve, though.
  Nonetheless, one should always strive at least for local consistency
  of modules and sub-systems, without deviating from some general
  principles how to write Isabelle/ML.

  In a sense, good coding style is like an \emph{orthography} for the
  sources: it helps to read quickly over the text and see through the
  main points, without getting distracted by accidental presentation
  of free-style code.
*}


subsection {* Header and sectioning *}

text {* Isabelle source files have a certain standardized header
  format (with precise spacing) that follows ancient traditions
  reaching back to the earliest versions of the system by Larry
  Paulson.  See @{file "~~/src/Pure/thm.ML"}, for example.

  The header includes at least @{verbatim Title} and @{verbatim
  Author} entries, followed by a prose description of the purpose of
  the module.  The latter can range from a single line to several
  paragraphs of explanations.

  The rest of the file is divided into sections, subsections,
  subsubsections, paragraphs etc.\ using a simple layout via ML
  comments as follows.

\begin{verbatim}
(*** section ***)

(** subsection **)

(* subsubsection *)

(*short paragraph*)

(*
  long paragraph,
  with more text
*)
\end{verbatim}

  As in regular typography, there is some extra space \emph{before}
  section headings that are adjacent to plain text (not other headings
  as in the example above).

  \medskip The precise wording of the prose text given in these
  headings is chosen carefully to introduce the main theme of the
  subsequent formal ML text.
*}


subsection {* Naming conventions *}

text {* Since ML is the primary medium to express the meaning of the
  source text, naming of ML entities requires special care.

  \paragraph{Notation.}  A name consists of 1--3 \emph{words} (rarely
  4, but not more) that are separated by underscore.  There are three
  variants concerning upper or lower case letters, which are used for
  certain ML categories as follows:

  \medskip
  \begin{tabular}{lll}
  variant & example & ML categories \\\hline
  lower-case & @{ML_text foo_bar} & values, types, record fields \\
  capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\
  upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\
  \end{tabular}
  \medskip

  For historical reasons, many capitalized names omit underscores,
  e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
  Genuine mixed-case names are \emph{not} used, because clear division
  of words is essential for readability.\footnote{Camel-case was
  invented to workaround the lack of underscore in some early
  non-ASCII character sets.  Later it became habitual in some language
  communities that are now strong in numbers.}

  A single (capital) character does not count as ``word'' in this
  respect: some Isabelle/ML names are suffixed by extra markers like
  this: @{ML_text foo_barT}.

  Name variants are produced by adding 1--3 primes, e.g.\ @{ML_text
  foo'}, @{ML_text foo''}, or @{ML_text foo'''}, but not @{ML_text
  foo''''} or more.  Decimal digits scale better to larger numbers,
  e.g.\ @{ML_text foo0}, @{ML_text foo1}, @{ML_text foo42}.

  \paragraph{Scopes.}  Apart from very basic library modules, ML
  structures are not ``opened'', but names are referenced with
  explicit qualification, as in @{ML Syntax.string_of_term} for
  example.  When devising names for structures and their components it
  is important aim at eye-catching compositions of both parts, because
  this is how they are seen in the sources and documentation.  For the
  same reasons, aliases of well-known library functions should be
  avoided.

  Local names of function abstraction or case/let bindings are
  typically shorter, sometimes using only rudiments of ``words'',
  while still avoiding cryptic shorthands.  An auxiliary function
  called @{ML_text helper}, @{ML_text aux}, or @{ML_text f} is
  considered bad style.

  Example:

  \begin{verbatim}
  (* RIGHT *)

  fun print_foo ctxt foo =
    let
      fun print t = ... Syntax.string_of_term ctxt t ...
    in ... end;


  (* RIGHT *)

  fun print_foo ctxt foo =
    let
      val string_of_term = Syntax.string_of_term ctxt;
      fun print t = ... string_of_term t ...
    in ... end;


  (* WRONG *)

  val string_of_term = Syntax.string_of_term;

  fun print_foo ctxt foo =
    let
      fun aux t = ... string_of_term ctxt t ...
    in ... end;

  \end{verbatim}


  \paragraph{Specific conventions.} Here are some specific name forms
  that occur frequently in the sources.

  \begin{itemize}

  \item A function that maps @{ML_text foo} to @{ML_text bar} is
  called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never
  @{ML_text foo2bar}, @{ML_text bar_from_foo}, @{ML_text
  bar_for_foo}, or @{ML_text bar4foo}).

  \item The name component @{ML_text legacy} means that the operation
  is about to be discontinued soon.

  \item The name component @{ML_text old} means that this is historic
  material that might disappear at some later stage.

  \item The name component @{ML_text global} means that this works
  with the background theory instead of the regular local context
  (\secref{sec:context}), sometimes for historical reasons, sometimes
  due a genuine lack of locality of the concept involved, sometimes as
  a fall-back for the lack of a proper context in the application
  code.  Whenever there is a non-global variant available, the
  application should be migrated to use it with a proper local
  context.

  \item Variables of the main context types of the Isabelle/Isar
  framework (\secref{sec:context} and \chref{ch:local-theory}) have
  firm naming conventions as follows:

  \begin{itemize}

  \item theories are called @{ML_text thy}, rarely @{ML_text theory}
  (never @{ML_text thry})

  \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text
  context} (never @{ML_text ctx})

  \item generic contexts are called @{ML_text context}, rarely
  @{ML_text ctxt}

  \item local theories are called @{ML_text lthy}, except for local
  theories that are treated as proof context (which is a semantic
  super-type)

  \end{itemize}

  Variations with primed or decimal numbers are always possible, as
  well as semantic prefixes like @{ML_text foo_thy} or @{ML_text
  bar_ctxt}, but the base conventions above need to be preserved.
  This allows to visualize the their data flow via plain regular
  expressions in the editor.

  \item The main logical entities (\secref{ch:logic}) have established
  naming convention as follows:

  \begin{itemize}

  \item sorts are called @{ML_text S}

  \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text
  ty} (never @{ML_text t})

  \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
  tm} (never @{ML_text trm})

  \item certified types are called @{ML_text cT}, rarely @{ML_text
  T}, with variants as for types

  \item certified terms are called @{ML_text ct}, rarely @{ML_text
  t}, with variants as for terms (never @{ML_text ctrm})

  \item theorems are called @{ML_text th}, or @{ML_text thm}

  \end{itemize}

  Proper semantic names override these conventions completely.  For
  example, the left-hand side of an equation (as a term) can be called
  @{ML_text lhs} (not @{ML_text lhs_tm}).  Or a term that is known
  to be a variable can be called @{ML_text v} or @{ML_text x}.

  \item Tactics (\secref{sec:tactics}) are sufficiently important to
  have specific naming conventions.  The name of a basic tactic
  definition always has a @{ML_text "_tac"} suffix, the subgoal index
  (if applicable) is always called @{ML_text i}, and the goal state
  (if made explicit) is usually called @{ML_text st} instead of the
  somewhat misleading @{ML_text thm}.  Any other arguments are given
  before the latter two, and the general context is given first.
  Example:

  \begin{verbatim}
  fun my_tac ctxt arg1 arg2 i st = ...
  \end{verbatim}

  Note that the goal state @{ML_text st} above is rarely made
  explicit, if tactic combinators (tacticals) are used as usual.

  \end{itemize}
*}


subsection {* General source layout *}

text {* The general Isabelle/ML source layout imitates regular
  type-setting to some extent, augmented by the requirements for
  deeply nested expressions that are commonplace in functional
  programming.

  \paragraph{Line length} is 80 characters according to ancient
  standards, but we allow as much as 100 characters (not
  more).\footnote{Readability requires to keep the beginning of a line
  in view while watching its end.  Modern wide-screen displays do not
  change the way how the human brain works.  Sources also need to be
  printable on plain paper with reasonable font-size.} The extra 20
  characters acknowledge the space requirements due to qualified
  library references in Isabelle/ML.

  \paragraph{White-space} is used to emphasize the structure of
  expressions, following mostly standard conventions for mathematical
  typesetting, as can be seen in plain {\TeX} or {\LaTeX}.  This
  defines positioning of spaces for parentheses, punctuation, and
  infixes as illustrated here:

  \begin{verbatim}
  val x = y + z * (a + b);
  val pair = (a, b);
  val record = {foo = 1, bar = 2};
  \end{verbatim}

  Lines are normally broken \emph{after} an infix operator or
  punctuation character.  For example:

  \begin{verbatim}
  val x =
    a +
    b +
    c;

  val tuple =
   (a,
    b,
    c);
  \end{verbatim}

  Some special infixes (e.g.\ @{ML_text "|>"}) work better at the
  start of the line, but punctuation is always at the end.

  Function application follows the tradition of @{text "\<lambda>"}-calculus,
  not informal mathematics.  For example: @{ML_text "f a b"} for a
  curried function, or @{ML_text "g (a, b)"} for a tupled function.
  Note that the space between @{ML_text g} and the pair @{ML_text
  "(a, b)"} follows the important principle of
  \emph{compositionality}: the layout of @{ML_text "g p"} does not
  change when @{ML_text "p"} is refined to the concrete pair
  @{ML_text "(a, b)"}.

  \paragraph{Indentation} uses plain spaces, never hard
  tabulators.\footnote{Tabulators were invented to move the carriage
  of a type-writer to certain predefined positions.  In software they
  could be used as a primitive run-length compression of consecutive
  spaces, but the precise result would depend on non-standardized
  editor configuration.}

  Each level of nesting is indented by 2 spaces, sometimes 1, very
  rarely 4, never 8 or any other odd number.

  Indentation follows a simple logical format that only depends on the
  nesting depth, not the accidental length of the text that initiates
  a level of nesting.  Example:

  \begin{verbatim}
  (* RIGHT *)

  if b then
    expr1_part1
    expr1_part2
  else
    expr2_part1
    expr2_part2


  (* WRONG *)

  if b then expr1_part1
            expr1_part2
  else expr2_part1
       expr2_part2
  \end{verbatim}

  The second form has many problems: it assumes a fixed-width font
  when viewing the sources, it uses more space on the line and thus
  makes it hard to observe its strict length limit (working against
  \emph{readability}), it requires extra editing to adapt the layout
  to changes of the initial text (working against
  \emph{maintainability}) etc.

  \medskip For similar reasons, any kind of two-dimensional or tabular
  layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
  avoided.

  \paragraph{Complex expressions} that consist of multi-clausal
  function definitions, @{ML_text handle}, @{ML_text case},
  @{ML_text let} (and combinations) require special attention.  The
  syntax of Standard ML is quite ambitious and admits a lot of
  variance that can distort the meaning of the text.

  Clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle},
  @{ML_text case} get extra indentation to indicate the nesting
  clearly.  Example:

  \begin{verbatim}
  (* RIGHT *)

  fun foo p1 =
        expr1
    | foo p2 =
        expr2


  (* WRONG *)

  fun foo p1 =
    expr1
    | foo p2 =
    expr2
  \end{verbatim}

  Body expressions consisting of @{ML_text case} or @{ML_text let}
  require care to maintain compositionality, to prevent loss of
  logical indentation where it is especially important to see the
  structure of the text.  Example:

  \begin{verbatim}
  (* RIGHT *)

  fun foo p1 =
        (case e of
          q1 => ...
        | q2 => ...)
    | foo p2 =
        let
          ...
        in
          ...
        end


  (* WRONG *)

  fun foo p1 = case e of
      q1 => ...
    | q2 => ...
    | foo p2 =
    let
      ...
    in
      ...
    end
  \end{verbatim}

  Extra parentheses around @{ML_text case} expressions are optional,
  but help to analyse the nesting based on character matching in the
  editor.

  \medskip There are two main exceptions to the overall principle of
  compositionality in the layout of complex expressions.

  \begin{enumerate}

  \item @{ML_text "if"} expressions are iterated as if there would be
  a multi-branch conditional in SML, e.g.

  \begin{verbatim}
  (* RIGHT *)

  if b1 then e1
  else if b2 then e2
  else e3
  \end{verbatim}

  \item @{ML_text fn} abstractions are often layed-out as if they
  would lack any structure by themselves.  This traditional form is
  motivated by the possibility to shift function arguments back and
  forth wrt.\ additional combinators.  Example:

  \begin{verbatim}
  (* RIGHT *)

  fun foo x y = fold (fn z =>
    expr)
  \end{verbatim}

  Here the visual appearance is that of three arguments @{ML_text x},
  @{ML_text y}, @{ML_text z}.

  \end{enumerate}

  Such weakly structured layout should be use with great care.  Here
  are some counter-examples involving @{ML_text let} expressions:

  \begin{verbatim}
  (* WRONG *)

  fun foo x = let
      val y = ...
    in ... end


  (* WRONG *)

  fun foo x = let
    val y = ...
  in ... end


  (* WRONG *)

  fun foo x =
  let
    val y = ...
  in ... end
  \end{verbatim}

  \medskip In general the source layout is meant to emphasize the
  structure of complex language expressions, not to pretend that SML
  had a completely different syntax (say that of Haskell or Java).
*}


section {* SML embedded into Isabelle/Isar *}

text {* ML and Isar are intertwined via an open-ended bootstrap
  process that provides more and more programming facilities and
  logical content in an alternating manner.  Bootstrapping starts from
  the raw environment of existing implementations of Standard ML
  (mainly Poly/ML, but also SML/NJ).

  Isabelle/Pure marks the point where the original ML toplevel is
  superseded by the Isar toplevel that maintains a uniform context for
  arbitrary ML values (see also \secref{sec:context}).  This formal
  environment holds ML compiler bindings, logical entities, and many
  other things.  Raw SML is never encountered again after the initial
  bootstrap of Isabelle/Pure.

  Object-logics like Isabelle/HOL are built within the
  Isabelle/ML/Isar environment by introducing suitable theories with
  associated ML modules, either inlined or as separate files.  Thus
  Isabelle/HOL is defined as a regular user-space application within
  the Isabelle framework.  Further add-on tools can be implemented in
  ML within the Isar context in the same manner: ML is part of the
  standard repertoire of Isabelle, and there is no distinction between
  ``user'' and ``developer'' in this respect.
*}


subsection {* Isar ML commands *}

text {* The primary Isar source language provides facilities to ``open
  a window'' to the underlying ML compiler.  Especially see the Isar
  commands @{command_ref "ML_file"} and @{command_ref "ML"}: both work the
  same way, only the source text is provided via a file vs.\ inlined,
  respectively.  Apart from embedding ML into the main theory
  definition like that, there are many more commands that refer to ML
  source, such as @{command_ref setup} or @{command_ref declaration}.
  Even more fine-grained embedding of ML into Isar is encountered in
  the proof method @{method_ref tactic}, which refines the pending
  goal state via a given expression of type @{ML_type tactic}.
*}

text %mlex {* The following artificial example demonstrates some ML
  toplevel declarations within the implicit Isar theory context.  This
  is regular functional programming without referring to logical
  entities yet.
*}

ML {*
  fun factorial 0 = 1
    | factorial n = n * factorial (n - 1)
*}

text {* Here the ML environment is already managed by Isabelle, i.e.\
  the @{ML factorial} function is not yet accessible in the preceding
  paragraph, nor in a different theory that is independent from the
  current one in the import hierarchy.

  Removing the above ML declaration from the source text will remove
  any trace of this definition as expected.  The Isabelle/ML toplevel
  environment is managed in a \emph{stateless} way: unlike the raw ML
  toplevel there are no global side-effects involved
  here.\footnote{Such a stateless compilation environment is also a
  prerequisite for robust parallel compilation within independent
  nodes of the implicit theory development graph.}

  \medskip The next example shows how to embed ML into Isar proofs, using
 @{command_ref "ML_prf"} instead of Instead of @{command_ref "ML"}.
  As illustrated below, the effect on the ML environment is local to
  the whole proof body, ignoring the block structure.
*}

notepad
begin
  ML_prf %"ML" {* val a = 1 *}
  {
    ML_prf %"ML" {* val b = a + 1 *}
  } -- {* Isar block structure ignored by ML environment *}
  ML_prf %"ML" {* val c = b + 1 *}
end

text {* By side-stepping the normal scoping rules for Isar proof
  blocks, embedded ML code can refer to the different contexts and
  manipulate corresponding entities, e.g.\ export a fact from a block
  context.

  \medskip Two further ML commands are useful in certain situations:
  @{command_ref ML_val} and @{command_ref ML_command} are
  \emph{diagnostic} in the sense that there is no effect on the
  underlying environment, and can thus used anywhere (even outside a
  theory).  The examples below produce long strings of digits by
  invoking @{ML factorial}: @{command ML_val} already takes care of
  printing the ML toplevel result, but @{command ML_command} is silent
  so we produce an explicit output message.  *}

ML_val {* factorial 100 *}
ML_command {* writeln (string_of_int (factorial 100)) *}

notepad
begin
  ML_val {* factorial 100 *}
  ML_command {* writeln (string_of_int (factorial 100)) *}
end


subsection {* Compile-time context *}

text {* Whenever the ML compiler is invoked within Isabelle/Isar, the
  formal context is passed as a thread-local reference variable.  Thus
  ML code may access the theory context during compilation, by reading
  or writing the (local) theory under construction.  Note that such
  direct access to the compile-time context is rare.  In practice it
  is typically done via some derived ML functions instead.
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
  @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
  @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
  @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML "ML_Context.the_generic_context ()"} refers to the theory
  context of the ML toplevel --- at compile time.  ML code needs to
  take care to refer to @{ML "ML_Context.the_generic_context ()"}
  correctly.  Recall that evaluation of a function body is delayed
  until actual run-time.

  \item @{ML "Context.>>"}~@{text f} applies context transformation
  @{text f} to the implicit context of the ML toplevel.

  \item @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of
  theorems produced in ML both in the (global) theory context and the
  ML toplevel, associating it with the provided name.  Theorems are
  put into a global ``standard'' format before being stored.

  \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to a
  singleton fact.

  \end{description}

  It is important to note that the above functions are really
  restricted to the compile time, even though the ML compiler is
  invoked at run-time.  The majority of ML code either uses static
  antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
  proof context at run-time, by explicit functional abstraction.
*}


subsection {* Antiquotations \label{sec:ML-antiq} *}

text {* A very important consequence of embedding SML into Isar is the
  concept of \emph{ML antiquotation}.  The standard token language of
  ML is augmented by special syntactic entities of the following form:

  @{rail \<open>
  @{syntax_def antiquote}: '@{' nameref args '}'
  \<close>}

  Here @{syntax nameref} and @{syntax args} are regular outer syntax
  categories \cite{isabelle-isar-ref}.  Attributes and proof methods
  use similar syntax.

  \medskip A regular antiquotation @{text "@{name args}"} processes
  its arguments by the usual means of the Isar source language, and
  produces corresponding ML source text, either as literal
  \emph{inline} text (e.g. @{text "@{term t}"}) or abstract
  \emph{value} (e.g. @{text "@{thm th}"}).  This pre-compilation
  scheme allows to refer to formal entities in a robust manner, with
  proper static scoping and with some degree of logical checking of
  small portions of the code.
*}


subsection {* Printing ML values *}

text {* The ML compiler knows about the structure of values according
  to their static type, and can print them in the manner of the
  toplevel loop, although the details are non-portable.  The
  antiquotations @{ML_antiquotation_def "make_string"} and
  @{ML_antiquotation_def "print"} provide a quasi-portable way to
  refer to this potential capability of the underlying ML system in
  generic Isabelle/ML sources.

  This is occasionally useful for diagnostic or demonstration
  purposes.  Note that production-quality tools require proper
  user-level error messages. *}

text %mlantiq {*
  \begin{matharray}{rcl}
  @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
  @{ML_antiquotation_def "print"} & : & @{text ML_antiquotation} \\
  \end{matharray}

  @{rail \<open>
  @@{ML_antiquotation make_string}
  ;
  @@{ML_antiquotation print} @{syntax name}?
  \<close>}

  \begin{description}

  \item @{text "@{make_string}"} inlines a function to print arbitrary
  values similar to the ML toplevel.  The result is compiler dependent
  and may fall back on "?" in certain situations.

  \item @{text "@{print f}"} uses the ML function @{text "f: string ->
  unit"} to output the result of @{text "@{make_string}"} above,
  together with the source position of the antiquotation.  The default
  output function is @{ML writeln}.

  \end{description}
*}

text %mlex {* The following artificial examples show how to produce
  adhoc output of ML values for debugging purposes. *}

ML {*
  val x = 42;
  val y = true;

  writeln (@{make_string} {x = x, y = y});

  @{print} {x = x, y = y};
  @{print tracing} {x = x, y = y};
*}


section {* Canonical argument order \label{sec:canonical-argument-order} *}

text {* Standard ML is a language in the tradition of @{text
  "\<lambda>"}-calculus and \emph{higher-order functional programming},
  similar to OCaml, Haskell, or Isabelle/Pure and HOL as logical
  languages.  Getting acquainted with the native style of representing
  functions in that setting can save a lot of extra boiler-plate of
  redundant shuffling of arguments, auxiliary abstractions etc.

  Functions are usually \emph{curried}: the idea of turning arguments
  of type @{text "\<tau>\<^sub>i"} (for @{text "i \<in> {1, \<dots> n}"}) into a result of
  type @{text "\<tau>"} is represented by the iterated function space
  @{text "\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>"}.  This is isomorphic to the well-known
  encoding via tuples @{text "\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>"}, but the curried
  version fits more smoothly into the basic calculus.\footnote{The
  difference is even more significant in higher-order logic, because
  the redundant tuple structure needs to be accommodated by formal
  reasoning.}

  Currying gives some flexibility due to \emph{partial application}.  A
  function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
  and the remaining @{text "(f x): \<tau>\<^sub>2 \<rightarrow> \<tau>"} passed to another function
  etc.  How well this works in practice depends on the order of
  arguments.  In the worst case, arguments are arranged erratically,
  and using a function in a certain situation always requires some
  glue code.  Thus we would get exponentially many opportunities to
  decorate the code with meaningless permutations of arguments.

  This can be avoided by \emph{canonical argument order}, which
  observes certain standard patterns and minimizes adhoc permutations
  in their application.  In Isabelle/ML, large portions of text can be
  written without auxiliary operations like @{text "swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times>
  \<alpha>"} or @{text "C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)"} (the latter not
  present in the Isabelle/ML library).

  \medskip The basic idea is that arguments that vary less are moved
  further to the left than those that vary more.  Two particularly
  important categories of functions are \emph{selectors} and
  \emph{updates}.

  The subsequent scheme is based on a hypothetical set-like container
  of type @{text "\<beta>"} that manages elements of type @{text "\<alpha>"}.  Both
  the names and types of the associated operations are canonical for
  Isabelle/ML.

  \begin{center}
  \begin{tabular}{ll}
  kind & canonical name and type \\\hline
  selector & @{text "member: \<beta> \<rightarrow> \<alpha> \<rightarrow> bool"} \\
  update & @{text "insert: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} \\
  \end{tabular}
  \end{center}

  Given a container @{text "B: \<beta>"}, the partially applied @{text
  "member B"} is a predicate over elements @{text "\<alpha> \<rightarrow> bool"}, and
  thus represents the intended denotation directly.  It is customary
  to pass the abstract predicate to further operations, not the
  concrete container.  The argument order makes it easy to use other
  combinators: @{text "forall (member B) list"} will check a list of
  elements for membership in @{text "B"} etc. Often the explicit
  @{text "list"} is pointless and can be contracted to @{text "forall
  (member B)"} to get directly a predicate again.

  In contrast, an update operation varies the container, so it moves
  to the right: @{text "insert a"} is a function @{text "\<beta> \<rightarrow> \<beta>"} to
  insert a value @{text "a"}.  These can be composed naturally as
  @{text "insert c \<circ> insert b \<circ> insert a"}.  The slightly awkward
  inversion of the composition order is due to conventional
  mathematical notation, which can be easily amended as explained
  below.
*}


subsection {* Forward application and composition *}

text {* Regular function application and infix notation works best for
  relatively deeply structured expressions, e.g.\ @{text "h (f x y + g
  z)"}.  The important special case of \emph{linear transformation}
  applies a cascade of functions @{text "f\<^sub>n (\<dots> (f\<^sub>1 x))"}.  This
  becomes hard to read and maintain if the functions are themselves
  given as complex expressions.  The notation can be significantly
  improved by introducing \emph{forward} versions of application and
  composition as follows:

  \medskip
  \begin{tabular}{lll}
  @{text "x |> f"} & @{text "\<equiv>"} & @{text "f x"} \\
  @{text "(f #> g) x"} & @{text "\<equiv>"} & @{text "x |> f |> g"} \\
  \end{tabular}
  \medskip

  This enables to write conveniently @{text "x |> f\<^sub>1 |> \<dots> |> f\<^sub>n"} or
  @{text "f\<^sub>1 #> \<dots> #> f\<^sub>n"} for its functional abstraction over @{text
  "x"}.

  \medskip There is an additional set of combinators to accommodate
  multiple results (via pairs) that are passed on as multiple
  arguments (via currying).

  \medskip
  \begin{tabular}{lll}
  @{text "(x, y) |-> f"} & @{text "\<equiv>"} & @{text "f x y"} \\
  @{text "(f #-> g) x"} & @{text "\<equiv>"} & @{text "x |> f |-> g"} \\
  \end{tabular}
  \medskip
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\
  @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
  @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
  @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
  \end{mldecls}
*}


subsection {* Canonical iteration *}

text {* As explained above, a function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be
  understood as update on a configuration of type @{text "\<beta>"},
  parametrized by arguments of type @{text "\<alpha>"}.  Given @{text "a: \<alpha>"}
  the partial application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates
  homogeneously on @{text "\<beta>"}.  This can be iterated naturally over a
  list of parameters @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \<dots> #> f a\<^sub>n"}.
  The latter expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}.
  It can be applied to an initial configuration @{text "b: \<beta>"} to
  start the iteration over the given list of arguments: each @{text
  "a"} in @{text "a\<^sub>1, \<dots>, a\<^sub>n"} is applied consecutively by updating a
  cumulative configuration.

  The @{text fold} combinator in Isabelle/ML lifts a function @{text
  "f"} as above to its iterated version over a list of arguments.
  Lifting can be repeated, e.g.\ @{text "(fold \<circ> fold) f"} iterates
  over a list of lists as expected.

  The variant @{text "fold_rev"} works inside-out over the list of
  arguments, such that @{text "fold_rev f \<equiv> fold f \<circ> rev"} holds.

  The @{text "fold_map"} combinator essentially performs @{text
  "fold"} and @{text "map"} simultaneously: each application of @{text
  "f"} produces an updated configuration together with a side-result;
  the iteration collects all such side-results as a separate list.
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
  @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
  @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML fold}~@{text f} lifts the parametrized update function
  @{text "f"} to a list of parameters.

  \item @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text
  "f"}, but works inside-out.

  \item @{ML fold_map}~@{text "f"} lifts the parametrized update
  function @{text "f"} (with side-result) to a list of parameters and
  cumulative side-results.

  \end{description}

  \begin{warn}
  The literature on functional programming provides a multitude of
  combinators called @{text "foldl"}, @{text "foldr"} etc.  SML97
  provides its own variations as @{ML List.foldl} and @{ML
  List.foldr}, while the classic Isabelle library also has the
  historic @{ML Library.foldl} and @{ML Library.foldr}.  To avoid
  unnecessary complication and confusion, all these historical
  versions should be ignored, and @{ML fold} (or @{ML fold_rev}) used
  exclusively.
  \end{warn}
*}

text %mlex {* The following example shows how to fill a text buffer
  incrementally by adding strings, either individually or from a given
  list.
*}

ML {*
  val s =
    Buffer.empty
    |> Buffer.add "digits: "
    |> fold (Buffer.add o string_of_int) (0 upto 9)
    |> Buffer.content;

  @{assert} (s = "digits: 0123456789");
*}

text {* Note how @{ML "fold (Buffer.add o string_of_int)"} above saves
  an extra @{ML "map"} over the given list.  This kind of peephole
  optimization reduces both the code size and the tree structures in
  memory (``deforestation''), but it requires some practice to read
  and write fluently.

  \medskip The next example elaborates the idea of canonical
  iteration, demonstrating fast accumulation of tree content using a
  text buffer.
*}

ML {*
  datatype tree = Text of string | Elem of string * tree list;

  fun slow_content (Text txt) = txt
    | slow_content (Elem (name, ts)) =
        "<" ^ name ^ ">" ^
        implode (map slow_content ts) ^
        "</" ^ name ^ ">"

  fun add_content (Text txt) = Buffer.add txt
    | add_content (Elem (name, ts)) =
        Buffer.add ("<" ^ name ^ ">") #>
        fold add_content ts #>
        Buffer.add ("</" ^ name ^ ">");

  fun fast_content tree =
    Buffer.empty |> add_content tree |> Buffer.content;
*}

text {* The slow part of @{ML slow_content} is the @{ML implode} of
  the recursive results, because it copies previously produced strings
  again.

  The incremental @{ML add_content} avoids this by operating on a
  buffer that is passed through in a linear fashion.  Using @{ML_text
  "#>"} and contraction over the actual buffer argument saves some
  additional boiler-plate.  Of course, the two @{ML "Buffer.add"}
  invocations with concatenated strings could have been split into
  smaller parts, but this would have obfuscated the source without
  making a big difference in allocations.  Here we have done some
  peephole-optimization for the sake of readability.

  Another benefit of @{ML add_content} is its ``open'' form as a
  function on buffers that can be continued in further linear
  transformations, folding etc.  Thus it is more compositional than
  the naive @{ML slow_content}.  As realistic example, compare the
  old-style @{ML "Term.maxidx_of_term: term -> int"} with the newer
  @{ML "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure.

  Note that @{ML fast_content} above is only defined as example.  In
  many practical situations, it is customary to provide the
  incremental @{ML add_content} only and leave the initialization and
  termination to the concrete application by the user.
*}


section {* Message output channels \label{sec:message-channels} *}

text {* Isabelle provides output channels for different kinds of
  messages: regular output, high-volume tracing information, warnings,
  and errors.

  Depending on the user interface involved, these messages may appear
  in different text styles or colours.  The standard output for
  terminal sessions prefixes each line of warnings by @{verbatim