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

[Andreas Abel]

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 ...

better.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/