整体和搜索流中的元素

Question

我想要一个大小结合类型流的 find函数，该函数类似于列表和vects的查找函数。

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

挑战是要做：

1. 总计
2. 消耗不超过常数 log_2 n空间，其中n是编码最大a所需的位数。
3. 不超过一分钟在编译时间检查
4. 不强加运行时费用

通常，流式的总发现实现听起来很荒谬。流是无限的，const False的谓词将使搜索永远继续进行。处理这种普遍情况的一种很好的方法是无限燃料技术。

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

对我的用例效果很好，但是我想知道在某些专业案例中，如果不使用forever，可以说服整体检查器。否则，有人可能会遭受无聊的生活，等待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

两个问题：即使有有限数量的Bits32居民可以尝试，它也不是总计，也无法返回Nothing。也许我可以使用take (pow 2 32)构建列表，然后使用List的Find ...呃，等等...单独的列表将占用空间的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