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

[Fredrik Nordvall Forsberg]

Hi,

On 06/05/11 21:26, Nils Anders Danielsson wrote:
> On 2011-05-06 17:50, Noam Zeilberger wrote:
>> See the other email I just sent -- if I recall correctly, the problem
>> was the overloading of "->" as a type constructor (and hence possibly
>> appearing in parser "Expr"s, and hence possibly on the left-hand side
>> of pattern-matching clauses), causing shift-reduce conflicts.
> 
> Is the grammar ambiguous? I don't think we should let our tools dictate
> the design of the language.

No, I've finally convinced our tools that it is not. Thus the syntax is now

   and = \ ( true x -> x ; false _ -> false )

which I, from the response on the mailing list, judge to be the right syntax
when it comes to '->' vs. '='. What about the rest of the syntax? At AIM
XIII, we were originally aiming for 

   and = \ { true x -> x ; false _ -> false }

(since, as Andreas remarked, "|" is already reserved). Is this the syntax
we want? (Making it so will involve resolving another shift/reduce conflict,
but as Nisse says, this shouldn't dictate the design.) Ideally, it would be
nice if the brackets could be omitted if the definition only contains one
clause:

   fst = \ (a , b) -> a

However, I can imagine that this would be hard to achieve the way we currently
do things -- how does the parser know if "\ true -> 0" should be parsed as a
traditional lambda with a variable named "true" (as current Agda does) or as
an incomplete pattern matching lambda (as it then probably should, to be
consistent with "f : Bool -> Nat ; f true = 0")?

Suggestions welcome.

-- 
All the best,
Fredrik