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

[Noam Zeilberger]

On Fri, May 6, 2011 at 10:00 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
> It would make sense to write the top-level definitions using -> but tradition and the fact that arrows are already overused speaks against it.

When we were working at this at AIM, the ultimate reason we settled on
the uniform '=' syntax was because we couldn't get '->' to parse.
IIRC this was because of the overloading of '->' as a type
constructor.  Maybe that problem could be resolved by introducing a
new keyword "mapsto"/Unicode character 0x21a6 for anonymous lambda?

Though, another possibility for making the syntax more
uniform/intuitive would be to use "named anonymous functions", i.e.,
something like

  the f . (f x zero = blah | f x one = bluh | ...)

to denote the functional value (potentially recursive) that returns
blah when applied to x and zero, bluh when applied to x and one, etc.
Presumably, such a syntax could be used to define recursive records as
well.

Noam