[Agda] Re: Syntax for anonymous functions

[Andreas Abel]

On 26.05.11 11:36 AM, Jean-Philippe Bernardy wrote:
>>   function
>>      {A = Int}  (c x)         y ->  ...
>>      {A = Bool} (d x (a , b)) y ->  ...
>
> I like the "function" thing too; but please use the "=" sign there.
> This means more consistency (and "manual lambda lifting" easier).

There was already a longer discussion on using "=" in this context on 
the Agda list.  It may make lamdba lifting a bit easier, but if you want 
to make a local function global you have to change the code anyway, you 
have to add the function identifier in the front everywhere.

The main concern with using "=" is that "bla = blurb" should really mean 
definitional equality, and using it for abstraction creates bad parses 
in my mind, and the mind of others that are involved in this discussion. 
  Sorry, but

   function
     h true = long
       piece
       of
       code
       ...
       pages
       later
     h false = ... h ...

looks to me as if you defined the value of

     h false

That will cause endless confusion.

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/