LiquidHaskell 入門その4

April 29, 2019
Haskell
形式検証

前回の記事はLiquidHaskellの表現力を高める機能であるAbstract RefinementとBounded Refinementの解説をしました。今回は前々回のナイーブなコードをHoareモナドを用いてHaskellらしいコードに書き直してみます。 Abstract RefinementとBounded Refinementをガンガン使っていきます。

今回書いたコードはgistに公開しています。

LiquidHaskellとStateモナド

LiquidHaskellによってスコープ付き環境とそれらの関数に対してより細かい型をつけ、実際に誤った使い方をしたときに型検査に失敗するところまで確認しました。 LiquidHaskellは確かに有用であることが分かりました。しかし、前々回のコードを見たHaskellerのみなさんはもどかしい気持ちになったのではないでしょうか。 evalの型をもう一度見直してみましょう。

eval :: (MonadWriter [Int] m, MonadError EvalException m) => Stm -> Env Int -> m ((), Env Int)
evalExp :: (MonadWriter [Int] m, MonadError EvalException m) => Exp -> Env Int -> m (Int, Env Int)

この型はStateモナドですので、本来なら以下のように書きたいです。

eval :: (MonadWriter [Int] m, MonadError EvalException m) => Stm -> StateT (Env Int) m ()
evalExp :: (MonadWriter [Int] m, MonadError EvalException m) => Exp -> StateT (Env Int) m Int

しかしながらそのままStateモナドを用いると、状態の事前条件と事後条件について何も言えません。実際にendScopeを呼んでみると、型検査に失敗します。 endScopeを呼ぶための事前条件を状態が満たしていることを保証できないためです。

eval' :: (MonadWriter [Int] m, MonadError EvalException m) => Stm -> StateT (Env Int) m ()
...

evalExp' :: (MonadWriter [Int] m, MonadError EvalException m) => Exp -> StateT (Env Int) m Int
...
evalExp' (EScope s e) = do
  modify beginScope
  eval' s
  v <- evalExp' e
  modify endScope
  return v

$ stack exec -- liquid src/Liquid/Env.hs
...
**** RESULT: UNSAFE ************************************************************


/src/Liquid/Env.hs:154:3-17: Error: Liquid Type Mismatch

 154 |   modify endScope
         ^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : (Liquid.Env.Env GHC.Types.Int) | Liquid.Env.scopeNum v >= 0}

   not a subtype of Required type
     VV : {VV : (Liquid.Env.Env GHC.Types.Int) | Liquid.Env.scopeNum VV > 0}

Hoareモナド

Stateモナドに事前条件と事後条件をつけたようなものはNanevskiらのHoareモナド*1として知られています。 LiquidHaskell上で実装すると以下のようになります。前回解説したAbstract Refinementを用いています。通常のStateモナドに2つの述語パラメータp :: s -> Bool、q :: a -> s -> s -> Boolを加えています。 p :: s -> Boolが状態の事前条件、q :: a -> s -> s -> Boolが事後条件を指定しています。事後の状態s<q x v>は事前の状態v: s<p>と返り値x::aに依存しているため、事前の状態に対する相対的な条件も指定することが可能です。例えば、v' = v + 1みたいな条件を書くことができます。

{-@ data Hoare s a <p :: s -> Bool, q :: a -> s -> s -> Bool> = Hoare (v: s<p> -> (x::a, s<q x v>)) @-}
data Hoare s a = Hoare (s -> (a, s))

Stateモナド周りの関数に対するRefinement Typeは以下のようになります。 runHoareはStateモナドの中身を抽出、putは状態を引数と同じにする、getは状態をそのままに状態を返すという条件を表しています。 modifyは状態に対して引数fを適用し、事前条件・事後条件をfと同じものにするという条件を表しています。 returnは状態を変更せず、返り値を引数にするという条件を表しています。 (>>=)は少し大変です。 p :: s -> Bool、q :: a -> s -> s -> Boolは通常のHoareモナドのパラメータです。 pp :: a -> s -> Boolは第二引数の事前条件に関するパラメータなのですが、第一引数の返り値に依存することができます。 qq :: b -> s -> s -> Boolは通常の事後条件に関するパラメータです。また、Bounded Refinementを用いて述語パラメータに制限を加えています。 Bounded Refinementの制約は2つ以上書くことができます。 1つ目の制約は第一引数の事後条件が第二引数の事前条件を満たすことを表しています。 2つ目の制約は第二引数の事後条件が最終的な事後条件を満たすことを表しています。

{-@ runHoare :: forall <p :: s -> Bool, q :: a -> s -> s -> Bool>. Hoare <p, q> s a -> v:s<p> -> (x::a, s<q x v>) @-}
runHoare :: Hoare s a -> s -> (a, s)
runHoare (Hoare f) = f

{-@ put :: forall <p :: s -> Bool>. v:s -> Hoare <p, {\x s t -> v == t}> s () @-}
put :: s -> Hoare s ()
put s = Hoare (const ((), s))

{-@ get :: forall <p :: s -> Bool>. Hoare <p, {\x s t -> x == t && s == t}> s s @-}
get :: Hoare s s
get = Hoare (\s -> (s, s))

{-@ modify :: forall <p :: s -> Bool
                    , q :: s -> s -> Bool>. 
                 (x: s<p> -> {v: s<q x> | true }) 
              -> Hoare <p, \_ t -> { v: s<q t> | true }> s () @-}
modify :: (s -> s) -> Hoare s ()
modify f = Hoare (\s -> ((), f s))

{-@ return :: forall <p :: s -> Bool>. y:a -> Hoare <p, {\x s t -> x == y && s == t}> s a @-}
return :: a -> Hoare s a
return a = Hoare (\s -> (a, s))

{-@ 
(>>=) :: forall < p  :: s -> Bool
                , q  :: a -> s -> s -> Bool
                , pp :: a -> s -> Bool
                , qq :: b -> s -> s -> Bool
                , r  :: b -> s -> s -> Bool>. 
            {x::a, ss::s<p> |- s<q x ss> <: s<pp x>}
            {x::a, y::b, ss::s<p>, sss::s<q x ss> |- s<qq y sss> <: s<r y ss>}
            Hoare <p, q> s a
         -> (x:a -> Hoare <{ v: s<pp x> | true }, qq> s b)
         -> Hoare <p, r> s b
@-}
(>>=) :: Hoare s a -> (a -> Hoare s b) -> Hoare s b
m >>= k = Hoare (\s -> let (a, s') = runHoare m s in runHoare (k a) s')

evalのHoareモナドを用いたリファクタリング

それでは第二回のevalをHoareモナドを用いて書き直していきます。 monad transformerには適用ができなかったため、SPrintを削ったり、未定義の変数に対してはundefinedを返してサボっています。現状型クラスへの抽象化とも相性が悪いみたいです。 Monad型クラスのインスタンスにしてdo構文を使うと、せっかく定義したRefinement Typeを使えなくなってしまいます。(おそらくMonad型クラスの(>>=)のRefinement Typeを参照してしまっているためです。) いくつかの難点はあるものの、Hoareモナドによって状態を隠ぺいしたコードに書き直すことに成功しました。

data Stm = SSeq Stm Stm
         | SAssign Id Exp
data Exp = EVar Id
         | EInt Int
         | EPlus Exp Exp
         | EScope Stm Exp

{-@ lazy eval @-}
{-@ eval :: forall <p :: Env Int -> Bool>. Stm -> Hoare <p, {\_ e0 e1 -> scopeNum e0 == scopeNum e1}> (Env Int) ()  @-}
eval :: Stm -> Hoare (Env Int) ()
eval (s1 `SSeq` s2) = eval s1 >>= \_ -> eval s2
eval (x `SAssign` e) =
  evalExp e >>= \v ->
  modify (insert x v)

{-@ evalExp :: forall <p :: Env Int -> Bool>. Exp -> Hoare <p, {\_ e0 e1 -> scopeNum e0 == scopeNum e1}> (Env Int) Int @-}
evalExp :: Exp -> Hoare (Env Int) Int
evalExp (EVar x) =
  get >>= \e ->
  case lookup x e of
    Just v -> return v
    Nothing -> undefined
evalExp (EInt n) = return n
evalExp (e1 `EPlus` e2) = 
  evalExp e1 >>= \v1 ->
  evalExp e2 >>= \v2 ->
  return (v1 + v2)
evalExp (EScope s e) =
  modify beginScope >>= \_ ->
  eval s            >>= \_ ->
  evalExp e         >>= \v ->
  modify endScope   >>= \_ ->
  return v

最後にテストをしてみます。以下のテスト関数はa := 5; b := ({a := 10}; a); c := aというプログラムをテストしています。

run :: Stm -> ((), Env Int)
run s = runHoare (eval s) empty

{-@ ignore testEval @-}
testEval :: IO ()
testEval = print $ run s
  where
    -- a := 5; b := ({a := 10}; a); c := a
    s =        ("a" `SAssign` EInt 5) 
        `SSeq` ("b" `SAssign` EScope ("a" `SAssign` EInt 10) (EVar "a")) 
        `SSeq` ("c" `SAssign` EVar "a")

実行結果は以下です。ちゃんとスコープを外れるとaへの束縛がもとに戻っていることが確認できます。

$ stack ghci
...
*Liquid.Hoare> testEval
((),Env {stack = [Push "c",Push "b",Push "a"], env = fromList [("a",[5]),("b",[10]),("c",[5])]})

補足: Hoareモナドの圏論的定義

Hoareモナドの実装はStateモナドにパラメータを付加したようなものになっていますが、そのせいでどういうモナドなのか直感的には分かりにくいと思います。(僕には分かりませんでした。) そのため、気になる人のためにHoareモナドの圏論的定義を確認します。 Jacobs*2によると、Hoareモナドは圏論的には以下のように定義されます。簡単のためベースとなるモナドをIdentityモナドで固定します。

これらがモナド則を満たすことは読者への演習問題とする(言ってみたかっただけ)。直感的には、$\mathcal{H}X$は状態の事前条件、計算、事後条件の3つ組で、事前条件を満たしている上で計算をすると事後条件を満たすものたちの集合です。事後条件$Q$は計算前の状態との相対的な条件を記述できるよう、$Q \subseteq S \times S \times X$となっています。例えば、v' = v + 1のような条件を書くことができます。 $f^*(P, h, Q)$の事前条件は、$P(s)$が成り立っていて、かつ$Q(s, s', x)$が成り立つならば$f(x)$の事前条件が成り立つというものです。計算部分は状態モナドと同じです。事後条件は、$Q$と$post(f(x))$を繋げる$s'$が存在するというものです。上で用いた実装では、$P$、$Q$が述語パラメータとなっていました。

まとめ

今回はLiquidHaskellでHoareモナドを扱いました。 HoareモナドはStateモナドの状態に対して事前・事後条件を追加したものであることを見ました。これによって前々回の実装したevalをHoareモナドによってHaskellらしいコードに書き直すことに成功しました。また、前回説明したAbstract, Bounded Refinementをふんだんに使うことで、それらの具体例を補いました。

当初の予定通り、Hoareモナドまで終わったので、今回でLiquidHaskell入門の連載を終わりにしたいと思います。ここまで見ていただきありがとうございました。

LiquidHaskell 入門 その4

LiquidHaskellとStateモナド

Hoareモナド

evalのHoareモナドを用いたリファクタリング

補足: Hoareモナドの圏論的定義

まとめ

参考文献

LiquidHaskell 入門その4