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

[wren ng thornton]

On 5/5/11 9:50 AM, Andreas Abel wrote:
> On 05.05.11 3:38 PM, Stefan Monnier wrote:
>>> Can you please remind me why the "->" does not work instead of "=".
>>
>> "->" is consistent with the current \lambda, but "=" is consistent with
>> the top-level definitions. Your "merge record and function" drift seems
>> to be arguing for the use of "=" rather than "->" since it makes it
>> closer to top-level definitions.
>
> Well, I have been brought up with using "=" for equations ;-), so I think
>
> f x zero = bla
>
> is fine for top-level definition, since the lhs actually reduces to the
> rhs (if we are lucky...) and they are treated equal by the type checker.
>
> But
>
> \ x zero = bla ...
>
> does not look so intuitive. We are speaking of a function that maps
> (x,zero) to bla (modulo currying), so I find
>
> \ x zero -> bla ...


For what it's worth, I agree with these aesthetics. There's a difference 
between defining a system of equations and exhibiting a term which 
happens to be a functional map. Using = to separate the lambda bound 
variables from the body just feels wrong.

To me, the distinction is a lot like the distinction between morphisms 
and exponential objects. Sure, it's often beneficial to pretend they're 
the same things, but there's a moral difference between them and it's 
good to keep them straight.

-- 
Live well,
~wren