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

[Andreas Abel]

Hi Karim,

that sounds great, even without with/where!

Concerning concrete syntax, I am hesitant to welcome parentheses as a 
obligatory means to delimit pieces of code that might be big.  I have 
bad memories of SML syntax where you had to wrap a case statement in 
parentheses to disambiguate.  Haskell uses parenthesized lists for 
import and export lists---in my opinion a bad design born out of the 
avoidance of a design and decision for a proper syntax.  I do not have 
to remind you of Scheme...

The discussion of the new syntax at AIM XIII was very short and I think 
the current syntax is the result of

   - making \lambda a layout keyword would break a lot of code

   - the "|" is reserved for parsing with-applications which might
     be implemented in a possible future, so cannot be used
     for separating clauses

   - without parentheses, the new syntax is unparsable

One option was not discussed that I want to bring forward:  Introduce a 
new layout keyword.  One possibility would be "function".  That would 
look like

   and = function
           true  x -> x
           false _ -> false

Without layout:

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

Unfortunately, Agda has no means of doing "without layout" (, yet ?!).

In the absence of layout, I am afraid one-line functions have to fall 
back to your syntax with parentheses.

Can you please remind me why the "->" does not work instead of "=".

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

On another note: records are like functions from fields to contents, so

   record
   { fst = bla
   ; snd = blurp
   }

is like

   function
     fst -> bla
     snd -> blurp

A common syntax for records would be beneficial, because then you could 
define a pair of functions as

   record
     fst x -> bla
     snd x -> blurp

which is possible in Coq and means

   record
   { fst = \ x -> bla
   ; snd = \ x -> blurp
   }

In a common syntax for records and functions, the layout keyword should 
maybe neither "function" nor "record", more something like "cases" or 
"clauses"

   clauses
     fst zero    -> bla0
     fst (suc n) -> blaS
     snd y       -> blurp

That would define a pair of functions, the first being defined by 
pattern matching on its first argument.

Concrete proposal for now:
- Add your syntax, but use -> instead of =
- Also add "function" layout keyword for bigger anonymous functions.
- Postpone fusion with records.

Cheers,
Andreas

On 04.05.11 10:09 PM, karim kanso wrote:
>
>
> On 4 May 2011 16:57, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>     On 5/4/11 5:02 PM, karim kanso wrote:
>
>         On behalf of Noam and Fredrick.
>
>         We have spend some more time working on an extended syntax for
>         lambda
>         expressions. It is currently
>         at status 3. The use of with and where clauses have issues, the
>         where
>         clauses have lambda lifting
>         issues, with clauses have scoping issues.
>
>         We could submit a beta patch that will allow for anonymous case
>         distinctions, but disable the use of with
>         and where clauses inside the lambda terms for now?
>
>     Could you explain what the syntax now is for the lambda with matching?
>
>
> The syntax, thanks to Noam and Fredrick whom tweaked the parser is
> essentially function clauses (omitting the name) delimited by
> semicolon's. So, one could define propositional conjunction as follows:
>
> and : Bool -> Bool -> Bool
> and = \ ( true x = x ; false _ = false )
>
> which is internally translated into
>
> .extlam0 : Bool -> Bool -> Bool
> .extlam0 true x = x
> .extlam0 false _ = false
>
> and : Bool -> Bool -> Bool
> and = .extlam0
>
> The dot being used to keep the namespace hygienic.
> .extlam0 is lambda lifted so we can write:
>
> or : Bool -> Bool -> Bool
> or x = \ ( true = true ; false = x )
>
> All the examples above work, now in the cases where we are having some
> difficulties. A with statement does not work at all, scope checking
> fails with the message "..." is out of scope.
>
> g : Bool -> Bool -> Bool
> g = \ ( x y with (and x y) ; ... | z = ?)
>
> The where statements have an issue when nested under other where
> statements,  causes extra lambda lifting (appears to be done twice).
>
> It is not currently clear if it even a significant advantage to have
> with and where statements inside the extended lambda notation as the
> main motivation as I understand it is to allow anonymous/in-situ case
> distinctions. Any other opinions would be welcome.
>
>
>         On 28 April 2011 15:30, Andreas Abel <andreas.abel at ifi.lmu.de
>         <mailto:andreas.abel at ifi.lmu.de>
>         <mailto:andreas.abel at ifi.lmu.de
>         <mailto:andreas.abel at ifi.lmu.de>>> wrote:
>
>             Hi AIM XIII participants,
>
>             two weeks after the end of this very successful meeting, I would
>             like to know the status of the code sprints which were continued
>             after the meeting.
>
>             @Makoto: I do not remember all the sprints, can I find the notes
>             online somewhere?
>
>             Status:
>               1 = finished
>               2 = almost finished
>               3 = still working, might take some more time
>               4 = indefinitely postponed
>               5 = abandoned
>
>             Sprint                           Leader            Status
>
>               clean up builtins              Simon             1?
>               unquote                        Nicolas           3?
>               first class lambda syntax      Noam               ?
>               mutual blocks                  James             3?
>               installer                      Makoto             ?
>               meta variables                 Andreas           3
>
>               what else?
>
>             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/