Why are there so many ways for doing the same thing in Lean?

Stream: new members

[Noah Stebbins]

One thing I noticed in Lean was just how many ways there are for doing the same thing. For example, let's say I want to define a Point structure with x & y coordinates and define element-wise addition. I could do

structure OrderedPair (α: Type*) where
  x: α
  y: α
  deriving Repr

def add (a b: OrderedPair Nat): OrderedPair Nat :=
  ⟨a.x + b.x, a.y + b.y⟩

def add2 (a b: OrderedPair Nat): OrderedPair Nat :=
  OrderedPair.mk (a.x + b.x) (a.y + b.y)

def add3 (a b: OrderedPair Nat): OrderedPair Nat where
  x := a.x + b.x
  y := a.y + b.y

def add4: OrderedPair Nat → OrderedPair Nat → OrderedPair Nat
  | ⟨x₁, y₁⟩, ⟨x₂, y₂⟩ => ⟨x₁ + x₂, y₁ + y₂⟩

def add5: OrderedPair Nat → OrderedPair Nat → OrderedPair Nat
  | OrderedPair.mk x₁ y₁, OrderedPair.mk x₂ y₂ => OrderedPair.mk (x₁ + x₂) (y₁ + y₂)

def add6 (x y: OrderedPair Nat): OrderedPair Nat :=
  match x, y with
  | ⟨x₁, y₁⟩, ⟨x₂, y₂⟩ => ⟨x₁ + x₂, y₁ + y₂⟩

My question is - why does Lean offer so many ways of doing the same thing? As a newbie, I find it challenging to figure out which way is better in certain cases or how they all compare. At first glance, I would think it far easier for the language designers to establish just 1 or 2 ways of doing something in order to establish uniformity and consistency.

[Bbbbbbbbba]

Even Python has many ways to do the same thing; I think what you are asking is which ways are idiomatic.

[Henrik Böving]

But you cant really establish 1 or 2 ways. Pattern matching is something we definitely need. The .mk way must be there because that's how the type theory works. The .x syntax is just too convenient not to have etc. You won't find a majority (or technical possibility) to remove any of the features here.

[Bbbbbbbbba]

Also add is obviously syntactic sugar for add2, and presumably add3 is syntactic sugar for add2 too, etc., so in those cases I believe there shouldn't be any lasting effects to worry about, and the only criteria is immediate readability.

[Bbbbbbbbba]

So I would use add by default, but add2 or add3 if I feel that the reader may be confused about the expected type and/or the order of the constructor parameters (and in context it is worth it to clarify).

[Johan Commelin]

Bbbbbbbbba said:

Also add is obviously syntactic sugar for add2, and presumably add3 is syntactic sugar for add2 too, etc., so in those cases I believe there shouldn't be any lasting effects to worry about, and the only criteria is immediate readability.

You are technically correct, but I'm not sure the "obviously" is obviously correct.

[Mark Fischer]

Noah Stebbins said:

far easier for the language designers to establish [...]

Even pretty basic syntax like = being an infix operator for Eq.refl isn't built-in to the language, but rather defined somewhere in the prelude. Part of Lean's core design is extremely powerful extensibility (meta-programming) facilities. This means Lean's users have a lot of power to, say, design 1,000 ways to do the same thing without any input/consent from the language designers. The good news is that generally, it's the good stuff that gets adopted by the wider community.

That said, you could certainly imagine some code bases becoming extremely hard to onboard even seasoned Lean users into due to be filled to the brim with bespoke domain specific symbols that baffle non-domain-experts. Understanding the trade-offs for such choices is part of the design space for a project rather than resting solely on the shoulders of language designers.

[Noah Stebbins]

Thank you guys for the different perspectives!

To provide additional context to my original question - since I'm relatively new to Lean all of the different ways of doing the same thing feel arbitrary to me since I don't yet fully understand the raison d'etre for each way yet. I've been reading through the Lean tutorials and they are like "you could do it this way, and this way, and this way".

Obviously there are many ways of doing the same thing in Python too but I wasn't given all the keys to the kingdom right away. For example, I didn't stumble upon Python metaclasses until way after I did my first Python tutorials.

This is absolutely not to say "Python is better than Lean" haha. On the contrary, I love Lean. But I've noticed that some concepts in Lean's tutorials have been harder for me to grok at first pass and this was one of them.

[Kyle Miller]

Using OrderedPair.mk directly is not encouraged. It's an implementation detail for structures. Instead, you can use "structure instance notation":

def add2 (a b : OrderedPair Nat) : OrderedPair Nat :=
  { x := a.x + b.x, y := a.y + b.y }

The where example (add3) is syntax sugar for this. It's basically a macro, where where ... becomes := { ... }.

[Kyle Miller]

add4, add5, and add6 are the exact same as each other, except that only add6 supports named arguments with add6 (x := val1) (y := val2), since in the other two the arguments aren't given any names.

These are different from add, add2, and add3 because they do pattern matching on the arguments, and, while they do turn out to be definitionally equal (making use of "eta for structures" I believe), the equation lemmas you get for add4, add5, add6 are more complicated. You can check this with

#check add.eq_1
#check add4.eq_1

[Kyle Miller]

You can use structure instance notation for pattern matching. Here's something that is exactly the same as add4:

def add4: OrderedPair Nat → OrderedPair Nat → OrderedPair Nat
  | {x := x₁, y := y₁}, {x := x₂, y := y₂} => {x := x₁ + x₂, y := y₁ + y₂}

[Kyle Miller]

That said, the OrderedPair type is called docs#Prod, and mathlib already has element-wise addition defined for it:

import Mathlib

variable (α β : Type*) [Add α] [Add β] (p q : α × β)

#check p + q -- succeeds

See docs#Prod.instAdd

[Michal Wallace (tangentstorm)]

@Noah Stebbins I think part of it is that we want two basic features of the languge:

• it should be very easy to check that proofs are correct
• it should be very easy to express complex mathematical ideas using notation familiar to mathematicians and computer scientists

In order to get the first property, you want a very simple core language. You haven't even gotten down to the lowest levels here... try typing #reduce add5to see what you're actually dealing with:

fun x x_1 =>
  { x := (Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, ⟨n_ih, PUnit.unit⟩⟩) x_1.1).1 x.1,
    y := (Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, ⟨n_ih, PUnit.unit⟩⟩) x_1.2).1 x.2 }

!!

In order to get the second property, you want to do a lot of aliasing and syntactic sugar, and just giving names to things for human readability...

There's no right way to use the language, but as more people use it (and want to be able to read and use each other's code), certain idioms and patterns become more common, like the naming conventions in Mathlib, etc...

[Kyle Miller]

I'm not sure #reduce add5 is very informative (and it's a bit misleading) — that's unfolding all definitions, including natural number addition. It's also simplifying away the match beyond what you might expect due to eta for structures.

[Kyle Miller]

Here's add5 at essentially the lowest levels:

def add5' : OrderedPair ℕ → OrderedPair ℕ → OrderedPair ℕ :=
  fun p q ↦
    OrderedPair.casesOn p fun px py ↦ OrderedPair.casesOn q fun qx qy ↦
      { x := px + qx, y := py + qy }

[Kyle Miller]

If you object to notation, then here's the interpretation of that notation:

def add5' : OrderedPair ℕ → OrderedPair ℕ → OrderedPair ℕ :=
  fun p q ↦
    OrderedPair.casesOn p fun px py ↦ OrderedPair.casesOn q fun qx qy ↦
      OrderedPair.mk (HAdd.hAdd px qx) (HAdd.hAdd py qy)

[Michal Wallace (tangentstorm)]

Right. It's not informative at all... But that's the level you want the core verifier to work at to make it as likely as possible that you can trust it.

[Kyle Miller]

No, I mean it's misleading to say that this is what you're "actually" dealing with. (Modified my message)

[Kyle Miller]

The problem is that #reduce is causing a large number of rules for definitional equality to be applied, giving a term that defeq but not very related anymore. What I wrote for add5' is the actual interpretation of add5 after unfolding an auxiliary definition created during elaboration.

[Kyle Miller]

One reason I'm pushing back on this because #reduce makes the terms that give a "!!" impression, but it's not hard to imagine writing this casesOn expression by hand. You can even see the correspondence that pattern matching is being turned into these casesOn expressions.