3

レイジー キューに関するLiquidHaskell ケース スタディの最初の演習を実行しようとしています。

module Main where

main :: IO ()
main = putStrLn "hello"

{-@ type Nat   = {v:Int | 0 <= v}        @-}

{-@ die :: {v:String | false} -> a @-}
die x = error x

{-@ measure realSize @-}
realSize      :: [a] -> Int
realSize []     = 0
realSize (_:xs) = 1 + realSize xs

{-@ data SList a = SL {
       size  :: Nat 
     , elems :: {v:[a] | realSize v = size}
     }
  @-}
data SList a = SL { size :: Int, elems :: [a]}

{-@ type NEList a = {v:SList a | 0 < size v} @-}

{-@ hd           :: NEList a -> a @-}
hd (SL _ (x:_))  = x 
hd _             = die "empty SList"

okList = SL 1 ["cat"]
okHd   = hd okList

okHd失敗します:

 app/Main.hs:30:13-18: Error: Liquid Type Mismatch
   Inferred type
     VV : {VV : (SList [Char]) | VV == Main.okList}

   not a subtype of Required type
     VV : {VV : (SList [Char]) | 0 < size VV}

   In Context
     VV : {VV : (SList [Char]) | VV == Main.okList}
     Main.okList
        : (SList [Char])

okListエラー メッセージから、LHが空でないことを「認識」するのに十分な情報を LH に提供していないことは確かですが、それを修正する方法がわかりません。

事後条件(?)で明示的に伝えてみました:

{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]

しかし、これはうまくいきません:

 app/Main.hs:29:5: Error: Specified Type Does Not Refine Haskell Type for Main.okList
 Haskell: Main.SList [GHC.Types.Char]
 Liquid : forall a. Main.SList a
4

1 に答える 1

4

の洗練されたタイプはタイプをokList制限していません。サイズを制限しましたが、 から までのタイプをルーズにしStringましたa。

変化する

{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]

に

{-@ okList :: NEList String @-}
okList = SL 1 ["cat"]

そして、それはうまくいきます。

私は Liquidhaskell についてよく知らないことを認めなければならないので、以下のすべては私の勝手な推測に過ぎないかもしれません。

これを行う必要がある主な理由はokList、デフォルトのコンストラクターで個別に定義しているためですSL。のみの洗練された型は、コンストラクターを呼び出すときにリストのサイズが検査され、数値リテラルと比較されてから破棄され、(液体) 型レベルで格納されないSListことを約束します。size v = realSize (elems v)したがって、 にフィードokListするhdと、推論に使用できる唯一の情報はsize v = realSize (elems v)(洗練されたデータ型から) およびsize v >= 0(sizeは として定義されますNat) であり、hdそれが正かどうかはわかりません。

ではhd okList、liquidhaskell は式を評価できない可能性があり、それによってサイズに関する情報を代入okListして取得するため、推論された洗練された型 (この場合は) に基づいてのみ判断を下すことができます。1 つの証拠は、洗練された型がなくても機能することです。Sl 1 ["cat"]okListSList Stringhd $ SL 1 ["cat"]

于 2016-02-22T05:38:57.097 に答える