functional equivalent of breaking out of a loop

Stream: new members

[Kevin Lacker]

I feel like there's some fancy way to do this without defining my own function and I just don't know it. Often I have some function where f(x) returns an option, and I have a list xs, and I want to return the first value of the list where f(x) is some. But I don't want to do a map on the list and spend time on the whole list if the answer is near the beginning. Ie in python

def find_first(f, mylist):
  for x in mylist:
    y = f(x)
    if y is not None:
      return y

Is there a Lean equivalent to this where I don't have to define a helper recursive function?

[Eric Wieser]

This is probably a fold by some monadic operator

[Rob Lewis]

docs#list.mfirst ?

[Kevin Lacker]

def list.mfirst {m : Type u → Type v} [monad m] [alternative m] {α : Type w} {β : Type u} (f : α → m β) : list α → m β
| []      := failure
| (a::as) := f a <|> list.mfirst as

won't that go down the whole list?

[Kevin Lacker]

oh, I was ignoring the <|> which perhaps does something unusual

[Rob Lewis]

No, if f a succeeds (e.g. returns some in the option monad) only the left side of the <|> will fire.

[Rob Lewis]

<|> is monadic "or else"

[Kevin Lacker]

does the monad system know to turn that failure into a none for the option monad

[Rob Lewis]

Yep

[Eric Wieser]

That's the docs#alternative bit

[Kevin Lacker]

if i have two monadic things with different monad types that have a "fail", can i convert from one to the other? like if I have a tactic foo and I want an option foo

[Reid Barton]

In this case you probably want docs#tactic.try_core

[Reid Barton]

In general option foo is exactly the thing you can convert into monads that have a "fail", but converting out of other monads is monad-specific

[Yakov Pechersky]

Is there a general name for this function?

func : option foo -> m foo
| some x = pure x
| none = failure

[Rob Lewis]

Kevin Lacker said:

if i have two monadic things with different monad types that have a "fail", can i convert from one to the other? like if I have a tactic foo and I want an option foo

You can turn an option into a tactic (I think there's a coercion?) but not the other way around, which would need you to summon a tactic state out of nowhere.