Zulip Chat Archive

Stream: new members

Topic: arbitrary nat as output


view this post on Zulip 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"?

view this post on Zulip Jalex Stark (Aug 06 2020 at 04:09):

there is in fact a natural number in there

view this post on Zulip 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.

view this post on Zulip Chris M (Aug 06 2020 at 04:27):

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

view this post on Zulip Jalex Stark (Aug 06 2020 at 04:45):

did you try going to the definition of arbitrary?

view this post on Zulip Jalex Stark (Aug 06 2020 at 04:46):

there's no magic going on anywhere

view this post on Zulip Jalex Stark (Aug 06 2020 at 04:47):

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

view this post on Zulip 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

view this post on Zulip 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) ?

view this post on Zulip 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".

view this post on Zulip Reid Barton (Aug 06 2020 at 13:58):

arbitrary is basically unused anyways

view this post on Zulip Reid Barton (Aug 06 2020 at 14:14):

at least, in mathlib

view this post on Zulip Jasmin Blanchette (Aug 06 2020 at 14:33):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 06 2020 at 14:37):

I actually had misremembered how this is set up

view this post on Zulip Reid Barton (Aug 06 2020 at 14:37):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Reid Barton (Aug 06 2020 at 14:43):

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

view this post on Zulip Reid Barton (Aug 06 2020 at 14:43):

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

view this post on Zulip 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.

view this post on Zulip 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