[Agda] nameless pattern-matching functions

[Dan Licata]

On Mar07, Nils Anders Danielsson 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.

But agda already doesn't let me refine outer scope variables in a helper
function, at least in this instance:

  data Unit : Set where
    <> : Unit

  data Nat : Set where
    Z : Nat
    S : Nat -> Nat

  data Vec : Nat -> Set where
    []  : Vec Z
    _::_ : {n : Nat} -> Nat -> Vec n -> Vec (S n)

  data Foo : Set where
    F : (n : Nat) -> (Vec n -> Unit) -> Foo

  example : (n : Nat) -> Foo
  example n = F n f where
    f : (Vec n -> Unit) 
    f [] = <>
    f (_ :: _ ) = <>

Z != n of type Nat
when checking that the pattern [] has type Vec n

So I don't see how an anonymous function would be any worse off.  If I
have to generalize the type of the function to do my pattern matching,
then I'd have to name it and give a type sig.  But anonymous
pattern-matching functions would catch a common case when you can
implement exactly the type that's flowing in from the context.

-Dan