summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/State_Monad.thy

author | krauss |

Tue Jul 13 11:50:22 2010 +0200 (2010-07-13) | |

changeset 37791 | 0d6b64060543 |

parent 37751 | 89e16802b6cc |

child 37817 | 71e5546b1965 |

permissions | -rw-r--r-- |

State_Monad uses Monad_Syntax

1 (* Title: HOL/Library/State_Monad.thy

2 Author: Florian Haftmann, TU Muenchen

3 *)

5 header {* Combinator syntax for generic, open state monads (single threaded monads) *}

7 theory State_Monad

8 imports Monad_Syntax

9 begin

11 subsection {* Motivation *}

13 text {*

14 The logic HOL has no notion of constructor classes, so

15 it is not possible to model monads the Haskell way

16 in full genericity in Isabelle/HOL.

18 However, this theory provides substantial support for

19 a very common class of monads: \emph{state monads}

20 (or \emph{single-threaded monads}, since a state

21 is transformed single-threaded).

23 To enter from the Haskell world,

24 \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}

25 makes a good motivating start. Here we just sketch briefly

26 how those monads enter the game of Isabelle/HOL.

27 *}

29 subsection {* State transformations and combinators *}

31 text {*

32 We classify functions operating on states into two categories:

34 \begin{description}

35 \item[transformations]

36 with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},

37 transforming a state.

38 \item[``yielding'' transformations]

39 with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},

40 ``yielding'' a side result while transforming a state.

41 \item[queries]

42 with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},

43 computing a result dependent on a state.

44 \end{description}

46 By convention we write @{text "\<sigma>"} for types representing states

47 and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}

48 for types representing side results. Type changes due

49 to transformations are not excluded in our scenario.

51 We aim to assert that values of any state type @{text "\<sigma>"}

52 are used in a single-threaded way: after application

53 of a transformation on a value of type @{text "\<sigma>"}, the

54 former value should not be used again. To achieve this,

55 we use a set of monad combinators:

56 *}

58 notation fcomp (infixl "\<circ>>" 60)

59 notation (xsymbols) fcomp (infixl "\<circ>>" 60)

60 notation scomp (infixl "o->" 60)

61 notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60)

63 abbreviation (input)

64 "return \<equiv> Pair"

66 text {*

67 Given two transformations @{term f} and @{term g}, they

68 may be directly composed using the @{term "op \<circ>>"} combinator,

69 forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.

71 After any yielding transformation, we bind the side result

72 immediately using a lambda abstraction. This

73 is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:

74 @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.

76 For queries, the existing @{term "Let"} is appropriate.

78 Naturally, a computation may yield a side result by pairing

79 it to the state from the left; we introduce the

80 suggestive abbreviation @{term return} for this purpose.

82 The most crucial distinction to Haskell is that we do

83 not need to introduce distinguished type constructors

84 for different kinds of state. This has two consequences:

85 \begin{itemize}

86 \item The monad model does not state anything about

87 the kind of state; the model for the state is

88 completely orthogonal and may be

89 specified completely independently.

90 \item There is no distinguished type constructor

91 encapsulating away the state transformation, i.e.~transformations

92 may be applied directly without using any lifting

93 or providing and dropping units (``open monad'').

94 \item The type of states may change due to a transformation.

95 \end{itemize}

96 *}

99 subsection {* Monad laws *}

101 text {*

102 The common monadic laws hold and may also be used

103 as normalization rules for monadic expressions:

104 *}

106 lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id

107 scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc

109 text {*

110 Evaluation of monadic expressions by force:

111 *}

113 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta

115 setup {*

116 Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}

117 *}

119 text {*

120 For an example, see HOL/Extraction/Higman.thy.

121 *}

123 end