Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: all_some vs traverse id


view this post on Zulip Yakov Pechersky (Dec 14 2020 at 21:13):

In the new induction' tactic, there is a new def all_some : list (option α) → option (list α) defined, which is provably equal to traverse id. It is used solely in the body of constructor_argument_naming_rule_index as

let local_index_instantiations :=
  (index_occs.map get_major_premise_arg_local_names).all_some in

Are there runtime efficiencies to providing this specialized function, or would traverse id be good enough? Just asking to understand what sorts of constraints there are for writing perfomant tactic code. @Jannis Limperg

view this post on Zulip Jannis Limperg (Dec 14 2020 at 21:21):

If I had realised that traverse id = all_some, I would have probably used the former. However, I suspect (but haven't checked) that traverse id does not short-circuit when it encounters a none, so the specialised thing should be faster. Lean also doesn't specialise type class instances like Haskell probably would, so that's another source of overhead. Whether this sort of consideration matters, given Lean's general slowness, I don't know.

view this post on Zulip Yakov Pechersky (Dec 14 2020 at 21:23):

What would be a way to check if the short-circuiting does occur?

view this post on Zulip Jannis Limperg (Dec 14 2020 at 21:52):

Good question actually. I didn't immediately find a way to test this experimentally; maybe our resident wizards can help with that. Failing that, you can always try to mentally step through the strict execution of traverse id [none, some1].

view this post on Zulip Eric Wieser (Dec 14 2020 at 22:16):

Is short-circuiting is a meaningful thing to ask about if there are no observable side-effects?

view this post on Zulip Eric Wieser (Dec 14 2020 at 22:19):

"does if c then f x else g x short-circuit" seems meaningless to me, and I'm not sure if this case is different

view this post on Zulip Mario Carneiro (Dec 14 2020 at 22:19):

Well, timing is observable; also lean isn't completely side effect free if you use trace

view this post on Zulip Mario Carneiro (Dec 14 2020 at 22:20):

also nonterminating computations are observable, and it's not hard to make those in meta code

view this post on Zulip Rob Lewis (Dec 14 2020 at 22:23):

import tactic.induction control.traversable.basic

def l : list (option ) := none::(list.range 1000000).map some

set_option profiler true

#eval list.all_some l

#eval traverse id l

implies traverse doesn't short circuit. (Both evals are O(n) because of list.map but you can see the difference in the profiler output.)

view this post on Zulip Mario Carneiro (Dec 14 2020 at 22:27):

Here are some evaluation order puzzlers:

meta def loop : bool := loop

-- #eval if tt then loop else ff -- don't use this, it will eat up all your memory
#eval if tt then ff else undefined -- ok
#eval if tt then undefined else ff -- fail
#eval ff && undefined -- ok
#eval let n : bool := undefined in ff && n -- ok

view this post on Zulip Yakov Pechersky (Dec 15 2020 at 14:59):

import control.traversable.basic

def l : list (option ) := none::(list.range 1000000).map some

def all_some {α : Type*} : list (option α)  option (list α)
| [] := some []
| (some a :: as) := list.cons a <$> all_some as
| (none :: as) := none

set_option profiler true

#eval all_some l
#reduce all_some [some 1, none, some 2]
#reduce all_some [some 1, some 0, some 2]

#eval mmap id l
#reduce mmap id [some 1, none, some 2]
#reduce mmap id [some 1, some 0, some 2]

#eval traverse id l
#reduce traverse id [some 1, none, some 2]
#reduce traverse id [some 1, some 0, some 2]

view this post on Zulip Yakov Pechersky (Dec 15 2020 at 15:00):

so mmap id is exactly all_some, and on my machine, actually a little faster (?)


Last updated: May 09 2021 at 21:10 UTC