## Stream: new members

### Topic: functional equivalent of breaking out of a loop

#### Kevin Lacker (Dec 08 2020 at 23:10):

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 (Dec 08 2020 at 23:13):

This is probably a fold by some monadic operator

#### Kevin Lacker (Dec 08 2020 at 23:15):

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 (Dec 08 2020 at 23:16):

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

#### Rob Lewis (Dec 08 2020 at 23:16):

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

#### Rob Lewis (Dec 08 2020 at 23:16):

<|> is monadic "or else"

#### Kevin Lacker (Dec 08 2020 at 23:17):

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

Yep

#### Eric Wieser (Dec 08 2020 at 23:17):

That's the docs#alternative bit

#### Kevin Lacker (Dec 08 2020 at 23:32):

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 (Dec 08 2020 at 23:33):

In this case you probably want docs#tactic.try_core

#### Reid Barton (Dec 08 2020 at 23:34):

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 (Dec 08 2020 at 23:41):

Is there a general name for this function?

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


#### Rob Lewis (Dec 08 2020 at 23:45):

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.

Last updated: May 13 2021 at 22:15 UTC