Totality and searching for elements in Streams

Question

I want a find function for Streams of size-bounded types which is analogous to the find functions for Lists and Vects.

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

The challenge is it to make it:

1. be total
2. consume no more than constant log_2 N space where N is the number of bits required to encode the largest a.
3. take no longer than a minute to check at compile time
4. impose no runtime cost

Generally a total find implementation for Streams sounds absurd. Streams are infinite and a predicate of const False would make the search go on forever. A nice way to handle this general case is the infinite fuel technique.

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

That works well for my use case, but I wonder if in certain specialized cases the totality checker could be convinced without using forever. Otherwise, somebody may suffer a boring life waiting for find forever ?predicateWhichHappensToAlwaysReturnFalse (iterate S Z) to finish.

Consider the special case where a is Bits32.

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

Two problems: it's not total and it can't possibly return Nothing even though there's a finite number of Bits32 inhabitants to try. Maybe I could use take (pow 2 32) to build a List and then use List's find...uh, wait...the list alone would take up GBs of space.

In principle it doesn't seem like this should be difficult. There's finitely many inhabitants to try, and a modern computer can iterate through all 32-bit permutations in seconds. Is there a way to have the totality checker verify the (Stream Bits32) $ iterate (+1) 0 eventually cycles back to 0 and once it does assert that all the elements have been tried since (+1) is pure?

Here's a start, although I'm unsure how to fill the holes and specialize find enough to make it total. Maybe an interface would help?

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}

Is there a way to tell the totality checker to use infinite fuel verifying a search over a particular stream is total?

Answer 1

Let's define what it means for a sequence to be cyclic:

%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)

The above means that we have a situation which can be depicted as follows:

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

where m is strictly less than n (but m can be equal to zero). n is some number of steps after which we get an element of the sequence we previously encountered.

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

Next, let's define a helper function, which uses an upper bound called fuel to break out from the loop:

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

Now find can be defined like so:

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

Here are some tests:

-- 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