Translate a Haskell `traversable` search

Stream: general

[Alex Meiburg]

This was a lovely puzzle + thread, about how to efficiently search over a tree (or more generally, any Traversable) to find an element matching a predicate - given a guarantee that there is one.

https://x.com/effectfully/status/1919157455772434887

I'd be really curious to see if we can translate this to Lean. And it might make a nice function to have in Batteries, I think?

[Alex Meiburg]

For those who don't want to click through Twitter, this is the puzzle:

GpKBtBiWgAArQ78.jpg

These are a few of the better solutions:

https://gist.github.com/LSLeary/5083d1dfe403d1562e7778713d97b22a
https://gist.github.com/LiamGoodacre/bce9e1fbe73b9b80e8cc521f2a2ca687
https://gist.github.com/sjoerdvisscher/dc1ab6b36ba6988d2bcca0face77dc57

[Alex Meiburg]

Mm, actually I'm not sure if it makes sense. I think that in Lean a Traversable is always finite, not so in Haskell...?

[Aaron Liu]

In Lean I think a traversable is always finite, because you can traverse over it with a monad that counts up how big the traversable is.