There is more than one way to do it

Stream: new members

[Isak Colboubrani]

To illustrate the principle that "there is more than one way to do it" in Lean, I've compiled the following list of one-liners for defining a function that takes two natural numbers as inputs and returns their sum. (Some of them are intentionally a bit convoluted!)

Given the variety of options: which of these would be considered idiomatic Lean? Is there a recommended Lean style guide for beginners to help them choose the most idiomatic formulation (for the cases here and more generally)?

def foo₁ (a b : Nat) : Nat := a + b
def foo₂ (a : Nat) (b : Nat) : Nat := a + b
def foo₃ := λ (a b : Nat) => a + b
def foo₄ := λ (a : Nat) (b : Nat) => a + b
def foo₅ : Nat → Nat → Nat := λ | a, b => a + b
def foo₆ : Nat → Nat → Nat := λ a => λ b => a + b
def foo₇ : Nat → Nat → Nat := λ a b => a + b
def foo₈ := fun (a b : Nat) => a + b
def foo₉ := fun (a : Nat) (b : Nat) => a + b
def foo₁₀ : Nat → Nat → Nat := fun a b => a + b
def foo₁₁ (a : Nat) : Nat → Nat := fun b => (a + b : Nat)
def foo₁₂ (a : Nat) : Nat → Nat := fun b => a + b
def foo₁₃ (a : Nat) (b : Nat) : Nat := let c := fun x y => x + y; c a b
def foo₁₄ : Nat → Nat → Nat := fun a => fun b => a + b
def foo₁₅ : Nat → Nat → Nat := fun a b => match (a, b) with | (a, b) => a + b
def foo₁₆ : Nat → Nat → Nat | a, b => a + b
def foo₁₇ (a b : Nat) : Nat := match a, b with | a, b => a + b
def foo₁₈ (a b : Nat) : Nat := have c : Nat := a + b; c
def foo₁₉ : Nat → Nat → Nat := Nat.add
def foo₂₀ : Nat → Nat → Nat := let c (a b : Nat) : Nat := a + b; c
def foo₂₁ : Nat → Nat → Nat := let f := λ a b => a + b; f

example : foo₁ 1 2 = 3 := by rfl
example : foo₁ = foo₂ := by rfl
example : foo₁ = foo₃ := by rfl
example : foo₁ = foo₄ := by rfl
example : foo₁ = foo₅ := by rfl
example : foo₁ = foo₆ := by rfl
example : foo₁ = foo₇ := by rfl
example : foo₁ = foo₈ := by rfl
example : foo₁ = foo₉ := by rfl
example : foo₁ = foo₁₀ := by rfl
example : foo₁ = foo₁₁ := by rfl
example : foo₁ = foo₁₂ := by rfl
example : foo₁ = foo₁₃ := by rfl
example : foo₁ = foo₁₄ := by rfl
example : foo₁ = foo₁₅ := by rfl
example : foo₁ = foo₁₆ := by rfl
example : foo₁ = foo₁₇ := by rfl
example : foo₁ = foo₁₈ := by rfl
example : foo₁ = foo₁₉ := by rfl
example : foo₁ = foo₂₀ := by rfl
example : foo₁ = foo₂₁ := by rfl

[Andrew Yang]

When declaring definitions, 1 (or 2) is usually the idiomatic way. 16 if it is an inductive definition (though we put newlines between). 19 if you are doing an alias (though we would use alias foo := Nat.add)

[Kyle Miller]

Yeah, I'd say only the following three are idiomatic:

def foo₁ (a b : Nat) : Nat := a + b
def foo₂ (a : Nat) (b : Nat) : Nat := a + b
def foo₁₆ : Nat → Nat → Nat | a, b => a + b

The Nat.add one is not, since Nat.add is never referred to directly, but rather it's referred to indirectly with notation. Instead you'd write it like

def foo₁₉ : Nat → Nat → Nat := (· + ·)

[Kyle Miller]

You should be guided by what's clearest for you to read and understand, and to prove things about.

Points for creativity, but there's no way someone would choose the following one over the other choices:

def foo₁₅ : Nat → Nat → Nat := fun a b => match (a, b) with | (a, b) => a + b

Plus, for match statements, using (a, b) for the discriminant rather than having two discriminants a and b can lead to a less-capable match, when there are dependent types involved.

[Ashley Blacquiere]

Not necessarily in a def, but is it also true that in Lean 4 fun a b => a + b is more idiomatic than λ a b => a + b in situations where an anonymous function is needed?

[Kevin Buzzard]

I think the dream was to reclaim lambda as a variable but somehow this never happened

[Michael Rothgang]

Ashley Blacquiere said:

Not necessarily in a def, but is it also true that in Lean 4 fun a b => a + b is more idiomatic than λ a b => a + b in situations where an anonymous function is needed?

The style guide even mentions this explicitly.
It shouldn't be hard to write a linter against this; it's on my short list of small things to do.