Streamsの要素の完全性と検索

Question

ListsとVectのfind関数に類似した、サイズに制限されたStreamsのストリームに対して、find関数が必要です。

total 
find : MaxBound a => (a -> Bool) -> Stream a -> Maybe a 

課題は、それを作ることである。

1. は
2. Nが最大aを符号化するために必要なビット数であるせいぜい定数 log_2 Nスペースを消費しない合計です。
3. 何のランタイムコスト

を課していないコンパイル時

でチェックすることはもはや分もかかり一般的にストリームの総検索の実装は不条理鳴りません。ストリームは無限で、述語がconst Falseの場合、検索は永遠に続行されます。この一般的なケースを処理するうまい方法は、無限の燃料技術です。私のユースケースに適していますが、特定の特殊なケースでは全体のチェッカーがforeverを使用せずに納得することができれば、私は疑問に思う

data Fuel = Dry | More (Lazy Fuel) 

partial 
forever : Fuel 
forever = More forever 

total 
find : Fuel -> (a -> Bool) -> Stream a -> Maybe a 
find Dry _ _ = Nothing 
find (More fuel) f (value :: xs) = if f value 
            then Just value 
            else find fuel f xs 

。そうしないと、誰かがfind forever ?predicateWhichHappensToAlwaysReturnFalse (iterate S Z)の終了を待つ退屈な生活に苦しむかもしれません。

aがBits32の特殊なケースを考えてみましょう。

find32 : (Bits32 -> Bool) -> Stream Bits32 -> Maybe Bits32 
find32 f (value :: xs) = if f value then Just value else find32 f xs 

2つの問題：それは、合計ではありませんし、しようとするBits32住民の有限数があるのにもかかわらず、それはおそらくNothingを返すことができません。たぶん私はtake (pow 2 32)を使用してリストを作成し、次にリストの検索を使用することができます。ああ、待つ...リストだけでGBのスペースを占有します。

原則として、これは難しいはずのようではありません。非常に多くの住民が試してみることができ、現代のコンピュータはすべての32ビットパーミュテーションを数秒で繰り返すことができます。 the (Stream Bits32) $ iterate (+1) 0が最終的には0に戻ってくることを確認する方法がありますか？(+1)は純粋なので、すべての要素が試されたことを一度アサートしますか？

私は穴を埋める方法がわかりませんが、それを合計するには十分にfindを特化していますが、ここは始まりです。おそらくインタフェースが助けになるだろうか？

total 
IsCyclic : (init : a) -> (succ : a -> a) -> Type 

data FinStream : Type -> Type where 
    MkFinStream : (init : a) -> 
       (succ : a -> a) -> 
       {prf : IsCyclic init succ} -> 
       FinStream a 

partial 
find : Eq a => (a -> Bool) -> FinStream a -> Maybe a 
find pred (MkFinStream {prf} init succ) = if pred init 
              then Just init 
              else find' (succ init) 
    where 
    partial 
    find' : a -> Maybe a 
    find' x = if x == init 
       then Nothing 
       else 
       if pred x 
       then Just x 
       else find' (succ x) 

total 
all32bits : FinStream Bits32 
all32bits = MkFinStream 0 (+1) {prf=?prf} 

合計で特定のストリーム上で検索を検証する無限の燃料を使用するように全体チェッカーを伝える方法はありますか？

Answer 1

のシーケンスは、環状であるためにそれが何を意味するのかを定義してみましょう：

%default total 

iter : (n : Nat) -> (a -> a) -> (a -> a) 
iter Z f = id 
iter (S k) f = f . iter k f 

isCyclic : (init : a) -> (next : a -> a) -> Type 
isCyclic init next = DPair (Nat, Nat) $ \(m, n) => (m `LT` n, iter m next init = iter n next init) 

次のように私たちが描くことができるような状況を持っている上記の手段：

-- x0 -> x1 -> ... -> xm -> ... -> x(n-1) -- 
--     ^     | 
--      |--------------------- 

をmは厳密ですn未満ですが（mはゼロに等しくてもかまいません）。nはいくつかのステップの後で、以前に遭遇したシーケンスの要素を取得します。

data FinStream : Type -> Type where 
    MkFinStream : (init : a) -> 
       (next : a -> a) -> 
       {prf : isCyclic init next} -> 
       FinStream a 

次に、のループから抜け出すためにfuelと呼ばれる上限を使用する、ヘルパー関数を定義してみましょう：

findLimited : (p : a -> Bool) -> (next : a -> a) -> (init : a) -> (fuel : Nat) -> Maybe a 
findLimited p next x Z = Nothing 
findLimited p next x (S k) = if p x then Just x 
           else findLimited pred next (next x) k 

今findはそうのように定義することができます。

find : (a -> Bool) -> FinStream a -> Maybe a 
find p (MkFinStream init next {prf = ((_,n) ** _)}) = 
    findLimited p next init n 

いくつかのテストがあります：

-- I don't have patience to wait until all32bits typechecks 
all8bits : FinStream Bits8 
all8bits = MkFinStream 0 (+1) {prf=((0, 256) ** (LTESucc LTEZero, Refl))} 

exampleNothing : Maybe Bits8 
exampleNothing = find (const False) all8bits    -- Nothing 

exampleChosenByFairDiceRoll : Maybe Bits8 
exampleChosenByFairDiceRoll = find ((==) 4) all8bits  -- Just 4 

exampleLast : Maybe Bits8 
exampleLast = find ((==) 255) all8bits      -- Just 255