Zulip Chat Archive

Stream: new members

Topic: functional equivalent of breaking out of a loop


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Dec 08 2020 at 23:13):

This is probably a fold by some monadic operator

view this post on Zulip Rob Lewis (Dec 08 2020 at 23:13):

docs#list.mfirst ?

view this post on Zulip 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?

view this post on Zulip Kevin Lacker (Dec 08 2020 at 23:16):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 08 2020 at 23:16):

<|> is monadic "or else"

view this post on Zulip Kevin Lacker (Dec 08 2020 at 23:17):

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

view this post on Zulip Rob Lewis (Dec 08 2020 at 23:17):

Yep

view this post on Zulip Eric Wieser (Dec 08 2020 at 23:17):

That's the docs#alternative bit

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 08 2020 at 23:33):

In this case you probably want docs#tactic.try_core

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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