## 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.

Last updated: May 14 2021 at 02:15 UTC