LiquidHaskell 入門 その3

前回の記事ではLiquidHaskellを用いて簡単な言語の評価機を作ってみました。 今回はそれをStateモナドを用いて書き直すために必要な新しい機能であるAbstarct Refinement, Bounded Refinmenetの解説をしていきたいと思います。

Abstract Refinement

LiquidHaskell入門その1で述べたように、LiquidHaskellでは量化子のない一階述語論理式を書くことができますが、それだけでは表現力が足りないケースが出てきます。 公式ブログにある例を引っ張ってみます。 次の関数maxIntを考えてみます。 

maxInt :: Int -> Int -> Int
maxInt = if x >= y then x else y
この関数のRefinement Typeとして、以下の全ての型は正しいです。 
maxInt :: Nat -> Nat -> Nat
maxInt :: {v: Int | v < 10} -> {v: Int | v < 10} -> {v: Int | v < 10}
maxInt : Even -> Even -> Even
しかしながら、型を一つ指定してしまうと、他の型としては扱えません。 
{-@ maxInt :: Nat -> Nat -> Nat @-}
{-@ test :: Even @-}
test :: Int
test = maxInt 0 2
$ stack exec -- liquid src/Liquid/AbstractRefinement.hs
...

**** RESULT: UNSAFE ************************************************************

/src/Liquid/AbstractRefienement.hs:126:1-18: Error: Liquid Type Mismatch

 126 | test = maxInt 2 0
       ^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : GHC.Types.Int | v >= 0}

   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV mod 2 == 0}
それではこの関数につけるべき正しい型は何でしょうか？ Abstrace Refinement*1は述語に対する全称量化を提供してくれます。 つまり、maxIntに対しては以下のような型を付けることができます。 
{-@ maxInt :: forall <p :: Int -> Bool>. Int<p> -> Int<p> -> Int<p> @-}
maxInt :: Int -> Int -> Int
maxInt x y = if x >= y then x else y
forall <p :: Int -> Bool>が全称量化された述語を導入しており、Int<p>は(感覚的には){v: Int | p v}と等価です。(実際に右の書き方をするとSort Errorと怒られます。) つまり、述語pを満たすInt型の値を2つ受け取って、pを満たすInt型の値を返すという型がmaxIntにはつきました。 実際に使ってみましょう。 本来ならばmaxIntを使うとき、述語を指定する必要がありそうですが、うまいこと推論してくれます。 
{-@ test2 :: Even @-}
test2 :: Int
test2 = maxInt 2 0
$ stack exec -- liquid src/Liquid/AbstractRefinement.hs
...

**** RESULT: SAFE **************************************************************
データ型の宣言にもAbstract Refinementが使えます。以下ではList型の宣言にAbstract Refinementを用いた例です。 テストでは述語としてすべての値が等しいというものを与えているので、testListUnSafeのみエラーを報告されています。 
{-@ 
data List a <p :: a -> a -> Bool> where
    Nil :: List <p> a
  | Cons :: h:a -> List <p> (a<p h>) -> List <p> a
@-}
data List a where
  Nil :: List a
  Cons :: a -> List a -> List a

{-@ testListSafe :: List <{\s t -> s == t}> Int @-}
testListSafe :: List Int
testListSafe = Cons 1 $ Cons 1 Nil

{-@ testListUnSafe :: List <{\s t -> s == t}> Int @-}
testListUnSafe :: List Int
testListUnSafe = Cons 2 $ Cons 1 Nil
$ stack exec -- liquid src/Liquid/AbstractRefinement.hs
...

**** RESULT: UNSAFE ************************************************************


 /src/Liquid/AbstractRefinement.hs:39:1-36: Error: Liquid Type Mismatch

 39 | testListUnSafe = Cons 2 $ Cons 1 Nil
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : GHC.Types.Int

   not a subtype of Required type
     VV : {VV : GHC.Types.Int | ?a == VV}

   In Context
     ?a : GHC.Types.Int

Bounded Refinement

有界量化や型クラスのように、全称量化を得たらそのドメインを制限して情報量を増やすような仕組みが欲しくなります。 述語に対する全称量化であったAbstract Refinementに対し、そのドメインを制限するのがBounded Refinement*2です。 早速具体例を見ていきましょう。 関数合成(.)は以下のように書けます。 引数として2つの関数f: (y:b -> c<p y>)、g: (z:a -> b<q z>)を受け取って新しい関数f . g: (a -> c<r x>)を返すのですが、rの条件として{x::a, w::b<q x> |- c<p w> <: c<r x>}という制限を与えています。 つまり、事後条件が連鎖していきます。 実際に使ってみましょう。 incrを2回適用する関数を合成したdoubleIncrは確かに検査されました。 

{-@
(.) :: forall < p :: b -> c -> Bool
              , q :: a -> b -> Bool
              , r :: a -> c -> Bool
              >.
       {x::a, w::b<q x> |- c<p w> <: c<r x>}
       f:(y:b -> c<p y>)
    -> g:(z:a -> b<q z>)
    -> x:a -> c<r x>
@-}
(.) f g x = f (g x)

-- example
{-@ incr :: x: Int -> {y: Int | y = x + 1} @-}
incr :: Int -> Int
incr = (+) 1

{-@ doubleIncr :: x: Int -> {y: Int | y = x + 2} @-}
doubleIncr = incr . incr

$ stack exec -- liquid src/Liquid/AbstractRefinement.hs
...

**** RESULT: SAFE **************************************************************

補足: 構文に関するいくつかの注意点

まとめ

今回はAbstract RefinementとBounded Refinementについて解説しました。 LiquidHaskellでは量化子のない一階述語論理式しか書けませんが、Abstract Refinementは述語の全称量化、Bounded Refinementは述語の有界量化を提供します。 これらによってLiquidHaskellの表現力が広がることを確認しました。

次回はこれらを用いてHoareモナドを実装し、前回の評価機をHoareモナドを用いてよりHaskellらしいコードに書き直します。

参考文献

comments powered by Disqus