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

[Andreas Abel]

On 5/8/11 9:45 PM, Thorsten Altenkirch wrote:
>
> 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.

That's also my preference.

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

With "with-application" in place, this would parse as

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

Meaning

   and true x = "a function type with domain (x | false _) and codomain 
false"

That's bad.  The question to be asked is however, if "with-application" 
should bind that strongly.  One could choose to let with application 
bind so weakly that one almost always requires parentheses around.  So 
to get that mis-parse of above you would have to type

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

However, I would not want to be the one having to implement the parser 
for with-application and clauses separated by "|".

Concering juxtaposition-as-application, I must say that I am not really 
fond of the (x y : Nat) -> ... syntax, because that looks like an 
application (x y) in my cerebral pattern matcher.  Yet we have it, and 
so we should also have

   \ x y -> ...

And Haskell also has it.  And the MLs.

Cheers,
Andreas



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