Zulip Chat Archive

Stream: general

Topic: lambda temptation


view this post on Zulip Patrick Massot (Apr 24 2018 at 21:29):

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

view this post on Zulip Patrick Massot (Apr 24 2018 at 21:30):

I learned to much about notations on Saturday

view this post on Zulip Patrick Massot (Apr 24 2018 at 21:30):

With great power comes great responsibility

view this post on Zulip Reid Barton (Apr 24 2018 at 22:05):

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

view this post on Zulip Simon Hudon (Apr 24 2018 at 23:26):

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

view this post on Zulip Simon Hudon (Apr 24 2018 at 23:30):

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.

view this post on Zulip Mario Carneiro (Apr 25 2018 at 00:10):

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

view this post on Zulip Scott Morrison (Apr 25 2018 at 00:49):

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"! :-)

view this post on Zulip Mario Carneiro (Apr 25 2018 at 00:55):

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

view this post on Zulip Patrick Massot (Apr 25 2018 at 07:04):

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.


Last updated: May 15 2021 at 22:14 UTC