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 noncommutative 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 possiblybundled function type and Y
is a definitely bundled function type. Unfortunately, the naming is currently very adhoc.
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:
``

Use
X.apply_Y
for all cases. The above functions becomepi.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₂

Use
Y.apply_X
for all cases. The above functions becomemonoid_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 computersciency 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 dotnotation 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