Merge (ordered) streams

Stream: Is there code for X?

[Logan Murphy]

Is there a way to use what's in data.stream to merge two ordered streams into an ordered stream? I'm guessing that if so, it uses stream.corec_on but I'm not quite sure how it would be done

[Logan Murphy]

E.g. merging

[0,1,2,4,6....]
[3,5,7...]

results in

[0,1,2,3,4,5,6....]

[Alex J. Best]

Here's a fun (monadic) way

def merge (a b : stream ℕ) : stream ℕ := corec_state ((do
    (c, d) ← get,
    if c.head < d.head then
      put (c.tail,d) >>
      return c.head
    else
      put (c,d.tail) >>
      return d.head) : state (stream ℕ × stream ℕ) ℕ)
  (a, b)
#eval (merge ([0,1,2,4,6] ++ₛ(const 8))
             ([3,5,7] ++ₛ const 8)).take 10

[Logan Murphy]

Ah, interesting! Thanks for sharing, Alex

[Yury G. Kudryashov]

Note that streams are highly computationally ineffective.