Stream: new members

Topic: arbitrary nat as output

Chris M (Aug 06 2020 at 04:06):

I'm somewhat puzzled by the following function definition: def f: ℕ → ℕ := fun n, arbitrary ℕ . It seems to me that f is not actually a mathematical function. It takes a natural number as input and outputs, ... a term that has type nat but it's not an actual natural number. I'm tempted to say that mathematically speaking, this is an ill-defined function? Should I think of this as essentially "using the axiom of choice"?

Jalex Stark (Aug 06 2020 at 04:09):

there is in fact a natural number in there

Shing Tak Lam (Aug 06 2020 at 04:09):

It just outputs the provided default for the inhabited typeclass on that type. For nat, the inhabited instance is

instance : inhabited  :=
nat.zero

so arbitrary ℕ = 0.

Chris M (Aug 06 2020 at 04:27):

Ohh I see. Does this hold for all arbitrary ...for some type at ...?

Jalex Stark (Aug 06 2020 at 04:45):

did you try going to the definition of arbitrary?

Jalex Stark (Aug 06 2020 at 04:46):

there's no magic going on anywhere

Jalex Stark (Aug 06 2020 at 04:47):

Shing Tak just unfolded the definition into an english sentence of comparable length

Mario Carneiro (Aug 06 2020 at 05:09):

This should be contrasted with def f: ℕ → ℕ := fun n, @classical.choice ℕ _, which is a function from nat to nat that we can prove is constant but for which we don't know the value

Jacques Carette (Aug 06 2020 at 13:32):

Is it just me, but while inhabited is a great name, arbitrary is likely to lead to confusion (witness: this thread) ?

Jalex Stark (Aug 06 2020 at 13:51):

i feel like arbitrary is well-named but needs a docstring. It's very close to the mathematician's "arbitrary".

Reid Barton (Aug 06 2020 at 13:58):

arbitrary is basically unused anyways

Reid Barton (Aug 06 2020 at 14:14):

at least, in mathlib

Jasmin Blanchette (Aug 06 2020 at 14:33):

Since the class is called inhabited, maybe inhabitant or some_inhabitant?

Jasmin Blanchette (Aug 06 2020 at 14:34):

We used to have arbitrary in Isabelle with the same meaning as in Lean (except that it worked with all types, since all HOL types are inhabited). It was renamed undefined. I never felt this was much of an improvement.

Andrew Ashworth (Aug 06 2020 at 14:35):

Is arbitrary even going to survive until Lean 4? I think where they are used - they can be replaced with meta constants.

Reid Barton (Aug 06 2020 at 14:37):

I actually had misremembered how this is set up

Reid Barton (Aug 06 2020 at 14:37):

arbitrary is basically an irreducible version of default which is the guy from inhabited

Andrew Ashworth (Aug 06 2020 at 14:39):

I always wondered why more arbitrary wasn't used in mathlib. It was supposed to be the canonical 37 for partial functions.

Jalex Stark (Aug 06 2020 at 14:39):

obviously anything one can do with arbitrary one can also do with default, but arbitrary is making a promise to the reader that all you need is some inhabited instance, not any particular one

Reid Barton (Aug 06 2020 at 14:41):

Andrew Ashworth said:

I always wondered why more arbitrary wasn't used in mathlib. It was supposed to be the canonical 37 for partial functions.

If you're going to totalize, it's usually more useful to totalize in a convenient way (normally meaning by 0 and not by 37)

Reid Barton (Aug 06 2020 at 14:43):

From a mathematician's perspective, inhabited ought to be called "pointed"

Reid Barton (Aug 06 2020 at 14:43):

or at least the definition of pointed would look exactly the same up to renaming

Jacques Carette (Aug 06 2020 at 14:55):

pointed is great, but one assumes that if something is pointed, then homomorphisms preserve the given point.

To use HoTT terminology, arbitrary does bring to mind a 'mere inhabitant'. That is indeed quite useful, as it corresponds nicely to the classical notion of inhabitation.

In all my codes, I consider the use of having a default point a "code smell". I have indeed been working to remove that from one of my student's codes in the last week. (inhabited is ok, as I know I can't rely on that mere point in any ways; default is more dangerous, as downstream code has this way of assuming it means pointed when there is in fact no such guarantee). But that is what my experience tells me, I certainly wouldn't make that a hard rule, not without more evidence.

Reid Barton (Aug 06 2020 at 14:55):

And I guess the point is even when you're in a general setting like option.iget where you can't totalize by something like 0, it's still more useful to pass on the option to know the default value is 0 to your client by using default, rather than using arbitrary which prevents anyone from knowing about the value

Last updated: May 15 2021 at 23:13 UTC