WHNF of partially applied constants

Stream: metaprogramming / tactics

[Rish Vaishnav]

I've been trying to understand this example from the Lean 4 metaprogramming book. The fact that WHNF has different rules for partial applications when a function is inlined makes me suspect that what's really going on here is that WHNF doesn't reduce partially applied constants, rather than functions. However, this seems to be a counterexample:

open Lean.Elab.Term in
def whnf' (e : TermElabM Syntax) (md := TransparencyMode.default) :
    TermElabM Format := do
  let e ← elabTermAndSynthesize (← e) none
  ppExpr (← whnf e)

def myadd : Nat → Nat → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

#eval whnf' `(myadd 1)
-- ▶ 231:1-231:6: information:
-- fun x =>
--   match 1, x with
--   | a, Nat.zero => a
--   | a, Nat.succ b => Nat.succ (Nat.add a b)
#eval whnf' `(Nat.add 1)
-- Nat.add 1

What explains the different behavior here? Is the function being inlined behind the scenes? Or is something else going on? Thanks. (and I'll be happy to update the book with any additional details)

[Gabriel Ebner]

I'm not sure what you mean by "different rules for partial applications"? The line you link to shows that WHNF does β-reduction.

[Gabriel Ebner]

In your example, the myadd function is defined the same way as Nat.add as far as I can tell. However Nat.add is special-cased (by name) in both the kernel and MetaM to use GMP.

[Rish Vaishnav]

So, WHNF always β-reduces regardless of whether a function is behind a constant and appears in a partial application? And Nat.add is a very special case that doesn't? I just tried #eval whnf' ``(List.append [1]) which does reduce, so yeah this does seem to be the case. The line "Functions applied to too few arguments are in WHNF" seems to suggest that something more general is going on here, though I can't put my finger on it.

[Gabriel Ebner]

Oh, that line seems to be wrong. EDIT: and Nat.add is a bad running example for WHNF, since it is special-cased everywhere.

[Gabriel Ebner]

β-reduction is when you syntactically have an application of a lambda. It doesn't matter what's in the lambda. But it literally needs to be a lambda, not a constant or free variable that unfolds to a lambda.