how am I getting infinite recursion?

Stream: metaprogramming / tactics

[Joe Palermo]

Hi,

I'm learning to write tactics to traverse the structure of an expr and extract certain bits. It seems that a tactic I wrote is leading to the error: "excessive memory consumption detected at 'vm' (potential solution: increase memory consumption threshold)". This sounds to me like it's running a bottomless recursion and it runs out of memory, but looking at my code I can't see how it would fail to reach the base case which ends the recursion. Perhaps what I wrote doesn't mean what I think it does. I would appreciate some guidance on how to fix it. Thanks!

namespace expr
open tactic

meta def extract_bindings (e: expr) : expr :=
  match e with
    | lam var_name b_info var_type body := lam var_name b_info var_type (extract_bindings body)
    | pi var_name b_info var_type body := pi var_name b_info var_type (extract_bindings body)
    | _ := (@expr.var tt 0)
  end

-- this one is fine
run_cmd tactic.trace (extract_bindings (@expr.var tt 0))

-- this one produces the error
run_cmd tactic.trace (extract_bindings
 (expr.lam (mk_simple_name "α") binder_info.implicit (expr.sort $ level.succ level.zero)
  (expr.lam (mk_simple_name "β") binder_info.implicit (expr.sort $ level.succ level.zero) (@expr.var tt 0))
 ))

end expr

[Yakov Pechersky]

Can you express your function using expr.fold?

[Yakov Pechersky]

If your thing truly recurses properly, you wouldn't need to write is as a meta def, just def

[Joe Palermo]

Thanks for the suggestion. I'll try to rewrite it with fold

[Jannis Limperg]

Okay this is a weird one. Here's a working version:

namespace expr
open tactic

meta def extract_bindings : expr → expr := λ e,
  match e with
    | lam var_name b_info var_type body := lam var_name b_info var_type (extract_bindings body)
    | pi var_name b_info var_type body := pi var_name b_info var_type (extract_bindings body)
    | _ := (@expr.var tt 0)
  end

run_cmd tactic.trace (extract_bindings (@expr.var tt 0))

run_cmd trace $
    extract_bindings $
      lam `α binder_info.default (expr.sort level.zero) $
      lam `β binder_info.default (expr.sort level.zero) $
      var 0

end expr

The difference is in the definition of extract_bindings. Arguments before the colon, like e in your version, are treated as parameters in definitions, meaning they are fixed in recursive calls. But I don't understand why Lean even accepted your definition in the first place. Usually, extract_bindings should have type expr in the body of its definition (since the e is fixed), so extract_bindings body should be a type error.

@Gabriel Ebner can you tell what's going on here?

Yakov Pechersky said:

If your thing truly recurses properly, you wouldn't need to write is as a meta def, just def

In this case, expr is already meta, so the definition must be meta as well.

[Gabriel Ebner]

Jannis Limperg said:

But I don't understand why Lean even accepted your definition in the first place. Usually, extract_bindings should have type expr in the body of its definition (since the e is fixed), so extract_bindings body should be a type error.

docs#expr.has_coe_to_fun :smile:

[Jannis Limperg]

Ha! That explains the infinite recursion. Thanks!

[Joe Palermo]

Wow, I didn't expect the problem to be in the function signature...

[Joe Palermo]

So (extract_bindings body) was being expanded to (expr.app extract_bindings body). Also extract_bindings had an implicit argument (causing infinite recursion), but has_coe_to_fun prevented a type error from showing up on (extract_bindings body) because of the extra expr.app...

[Joe Palermo]

I hope I'm understanding correctly here.

How can you prevent has_coe_to_fun from doing that? When does has_coe_to_fun apply? Was the change to the function signature enough to inhibit it? Because I don't see an extra expr.app in the resulting expression now that the program works

[Eric Wieser]

local attribute [-instance] expr.has_coe_to_fun

[Jannis Limperg]

Your understanding seems correct.

Joe Palermo said:

When does has_coe_to_fun apply?

Whenever Lean sees an application x y with x : T and T not a function type, it tries to look for an instance of has_coe_to_fun T. (There are probably nasty details to consider, but that's the idea.) For expr specifically, this allows you to write f x with f, x : expr and f presumably of function type, which is occasionally handy.

Was the change to the function signature enough to inhibit it? Because I don't see an extra expr.app in the resulting expression now that the program works

With the change to the function signature, extract_bindings has type expr -> expr in the body of its definition, so it's already a function and the has_coe_to_fun business doesn't apply.