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

[Noam Zeilberger]

On Mon, May 9, 2011 at 4:28 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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.

To nitpick, actually, neither SML nor OCaml has notation for defining
an anonymous curried function with an array of arguments, only with a
single argument ("fn x => fn y => ..." and "fun x -> fun y -> ..."
respectively), which again is different from the point-of-view of the
semantics of pattern-matching.  It doesn't matter too much because you
can just use uncurrying and define the same function by
pattern-matching on a tuple instead.  Still, the combination of
multiple arguments with pattern-matching seems to be new notational
territory.

Noam