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

[Noam Zeilberger]

On Sat, May 7, 2011 at 9:26 PM, Peter Hancock <hancock at spamcop.net> wrote:
> I generally use
>
>   [ c1 p11 .. p1k_1 |-> ... | ... ] : (x : Coprod)  -> ... x ...

So I guess the point is that (leaving aside the question of
brackets/arrows/etc.) our current notation

  \ ( p11 .. p1k_1 -> e1; ... ; pn1 .. pnk_n -> en)
-- example...
  and = \ ( true x -> x ; false _ -> false )

for a curried function is potentially misleading, with the head
patterns pi1 naturally being read as (k_i-1)-ary constructors.
Indeed, in the current notation we obtain that reading just by placing
extra parentheses around the left hand sides:

 dna = \ ( (true x) -> x ; (false _) -> false )
-- (now true and false are unary constructors for some datatype.)

Is this dangerous?

On the other hand, like Thorsten, I am not a fan of the chain-of-arrows notation

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

because it seems to suggest you're defining multiple nested functions,
whereas we want to define a single function with multiple arguments,
which is different.  For example there is no problem defining 'and' to
analyze its second argument rather than the first:

  and x true = x
  and _ false = false

but the notation

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

seems to describe overlapping clauses of incomplete pattern-matchings.

If the current notation is seen as a problem, again I would propose
something like the following, more general since it also allows
recursive function definitions (but easy to implement given the
strategy of converting to top-level definitions):

 and = the f { f true x = x ; f false _ = false }

Such a notation could work for (potentially-recursive) records as well, e.g.,

 pair e1 e2 = the f { fst f = e1 ; snd f = e2 }

If you want to be explicit that a function/record is non-recursive,
perhaps you could use a keyword that introduces a dummy name, e.g.,

 and = the# { # true x = x ; # false _ = false }

There are probably better choices of keywords here than "the" and "the#"...

> using `|->' for the symbol that segregates a (linear) pattern from the
> corresponding
> rhs, which may contain the variables of the pattern.  I call this co-tuple
> notation,
> when there is more than one |-separated "arm", and functional abstraction
> when the pattern is empty.
>
> I also use (x |-> .. x ..) for simple functional abstraction, occasionally
> ( x : A |-> .. x .. ) if I want to show the type of the domain,
> ( x : A |-> .. x .. : B x) if the codomain is also interesting.

This reminds me of the other peculiarity of the existing lambda in
Agda with respect to top-level definitions, which prevented us from
treating pattern-matching lambda as a proper generalization: type
annotations.  In Agda you are not allowed to put type annotations
inside the left-hand side patterns of definitions (type information
can only come from the declaration), but you are allowed to annotate
lambda-bound variables.  We looked in the agda library and this
feature of lambda was used in a few places, though rarely, and in most
cases the annotation could be removed (some cases were less obvious).

Again my opinion is that there is nothing special about the domain of
a lambda, and that if type annotations are needed there should be a
more general mechanism for annotating terms, not tied to lambda
abstraction.  For example, one approach to type annotations in the
setting of bidirectional typechecking with dependent (refinement)
types is described in section 4 of:

Tridirectional Typechecking
Joshua Dunfield and Frank Pfenning
http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking-TR/Dunfield04_tridirectional-TR.pdf

How does this work in Epigram?

Noam