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

[Wolfram Kahl]

On Sat, May 07, 2011 at 04:08:13AM +0100, Darin Morrison wrote:
> On 7 May 2011, at 02:54, Fredrik Nordvall Forsberg wrote:
> 
> >> 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 }
> 
> The second one is the version I prefer since it matches the style used for records whereas the other version would look strange when split across multiple lines.

Since we are all used to juxtaposition binding very strongly,
I would tend to avoid it here, where it is misleading;
I would therefore prefer:

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

Since in Agda, the function type arrow can be used in expressions,
I would also prefer a different kind of arrow,
for example a \mapsto arrow:

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


(And I have to admit that this is also somewhat influenced
 by my pattern matching calculus

   http://www.cas.mcmaster.ca/~kahl/Publications/Conf/Kahl-2004a.html
   http://www.cas.mcmaster.ca/~kahl/Publications/Conf/Kahl-Carette-Ji-2006a.html

 which uses a double \mapsto-style arrow |=>
 which, at least in ASCII, looks better than |->,
 and PMC also has special braces that directly turn
 a sequence of matchings into a (function) expression
 (and uses a thicker bar for alternative):

  and = {|  true |=> x |=> x  ||  false |=> _ |=> false  |}

)


Wolfram