LiquidHaskell 入門その2

March 29, 2019
Haskell
形式検証

前回の記事ではLiquidHaskellの基礎を学びました。今回はLiquidHaskellを用いて、とあるデータ型に対して、通常のHaskellの型の上に、実装者の暗黙の意図を反映したより細かい型をつけてみたいと思います。

スコープ付き環境

今回題材とするのはスコープ付きの言語の環境を表現する以下のようなデータ型です。データとしては、環境に対するこれまでの操作を記録するスタックと、idと値のリストを結びつけるマップEnvを持っています。操作ScopeOpとしては、スコープの開始を表すBeginと環境への値の挿入を表すPushがあります。この環境は各idに対して値のリストを持っており、同じ記号に対する値の挿入が起きるとリストの先頭に値を挿入します。スコープから出るときはスコープの開始前の環境に戻す必要があるのですが、これはスタックに積んだ操作を巻き戻すことによって実現します。このデータ型はTiger本から拝借しました。このデータ型をここではスコープ付き環境と呼ぶことにします。スコープ付き環境はスコープの概念のあるプログラミング言語のインタプリタでの変数の環境や、型検査時の型環境を表すことが可能です。 Tiger本ではTiger言語の型検査器の実装等に実際に用いられていました。

type Id = String
data ScopeOp = Begin | Push Id deriving (Eq, Show)
data Env a = Env { stack :: [ScopeOp], env :: Map.Map Id [a] } deriving (Eq, Show)

このデータ構造を操作する関数として以下のようなものがあります。 empty, insert, lookupは通常のマップと同様な関数です。ただし、insert時にはスタックにPush idを積むことで、このスコープ内でidに値が束縛されたということを記録します。マップ標準の関数に加えて、beginScopeとendScopeという特徴的な関数があります。これらは文字通りスコープの開始、終了を行う関数です。 beginScopeはスタックにBeginを積みます。 endScopeはスタックの操作をBeginまで巻き戻します。スタックの先頭がPush idならばマップからidのリストの先頭をpopし、リストが空になったらマップからidを消去します。スタックの先頭がBeginならば、それをスタックからpopして終了します。

empty :: Env a
empty = Env [] Map.empty
insert :: Id -> a -> Env a -> Env a
insert id a (Env s e) = Env { stack = Push id : s, env = Map.alter f id e }
  where
    f Nothing = Just [a]
    f (Just as) = Just (a:as)
lookup :: Id -> Env a -> Maybe a
lookup id (Env _ e) = case Map.lookup id e of
  Just (a:_) -> return a
  Nothing -> Nothing

beginScope :: Env a -> Env a
beginScope e = e { stack = Begin : stack e }
endScope :: Env a -> Env a
endScope (Env (Push id : rest) e) = endScope $ Env rest (Map.update pop id e)
  where
    pop [] = Nothing
    pop [_] = Nothing
    pop (_:as) = Just as
endScope (Env (Begin : rest) e) = Env rest e

実際に使ってみましょう。以下のテストコードを走らせます。 Stateモナドの状態にスコープ付き環境Env Intを与えています。

testEnv :: IO ()
testEnv = flip evalStateT empty $ do
  printState
  modify (insert "x" 10) >> printState
  modify beginScope      >> printState
  modify (insert "x" 12) >> printState
  modify endScope        >> printState
  where
    printState = get >>= lift . print

結果は以下のようになります。スコープから出るとスコープ内で挿入したx = 12が解放されていることが分かります。また、スタックに行った操作が記録され、endScopeが呼ばれるとBeginまで解放されていることも分かります。

$ stack ghci
...
*Main Env> testEnv
Env {stack = [], env = fromList []}
Env {stack = [Push "x"], env = fromList [("x",[10])]}
Env {stack = [Begin,Push "x"], env = fromList [("x",[10])]}
Env {stack = [Push "x",Begin,Push "x"], env = fromList [("x",[12, 10])]}
Env {stack = [Push "x"], env = fromList [("x",[10])]}

ところで先ほどのコードをコンパイルすると以下の警告が出ます。警告はWincomplete-patternsで、lookupに対してはidに束縛されたリストが空の場合、endScopeに対してはスタックが空の場合のパターンが足りていないようです。

/src/Env.hs:6:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: (Just [])
   |
12 | lookup id (Env _ e) = case Map.lookup id e of
   |                       ^^^^^^^^^^^^^^^^^^^^^^^...

/src/Env.hs:6:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for endScope: Patterns not matched: (Env [] _)
   |
19 | endScope (Env (Push id : rest) e)  = endScope $ Env rest (Map.update pop id e)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...

従って、これらの関数はMaybeモナドやEitherモナドに包んでエラーを表現するのがお行儀がよいです。しかしながら、これらは呼び出すときに以下のルールを定めることで、実際にはそのパターンにマッチすることはなく、問題にならないことが分かります。

idに束縛されている値のリストは空にならない
endScopeが呼ばれる前に必ずbeginScopeが呼ばれている。

1はendScope内で定義されているpop関数によって既に実現されています。リストが空になる時は環境から削除されるため、パターンマッチの時にリストが空になることはありません。 2は、例えば言語処理系などでこれを用いる場合、構文解析の時点で{}の数が合っていることが保証されていることが多いため妥当な仮定と言えるでしょう。余計なモナドで包むことを避けるために、これらのルールをLiquid Haskellを用いて型で表現してみます。

まず1を表現するために、Envの定義で値のリストの長さを0より大きいという型を与えてあげてみます。

{-@ data Env a = Env { stack :: [ScopeOp], env :: (Map Id { v: [a] | len v > 0 })} @-}
data Env a = Env { stack :: [ScopeOp], env :: Map.Map Id [a]} deriving (Eq, Show)

2を型で表現するためには、Envのスコープ数を表現することができるときれいに型がつきそうです。そこで、以下の補助関数を定義します。 beginNumはスタック内のBeginの数、つまり現在のスコープの深さを計算します。前回は説明していなかったのですが、measureとなる関数には停止性を保証しておく必要があるため、メトリクスを書いておきます。 scopeNumはEnvのスタックをに対してbeginNumを適用します。これでEnvのスコープ数を表現する準備が整いました。 NEEnvはスタックのスコープが空でないEnv、EnvNはスタックのスコープ数が第二引数NとなっているEnv、EnvXはスコープ数が第二引数のEnvと等しいEnvを表します。

{-@ measure beginNum @-}
{-@ beginNum :: s: [ScopeOp] -> Nat / [len s] @-}
beginNum :: [ScopeOp] -> Int
beginNum [] = 0
beginNum (Begin:xs) = 1 + beginNum xs
beginNum (_:xs) = beginNum xs
{-@ measure scopeNum @-}
{-@ scopeNum :: e: Env a -> {n: Nat | n == beginNum (stack e) } @-}
scopeNum :: Env a -> Int
scopeNum (Env s _) = beginNum s

{-@ type NEEnv a = {e: Env a | scopeNum e > 0} @-}
{-@ type EnvN a N = {e: Env a | scopeNum e = N} @-}
{-@ type EnvX a E = {e: Env a | scopeNum e = scopeNum E} @-}

これらを用いて先ほど定義した関数にさらに細かい型を与えてみます。 emptyはスコープが0のEnvを返す、insertはスコープの大きさを変えない、といったような型を与えることができました。 beginScopeはスコープの深さを1増やす、endScopeはスコープが空でないEnvを受け取ってスコープの深さを1減らす、といったような型を与えることができます。 endScopeには無限ループしないことを示すためにメトリックを与えています。スタックの長さは単調減少するので、無限ループしないことを示すためにはメトリックとしてスタックの長さ[len (stack e)]を与えてあげれば十分です。

{-@ empty :: EnvN a 0 @-}
empty :: Env a
empty = Env [] Map.empty
{-@ insert :: Id -> a -> e:Env a -> EnvN a {scopeNum e} @-}
insert :: Id -> a -> Env a -> Env a
insert id a (Env s e) = Env { stack = Push id : s, env = Map.alter f id e }
  where
    f Nothing = Just [a]
    f (Just as) = Just (a:as)
lookup :: Id -> Env a -> Maybe a
lookup id (Env _ e) = case Map.lookup id e of
  Just (a:_) -> return a
  Nothing -> Nothing

{-@ beginScope :: e: Env a -> EnvN a {1 + scopeNum e} @-}
beginScope :: Env a -> Env a
beginScope e = e { stack = Begin : stack e }
{-@ endScope :: e: NEEnv a -> EnvN a {scopeNum e - 1} / [len (stack e)] @-}
endScope :: Env a -> Env a
endScope (Env (Push id : rest) e) = endScope $ Env rest (Map.update pop id e)
  where
    pop [] = Nothing
    pop [_] = Nothing
    pop (_:as) = Just as
endScope (Env (Begin : rest) e) = Env rest e

これで先ほどの1,2のルールを表現することができました。実際にLiquidHaskellでコンパイルしてみましょう。今回はScopeOpでバリアント型を用いたため、オプション--exactdcを使う必要があります。ファイルの先頭に{-@ LIQUID "--exactdc" @-}を記述してもokです。

$ stack exec -- liquid src/Env.hs --exactdc
...
**** RESULT: SAFE **************************************************************

問題なさそうです。

実践: 評価関数

それでは先ほど作ったスコープ付き環境を用いて簡単な評価関数evalを実装してみます。対象とする言語は、Tiger本で扱われていたプログラミング言語Linearの算術式を制限したもので、構文は以下です。逐次実行、変数の割り当て、プリントができます。 ExpのEScope Stm Expはスコープを作る構文で、左のStmで定義した変数はそのスコープ内で有効で、右のExpを評価した値を返します。

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

これのevalを実装したものが以下です。 SPrintはによる副作用はIOモナドでもよいのですが、MonadWriterで代用します。未定義変数へのアクセスが起こりうるので、MonadErrorを与えます。簡単のため、停止性検査を無効にしておきます。

data EvalException = UndefinedVariableException deriving (Show)

{-@ lazy eval @-}
{-@ eval :: (MonadWriter [Int] m, MonadThrow m) => Stm -> e: Env Int -> m ((), EnvX Int e)  @-}
eval :: (MonadWriter [Int] m, MonadError EvalException m) => Stm -> Env Int -> m ((), Env Int)
eval (s1 `SSeq` s2) env0 = do
  (_, env1) <- eval s1 env0
  eval s2 env1
eval (x `SAssign` e) env0 = do
  (v, env1) <- evalExp e env0
  return ((), insert x v env1)
eval (SPrint es) env0 = (,) () <$> foldl f (pure env0) es
  where
    f m e = do
      (n, env') <- evalExp e =<< m
      tell [n]
      return env'

{-@ lazy evalExp @-}
{-@ evalExp :: (MonadWriter [Int] m, MonadThrow m) => Exp -> e: Env Int -> m (Int, EnvX Int e)  @-}
evalExp :: (MonadWriter [Int] m, MonadError EvalException m) => Exp -> Env Int -> m (Int, Env Int)
evalExp (EVar x) env0 = case lookup x env0 of
  Just v -> return (v, env0)
  Nothing -> throwError UndefinedVariableException
evalExp (EInt n) env0 = return (n, env0)
evalExp (e1 `EPlus` e2) env0 = do
  (v1, env1) <- evalExp e1 env0
  (v2, env2) <- evalExp e2 env1
  return (v1 + v2, env2)
evalExp (EScope s e) env0 = do
  let env1 = beginScope env0
  (_, env2) <- eval s env1
  (v, env3) <- evalExp e env2
  let env4 = endScope env3
  return (v, env4)

ここで重要なのは、evalExp内のEScopeのパターンマッチの部分です。 beginScopeとendScopeで挟んであります。例えば、ここのうちendScopeをコメントアウトすると、以下のようにちゃんとエラーを報告してくれます。

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


/src/Liquid/Env.hs:(111,29)-(116,18): Error: Liquid Type Mismatch

 111 | evalExp (EScope s e) env0 = do
 112 |   let env1 = beginScope env0
 113 |   (_, env2) <- eval s env1
 114 |   (v, env3) <- evalExp e env2
 115 |   -- let env4 = endScope env3
 116 |   return (v, env3)

   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 == Liquid.Env.scopeNum env0}

   In Context
     env0 : {env0 : (Liquid.Env.Env GHC.Types.Int) | Liquid.Env.scopeNum env0 >= 0}

それではLiquidHaskellでコンパイルしたうえで、正しく動いているかテストしてみましょう。以下のテスト関数を用意してください。読みにくいですが、a := 5 + 3; print [a, {a := 10, a}]のようなプログラムをテストをしています。

run :: Stm -> Either EvalException (((), Env Int), [Int])
run s = runWriterT $ eval s empty

{-@ ignore testEval @-}
testEval :: IO ()
testEval = print $ run s
  where
    s =        ("a" `SAssign` (EInt 5 `EPlus` EInt 3)) 
        `SSeq` SPrint [ EVar "a", 
                        EScope ("a" `SAssign` EInt 10) (EVar "a")]

実行結果は以下です。これはまた読みづらいですが、Envが終了時の環境で、一番右の[8, 10]がSPrintによる出力結果です。問題ないようです。

$ stack ghci
...
*Main Env> testEval
Right (((),Env {stack = [Push "a"], env = fromList [("a",[8])]}),[8,10])

まとめ

今回はスコープ付き環境というデータ型を題材にLiquidHaskellを用いてみました。その中で、通常のHaskellでは表現できない、実装者の意図している暗黙の仕様をRefinemet Typeを用いて表現することができ、それをLiquidHaskllを用いて検証することができました。さらに、検証された関数を用いて簡単な言語の評価関数の実装をしてみました。実際に誤ったコードを書いたときに型検査に失敗するところも確認し、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モナドの状態に対して事前条件・事後条件を設定したくなります。そしてこれが前回の記事の冒頭で触れたHoareモナドの正体となります。しかしながら、前回軽く触れたようにLiquidHaskellでは量化子のない述語論理式しか書けないため、そのままではHoareモナドが実装できません。ここでLiquidHaskellの発展的?な機能であるAbstract Refienement、Bounded Refinementを用いてHoareモナドを実装してみます。次回はAbstract Refinement、Bounded Refinementの解説をし、次々回でHoareモナドの実装をして上のコードを書き直してみます。

LiquidHaskell 入門 その2

スコープ付き環境

Refinement Typeをつけてみる

実践: 評価関数

まとめ

次(々)回予告

LiquidHaskell 入門その2