Zulip Chat Archive

Stream: maths

Topic: Notation for `linear_pmap`


Moritz Doll (Jul 28 2022 at 19:32):

I think the time has come that I really want to have notation for linear_pmap R E F, but I have no good idea. The natural choices would be E →ₗₚ[R] F or E →ₚₗ[R] F, but lp feels very wrong and I am not convinced about pl either. Are there maybe some good-looking arrows that could be used in conjunction with l?

Yaël Dillies (Jul 28 2022 at 19:33):

A dashed arrow, to illustrate that it's partial?

Moritz Doll (Jul 28 2022 at 19:37):

this one would be nice, but in VSCode it looks almost identical to the usual arrow.

Moritz Doll (Jul 28 2022 at 19:37):

or am I just blind?

Moritz Doll (Jul 28 2022 at 19:40):

I guess this one is used already

Yaël Dillies (Jul 28 2022 at 19:43):

Moritz Doll said:

this one would be nice, but in VSCode it looks almost identical to the usual arrow.

Actually I find them more different in VScode than on Zulip.

Anatole Dedecker (Jul 28 2022 at 21:09):

Why not stick with the →. notation from docs#pfun ? So something like →ₗ. ? Or is it too subtle ?

Moritz Doll (Jul 28 2022 at 21:32):

because I did not know that that exists :grinning:

Yaël Dillies (Jul 28 2022 at 21:40):

Is docs#linear_pfun actually implemented with pfun?

Anatole Dedecker (Jul 28 2022 at 21:40):

No (docs#linear_pmap)

Yaël Dillies (Jul 28 2022 at 21:41):

Sorry, I am writing this from a brick (aka my phone).

Yaël Dillies (Jul 28 2022 at 21:42):

Then that sounds like a semidangerous association of symbols.

Moritz Doll (Jul 28 2022 at 21:57):

Why do you think this is semidangerous? I don't think the two definitions will ever be used in the same file

Yaël Dillies (Jul 29 2022 at 11:20):

Semidangerous is not dangerous! Otherwise it wouldn't be called semidangerous.

Moritz Doll (Jul 29 2022 at 11:38):

but I've asked why it is semidangerous. and could you define that?

Yaël Dillies (Jul 29 2022 at 11:39):

Because I can see people finding both and assuming linear_pmap is implemented using pfun, but it's a mild concern, really.

Frédéric Dupuis (Jul 29 2022 at 12:30):

I don't think we should worry about this, you should never assume anything about implementation details from notation anyway.

Moritz Doll (Jul 29 2022 at 13:13):

fyi the PR is here #15751

Mario Carneiro (Jul 29 2022 at 18:52):

I don't think it's all that misleading to associate this with pfun. It very naturally induces one

Mario Carneiro (Jul 29 2022 at 18:53):

I would argue this is the "natural generalization" of pfun to linear maps

Moritz Doll (May 31 2023 at 14:25):

@Jireh Loreaux mentioned in a PR that the current E →ₗ.[𝕜] F looks too much like E →ₗ⋆[𝕜] F in VSCode, does anyone else have this issue?

Jireh Loreaux (May 31 2023 at 14:27):

A simple solution might be to reverse the order: E →.ₗ[𝕜] F instead of E →ₗ.[𝕜] F

Jireh Loreaux (May 31 2023 at 14:29):

And to be clear, it's not that I can't tell the difference at all on my machine, it's just that I have to do a double take and think about how the characters .and normally render on my screen, which seems suboptimal.

Jireh Loreaux (May 31 2023 at 14:31):

(Alternative solution for me: get a bigger screen or better eyes! :rofl:)


Last updated: Dec 20 2023 at 11:08 UTC