lambda temptation

Stream: general

[Patrick Massot]

Do I get kicked out of this forum by CS people if I use

notation ` ` binders `↦` F:(scoped f, f) := F
#check (x y) ↦ x + y + 1

[Patrick Massot]

I learned to much about notations on Saturday

[Patrick Massot]

With great power comes great responsibility

[Reid Barton]

I like it. Makes things a little friendlier for mathematicians who aren't used to λx y,

[Simon Hudon]

Actually, the CS people had a meeting and your past violations are already sufficient to get you booted out

[Simon Hudon]

But seriously, I understand it's tempting because it's a more traditional notation but I think it's worth re-examining conventions every now and then. In mathematics, the same idea (bound variables) seems to be reinvented over and over and over. If you look at notations like indexed unions, argmax and sums, there are a lot of vary different conventions in application. I think it's worth streamlining those notations and writing conceptually similar things with similar notations.

[Mario Carneiro]

I'm not sure I'm ready to give up ↦ as an available notation, arrows are hard to come by

[Scott Morrison]

I actually agree with Simon, that it's not a bad thing to ask mathematicians to get used to using lambdas. Conversely, I would be upset by Mario using ↦ for something other than "maps to"! :-)

[Mario Carneiro]

It's conceivable that something that is morally "maps to" but isn't literally lambda could come up, like ZFC maps to producing a Set

[Patrick Massot]

Actually I think the unicode thin space at the beginning of the notation is worse than the Church sacrilege. But I don't know another way. Maybe I don't know enough about notations in the end.