[Agda] nameless pattern-matching functions

[Noam Zeilberger]

On Fri, Mar 07, 2008 at 04:48:50PM +0000, Nils Anders Danielsson wrote:
> On Thu, Mar 6, 2008 at 12:49 PM, Noam Zeilberger <noam+agda at cs.cmu.edu> wrote:
> >  Would it be tricky to extend Agda to allow pattern-matching in
> >  nameless functions?
> 
> In the simply typed case I don't think it would be very hard (you may
> have to give a type signature for the domain of the function).
> However, in the dependently typed case matching on an expression can
> lead to variables in an outer scope becoming instantiated. You may
> have noticed this when using "with", for instance. One could invent
> some syntax which takes this into account, I suppose, but I fear it
> would be rather heavyweight.

I guess I'm assuming a restriction to bidirectional type-checking.
With such a restriction, this problem would not arise, because you
would not allow any expressions (\x -> e1) e2.  You could only define
an anonymous function in order to return it in a value (like in my
example, where it is wrapped with the constructor Bar), or to pass it
to a named function (or other type "synthesizing" object).

Isn't Agda already pretty close to bidirectional type-checking, since
there is no case construct?  In fact, is "(\x -> e1) e2" the only
exception?

Noam