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

[wren ng thornton]

On 5/6/11 11:26 AM, Noam Zeilberger wrote:
> 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?

I'd support using that character to remove the overloading problem (or, 
since that's been resolved, to avoid any human confusion)--- provided 
it's used uniformly for everywhere we use arrows in this fashion (e.g., 
lambdas, branches of case analysis in Haskell,...).

I'm sure it's old history, but what reasons are there for avoiding the 
use of a period for these kind of binders (as is done in mathematical 
notation)?

-- 
Live well,
~wren