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

[Thorsten Altenkirch]

On 5 May 2011, at 14:50, 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 ...
> 

Also \ x = 0 looks like x should be 0. 

It would make sense to write the top-level definitions using -> but tradition and the fact that arrows are already overused speaks against it.

> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda