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

[Thorsten Altenkirch]

On 7 May 2011, at 14:56, Wolfram Kahl wrote:

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

This looks very ugly and not very consistent with the rest of the Agda syntX. 

Btw, I haven't yet understood why we cannot have 
and = \ ( true x -> x | false _ -> false )

Thorsten

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