all_some vs traverse id

Stream: metaprogramming / tactics

[Yakov Pechersky]

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

[Jannis Limperg]

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.

[Yakov Pechersky]

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

[Jannis Limperg]

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].

[Eric Wieser]

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

[Eric Wieser]

"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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Rob Lewis]

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.)

[Mario Carneiro]

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

[Yakov Pechersky]

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]

[Yakov Pechersky]

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