[Agda] Re: Syntax for anonymous functions

[Andreas Abel]

Well, I think having a "function" keyword is not a bad thing, we already 
have the "record".  My intention was to have it as layout keyword for 
anonymous functions that exceed one line.

My gut feeling is that syntax is getting a bit to diverse now.  If we 
embrace the |->, we should drop the \lambda (that would make a function 
syntax similar to scala).  On the other hand, \lambda is useful for 
saving parentheses, similar to the $ in Haskell.

   Sigma A \ x -> B x

To get back to an older question of Nisse:  Is the syntax with -> 
instead of |-> ambiguous or is it just that the LALR parser cannot 
handle it?

My favorites are still:

   \ {A = Int} (a , b) y -> ...

   function
      {A = Int}  (c x)         y -> ...
      {A = Bool} (d x (a , b)) y -> ...

Cheers,
Andreas

On 25.05.11 11:26 AM, Nils Anders Danielsson wrote:
> On 2011-05-24 21:52, Fredrik Nordvall Forsberg wrote:
>> This is a bit heavyweight for a small function, though, so we have also
>> introduced the syntax
>>
>> (a , b) |-> a
>>
>> for one clause functions. The Unicode-inclined can use \mapsto in the
>> emacs mode.
>
> Adding both function and ↦ as keywords seems excessive to me. Would the
> following syntax work?
>
> { p₁ ↦ e₁; p₂ ↦ e₂; … }
>


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