Defining partial functions: Why is this pattern not common?

Stream: new members

[Huỳnh Trần Khanh]

import data.nat.basic

-- Can you define partial functions in Lean? Yes, you can!

def this_is_a_partial_function (n : ℕ) (h : n > 0) : ℕ := if h1 : n > 0 then n - 1 else begin
  exfalso,
  exact h1 h,
end

#eval this_is_a_partial_function 12837481729847128934718237489178942739 (nat.succ_pos 12837481729847128934718237489178942738)

In this vein, nat subtraction and division can be partial functions.

[Huỳnh Trần Khanh]

Why are they not partial functions? It must have been an intentional design choice.

[Kevin Buzzard]

Yes I totally agree that this can be done. Indeed I even tried to do it myself once. However I just ended up learning the hard way that it's simply much easier in practice to let functions return junk values outside the domain of definition.

[Kevin Buzzard]

The example which taught me why the current design decision is a good one was square roots. I was formalising 1st year example sheets and some questions mentioned square roots, which we didn't have in mathlib at the time. In fact I was teaching my students the formal definition -- if x>=0 then the square root of x is the sup of {y | y^2 <= x}, and if x < 0 then this set doesn't have a sup but who cares, negative reals don't have square roots.

[Kevin Buzzard]

So I defined a square root function to take as input a real number r and a proof that it was >= 0, and then returned this sup. And I posted it on the gitter chat (we used gitter before Zulip) and the computer scientists laughed at me because actually nowhere in my definition did I use the assumption that the real number was >= 0, so the function to them looked farcical, it demanded an input and then just ignored it.

[Kevin Buzzard]

The sup function returned junk values for sets without a sup, so the function ran happily even when presented with a negative number (it probably just returned the value 0). I was offended by this idea because sqrt(-1) might be a lot of things but it's certainly not 0, so I went with my definition when formalising the solutions to my problem sheets. Mario just formalised the current mathlib version and added it to mathlib in the interim. And then I found when doing my example sheets that this stupid extra input was a complete pain because whenever I even mentioned a square root I had to supply this proof, even though I knew it wasn't even necessary for the function to run. For example doing a long calc proof that sqrt(2)+sqrt(3)<sqrt(10) was really painful because on every line there were new square roots popping up and I had to just keep proving that various random numbers were positive.

I soon came around to the idea of letting functions be total and returning junk values.