这并不是 monad 教学。

最近在用 Isabelle 写 spaceos 的一些验证，打算用 seL4/l4v 里的 StateMonad 简化代码。

seL4 这帮人写了一堆各种各样的 StateMonad ，然后还做了一套类似于命令式编程的 syntax，有点像 Haskell 里的 do。并且为这个 StateMonad 做了一套证明方法、一些lemma，高科技无人驾驶。虽然看起来挺好用的，但是他们也只是自己用用，没具体写文档教咋用… 注释里各种 from Haskell-Like sth。没办法，还是老老实实补一下 Haskell。

粗略过了一下 Haskell，很多地方和 Isabelle 还是比较像的，比如 class、科里化参数、infix等(感觉 Isabelle 就像是有一堆毛病的升级版 Haskell)。依次过一下 Functor，applicative 函子，monoid，monad。这里不扯 IO 什么的，感觉并没有啥太大的关系。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
class Functor f where
	fmap :: (a->b) -> f a -> f b
	(<$) :: a -> f b -> f a

class (Functor f) => (Applicative f) where
	pure :: a -> f a
	(<*>) :: f (a -> b) -> f a -> f b

class Monoid m where
	mempty :: m
	mappend :: m -> m -> m
	mconcat :: [m] -> m
	mconcat = foldr mappend mempty

class Monad m where
	(>>=)  :: m a -> (  a -> m b) -> m b
	(>>)   :: m a ->  m b         -> m b
	return ::   a                 -> m a
	fail   :: String -> m a

需要满足一些 Laws:

Functor Laws:

1
2
fmap id = id
fmap (f . g)  ==  fmap f . fmap g

Applicative functor laws:

1
2
3
4
pure id <*> v = v
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
pure f <*> pure x = pure (f x)
u <*> pure y = pure ($ y) <*> u

Monoid Laws:

1
2
3
mempty `mappend` x = x
x `mappend` mempty = x
(x `mappend` y) `mappend` z = x `mappend` (y `mappend` z)

Monad Laws:

1
2
3
return x >>= f = f x
m >>= return = m
(m >>= f) >>= g = m >>= (\x -> f x >>= g)

以上，估计我也没有完全理解。下面看一下 Isabelle/HOL 的 State_Monad 和 seL4/l4v 的 NonDetMonad。

State_Monad:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
datatype ('s, 'a) state = State (run_state: "'s ⇒ ('a × 's)")

qualified definition return :: "'a ⇒ ('s, 'a) state" where
"return a = State (Pair a)"

qualified definition ap :: "('s, 'a ⇒ 'b) state ⇒ ('s, 'a) state ⇒ ('s, 'b) state" where
"ap f x = State (λs. case run_state f s of (g, s') ⇒ case run_state x s' of (y, s'') ⇒ (g y, s''))"

qualified definition bind :: "('s, 'a) state ⇒ ('a ⇒ ('s, 'b) state) ⇒ ('s, 'b) state" where
"bind x f = State (λs. case run_state x s of (a, s') ⇒ run_state (f a) s')"

lemma run_state_return[simp]: "run_state (return x) s = (x, s)"
unfolding return_def
by simp

adhoc_overloading Monad_Syntax.bind bind

lemma bind_left_identity[simp]: "bind (return a) f = f a"
unfolding return_def bind_def by simp

lemma bind_right_identity[simp]: "bind m return = m"
unfolding return_def bind_def by simp

lemma bind_assoc[simp]: "bind (bind m f) g = bind m (λx. bind (f x) g)"
unfolding bind_def by (auto split: prod.splits)

NonDetMonad

1
type_synonym ('s,'a) nondet_monad = "'s \<Rightarrow> ('a \<times> 's) set \<times> bool"

HOL 里的 State Monad 和 Haskell 里的是同一个东西，l4v 里的 NonDetMonad 把 $’s \rightarrow (‘s, ‘a)$ 换成了 $’s \rightarrow (‘s, ‘ a) set \times bool$ 。其实 NonDetMonad 描述了非确定性，一个状态执行之后包含一系列结果和后续状态以及一个 bool Flag，这个 Flag 指示后续路径里是否存在执行失败的可能。贴一段注释：

text {
The basic type of the nondeterministic state monad with failure is
very similar to the normal state monad. Instead of a pair consisting
of result and new state, we return a set of these pairs coupled with
a failure flag. Each element in the set is a potential result of the
computation. The flag is @{const True} if there is an execution path
in the computation that may have failed. Conversely, if the flag is
@{const False}, none of the computations resulting in the returned
set can have failed. }

以上，先说到这里