Zulip Chat Archive

Stream: new members

Topic: Defining partial functions: Why is this pattern not common?

view this post on Zulip Huỳnh Trần Khanh (Feb 18 2021 at 12:31):

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
  exact h1 h,

#eval this_is_a_partial_function 12837481729847128934718237489178942739 (nat.succ_pos 12837481729847128934718237489178942738)

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

view this post on Zulip Huỳnh Trần Khanh (Feb 18 2021 at 12:32):

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

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 12:32):

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.

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 12:34):

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.

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 12:35):

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.

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 12:38):

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.

Last updated: May 07 2021 at 00:30 UTC