(* Title: HOL/Library/Open_State_Syntax.thy Author: Florian Haftmann, TU Muenchen
*)
section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>
theory Open_State_Syntax imports Main begin
context includes state_combinator_syntax begin
subsection \<open>Motivation\<close>
text\<open>
The logic HOL has no notion of constructor classes, so it is not
possible to model monads the Haskell way in full genericity in
Isabelle/HOL.
However, this theory provides substantial support for a very common class of monads: \emph{state monads} (or \emph{single-threaded
monads}, since a state is transformed single-threadedly).
subsection \<open>State transformations and combinators\<close>
text\<open>
We classify functions operating on states into two categories:
\begin{description}
\item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>,
transforming a state.
\item[``yielding'' transformations] with type signature \<open>\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a
state.
\item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a
result dependent on a state.
\end{description}
By convention we write \<open>\<sigma>\<close> for types representing states and \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types
representing side results. Type changes due to transformations are
not excluded in our scenario.
We aim to assert that values of any state type \<open>\<sigma>\<close> are used in a single-threaded way: after application of a transformation on a value of type \<open>\<sigma>\<close>, the former value should not be used
again. To achieve this, we use a set of monad combinators: \<close>
text\<open>
Given two transformations \<^term>\<open>f\<close> and \<^term>\<open>g\<close>, they may be
directly composed using the \<^term>\<open>(\<circ>>)\<close> combinator, forming a
forward composition: \<^prop>\<open>(f \<circ>> g) s = f (g s)\<close>.
After any yielding transformation, we bind the side result
immediately using a lambda abstraction. This is the purpose of the \<^term>\<open>(\<circ>\<rightarrow>)\<close> combinator: \<^prop>\<open>(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
= f s in g s')\.
For queries, the existing \<^term>\<open>Let\<close> is appropriate.
Naturally, a computation may yield a side result by pairing it to
the state from the left; we introduce the suggestive abbreviation \<^term>\<open>return\<close> for this purpose.
The most crucial distinction to Haskell is that we do not need to
introduce distinguished type constructors for different kinds of
state. This has two consequences:
\begin{itemize}
\item The monad model does not state anything about the kind of
state; the model for the state is completely orthogonal and may
be specified completely independently.
\item There is no distinguished type constructor encapsulating
away the state transformation, i.e.~transformations may be
applied directly without using any lifting or providing and
dropping units (``open monad'').
\item The type of states may change due to a transformation.
\end{itemize} \<close>
subsection \<open>Monad laws\<close>
text\<open>
The common monadic laws hold and may also be used as normalization
rules for monadic expressions: \<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
