Naming: eval vs apply

Stream: general

[Eric Wieser]

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]

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]

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

[Anne Baanen]

/poll eval or apply?
eval
apply

[Anne Baanen]

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

[Mario Carneiro]

I don't understand any of these questions

[Mario Carneiro]

for me apply means function application

[Anne Baanen]

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

[Mario Carneiro]

eval seems fine since it's backwards

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Eric Wieser]

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]

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]

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

[Johan Commelin]

Maybe dot-notation will not work :sad:

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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]

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

[Kevin Buzzard]

I totally agree that proj=eval; I prefer proj because even though $\oplus_iA_i$ is implemented as a function type, it doesn't mean that people think of elements as functions and as the map $(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]

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.