Zulip Chat Archive

Stream: general

Topic: Naming: eval vs apply


Eric Wieser (Jan 24 2021 at 13:27):

I'd like to unify the names of the following definitions:

  • docs#monoid_hom.apply: Evaluation of a dependent function at a point is a monoid hom
  • docs#ring_hom.apply: Evaluation of a dependent function at a point is a ring hom
  • docs#monoid_hom.eval: Evaluation of a monoid_hom at a point is a monoid hom
  • docs#linear_map.applyₗ: Evaluation of a linear_map over a commutative R at a point is a linear_map
  • doesn't yet exist: Evaluation of a linear map over a non-commutative R at a point is an add_monoid_hom

Essentially, these are all "evaluation of an X at a point is a Y", where X is possibly-bundled function type and Y is a definitely bundled function type. Unfortunately, the naming is currently very ad-hoc.

I've opened #5851 and #5847 to make the picture a little better, but realized that even with my naming there, the question of eval vs apply still comes up. Some naming options:

``

  1. Use X.apply_Y for all cases. The above functions become

    • pi.apply_monoid_hom : (Π i, f i) →* f i
    • pi.apply_ring_hom : (Π i, f i) →+* f i
    • monoid_hom.apply_monoid_hom : (M →* M₂) →* M₂
    • linear_map.apply_linear_map : (M →ₗ[R] M₂) →ₗ[R] M₂
    • linear_map.apply_add_monoid_hom : (M →ₗ[R] M₂) →+ M₂
  2. Use Y.apply_X for all cases. The above functions become

    • monoid_hom.apply_pi : (Π i, f i) →* f i
    • ring_hom.apply_pi : (Π i, f i) →+* f i
    • monoid_hom.apply_monoid_hom : (M →* M₂) →* M₂
    • linear_map.apply_linear_map : (M →ₗ[R] M₂) →ₗ[R] M₂
    • monoid_hom.apply_linear_map : (M →ₗ[R] M₂) →+ M₂

Plus some variants:

(i) Use eval instead of apply
(ii) Shorten X.apply_pi to X.apply
(iii) Shorten X.apply_X to X.apply

I have a fairly strong feeling that 1 is better than 2 (it enables dot notation).
I don't have any opinion on (i), (ii) is moot given the choice of 2, and (iii) is in my opinion not worth the impact it has on discoverability of the other variants.

Anne Baanen (Jan 25 2021 at 09:49):

I agree the dot notation is a good reason to prefer 1 over 2 (except for pi). Slight preference for apply over eval (for computer-sciency reasons: eval indicates some kind of "syntactical" representation of a function, e.g. polynomials). Slight preference for (iii), for symmetry.

Anne Baanen (Jan 25 2021 at 09:50):

/poll X.apply_Y turns a:
X into a Y
Y into an X

Anne Baanen (Jan 25 2021 at 09:51):

/poll eval or apply?
eval
apply

Anne Baanen (Jan 25 2021 at 09:52):

/poll X.apply is short for?
X.apply_pi
X.apply_X
neither

Mario Carneiro (Jan 25 2021 at 09:52):

I don't understand any of these questions

Mario Carneiro (Jan 25 2021 at 09:53):

for me apply means function application

Anne Baanen (Jan 25 2021 at 09:53):

What would you call the definition M → (M →ₗ[R] M₂) →ₗ[R] M₂?

Mario Carneiro (Jan 25 2021 at 09:54):

eval seems fine since it's backwards

Mario Carneiro (Jan 25 2021 at 09:54):

it could be apply but not if that name is already being used for the reverse

Mario Carneiro (Jan 25 2021 at 09:55):

I don't think we have a proper name for \lam f, f x

Johan Commelin (Jan 25 2021 at 09:57):

this is the "evaluation at x" function, which is different from pi.apply right?

Eric Wieser (Jan 25 2021 at 10:02):

The current monoid_hom.apply _ x f is "evaluation of a pi function f at x" (which is what I'm proposing be renamed to pi.apply or pi.eval, making your statement wrong)

Eric Wieser (Jan 25 2021 at 10:02):

The current monoid_hom.eval _ x f is "evaluation of a monoid_hom function f at x".

All of these definitions take an argument x and emit a bundled hom mapping f to f x. They differ both in the type of f, and the bundling of the resulting hom.

Johan Commelin (Jan 25 2021 at 10:05):

I could imagine calling "evaluation of a pi function f at x" something like f.coeff x.

Johan Commelin (Jan 25 2021 at 10:05):

Maybe dot-notation will not work :sad:

Eric Wieser (Jan 25 2021 at 10:05):

In most cases when you're using these definitions you don't have f, because the whole points is to create the bundled thing from f \to f x

Eric Wieser (Jan 25 2021 at 10:07):

And I guess even when you do end up working through the proof and end up with monoid_hom.coeff x f, dot notation won't be used by the pretty printer because dot notation isn't used for bundled homs

Eric Wieser (Jan 25 2021 at 10:11):

Some other cases for X not mentioned in my top message: finsupp, dfinsupp.

Eric Wieser (Jan 25 2021 at 22:28):

There seems to be consensus at least on which namespace these defs belong in. Any more votes on eval vs apply?

Eric Wieser (Feb 03 2021 at 22:18):

Oh, we also have docs#function.eval : i → (Π i, f i) → f i it seems (cf docs#monoid_hom.apply : i → (Π i, f i) →* f i, docs#monoid_hom.eval : A →* (A →* B) →* B)

Floris van Doorn (Feb 03 2021 at 23:53):

I have a small preference for eval, but am fine with either.

I have a fairly strong feeling that 1 is better than 2 (it enables dot notation).

This confuses me. I thought that dot notation doesn't work, even with this naming scheme, because it has to insert a coe_fn before the definition has an argument that is actually an X, and dot notation doesn't do that(?)

Eric Wieser (Feb 04 2021 at 00:22):

A related question is whether things belong in the function or pi namespace

Eric Wieser (May 12 2021 at 14:45):

I've renamed just the pi definitions in #5851, so that we have pi.eval_add_monoid_hom for consistency with docs#dfinsupp.eval_add_monoid_hom and docs#quadratic_form.eval_add_monoid_hom, and partial consistency with docs#function.eval. That choice seems consistent with the result of the poll above.

Eric Wieser (May 16 2021 at 08:52):

Left out of the above was docs#linear_map.proj, which I figured would be unpopular as pi.eval_linear_map

Kevin Buzzard (May 16 2021 at 10:09):

When we were discussing these things and writing LTE code you suggested eval_add_monoid_hom and I ended up getting really irritated with how long this name was for a function which was appearing everywhere in my code, so I changed it to proj in LTE.

Eric Wieser (May 16 2021 at 10:10):

I assume you're referring to docs#dfinsupp.eval_add_monoid_hom?

Eric Wieser (May 16 2021 at 10:11):

The problem is that proj is really just an alternative for eval; it doesn't solve the "preserves zero" / "preserves add" / "preserves both" / "preserves both and smul" part of the name that is _add_monoid_hom.

Eric Wieser (May 16 2021 at 10:14):

How close to possible is syntax that promotes functions to bundled homs like (function.eval i : _ \to+ _)? Could docs#can_lift help?

Kevin Buzzard (May 16 2021 at 12:46):

I totally agree that proj=eval; I prefer proj because even though iAi\oplus_iA_i is implemented as a function type, it doesn't mean that people think of elements as functions and as the map (ai)aj(a_i)\mapsto a_j as an evaluation. You're also totally right that there is no way to distiguish whether the evaluations is a group hom, a monoid hom or whatever. I'm merely making the point that if you're actually working with graded objects then you use these maps all the time and eval_add_monoid_hom is a _really long name_ for something you're writing everywhere. How about we use notation for this? pr+?

Eric Wieser (May 16 2021 at 14:19):

Oh, I agree that for direct_sum that proj is better than eval. For pi it's a bit of a gray area - proj is clearly appropriate for things like fin 3 -> R, but less clear for arbitrary functions.


Last updated: Dec 20 2023 at 11:08 UTC