The space after the lambda inserted by the formatter always struck me as weird and annoying. Now I can articulate the reason: logically, what follows after a lambda is a part of the lambda abstraction, not the next argument to the function. If we put a space after a lambda it looks as if the lambda itself were a standalone function argument.
Compare:
partition \ {y := y < x} xs
with
partition \{y := y < x} xs
The second makes it clear that \{y := y < x} is one thing, and not two things \ and {y := y < x}. Another way to see this is that the lambda binds stronger than application to whatever follows it. An analogous situation is with the record update/creation notation, where we for this reason don't put a space before @: we write record@{x := y} to make it clear that this is one thing, and not two arguments record and @{x := y}.
The space after the lambda inserted by the formatter always struck me as weird and annoying. Now I can articulate the reason: logically, what follows after a lambda is a part of the lambda abstraction, not the next argument to the function. If we put a space after a lambda it looks as if the lambda itself were a standalone function argument.
Compare:
with
The second makes it clear that
\{y := y < x}
is one thing, and not two things\
and{y := y < x}
. Another way to see this is that the lambda binds stronger than application to whatever follows it. An analogous situation is with the record update/creation notation, where we for this reason don't put a space before@
: we writerecord@{x := y}
to make it clear that this is one thing, and not two argumentsrecord
and@{x := y}
.