[Agda] Re: Syntax for anonymous functions

[Fredrik Nordvall Forsberg]

Hi Andreas,

On 26/05/11 10:02, Andreas Abel wrote:
> 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?

The syntax with -> and a lambda (plus braces) works, thanks to a trick 
similar to yours for CommaBIds.

The syntax with -> without lambdas will never work, because then we 
can't tell a function space A -> B and an anonymous function x -> e apart.

> My favorites are still:
>
> \ {A = Int} (a , b) y -> ...

This is my favourite as well, but this won't work until we get rid of 
"normal" lambdas, which I don't think we should do before equality of 
function definitions has been sorted out.

In the meantime, I managed to get

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

to work if one excludes the case

\ { x y () }

(but not

\ { true x -> x ; false () }

), that is all absurd pattern matching lambdas must have at least two 
clauses. This works, because the parser thinks the problem is an 
expression like

\ {x y z} -> ...

By disallowing pattern matching lambdas of that form, we keep the parser 
happy. With more work, it should be possible to handle this case 
correctly as well, though.


Similarly, the absurd clause part of the syntax

 >> { p₁ ↦ e₁; p₂ ↦ e₂; … }

clashes with the expression

{ and true false }

(which is a hidden argument evaluating to {false}, thus a valid 
expression). I think \ { ... } is easier to get right.The syntax would 
then (once again) be

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

which I personally think is fine.

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

Adding a (then layout) function keyword is easy (I would assume also 
with "=" instead of "->" as Jean-Philippe suggests), but I'm still not 
convinced of its use -- in what scenario would you use this instead of 
defining a real function or write a small \ { ... }?

>
> 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₂; … }
>>
>
>