Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]

[Noam Zeilberger]

On Thu, May 5, 2011 at 11:32 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> One option was not discussed that I want to bring forward:  Introduce a new
> layout keyword.  One possibility would be "function".  That would look like
>
>  and = function
>          true  x -> x
>          false _ -> false

Remember that the main use for anonymous lambda is to define a
functional value to pass to a higher-order constructor/function,
without having to give a type signature (since it is pushed down from
the constructor/called function).  It is not clear to me how this
would work with the layout syntax.  For example, suppose "bar" is a
higher-order constructor/function, and we build the following
expression using anonymous lambda syntax:

  foo (bar \(true x = x | false _ = false)) 0 1 2

How would you express this with an alternative syntax?

> Can you please remind me why the "->" does not work instead of "=".
>
>  and = \ ( true x ->x ; false _ -> false )

See the other email I just sent -- if I recall correctly, the problem
was the overloading of "->" as a type constructor (and hence possibly
appearing in parser "Expr"s, and hence possibly on the left-hand side
of pattern-matching clauses), causing shift-reduce conflicts.  Would
it be reasonable to introduce another kind of arrow to remove the
overloading?

Noam