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

[Noam Zeilberger]

On 06/05/11 21:26, Nils Anders Danielsson wrote:
> Is the grammar ambiguous? I don't think we should let our tools dictate
> the design of the language.

No of course we shouldn't, it was just a temporary hack to get around
the parsing problems, and now it looks like Fredrik has resolved some
of those problems...

On Sat, May 7, 2011 at 3:54 AM, Fredrik Nordvall Forsberg
<csfnf at swansea.ac.uk> wrote:
>
> No, I've finally convinced our tools that it is not. Thus the syntax is now
>
>   and = \ ( true x -> x ; false _ -> false )

excellent.

> which I, from the response on the mailing list, judge to be the right syntax
> when it comes to '->' vs. '='. What about the rest of the syntax? At AIM
> XIII, we were originally aiming for
>
>   and = \ { true x -> x ; false _ -> false }
>
> (since, as Andreas remarked, "|" is already reserved). Is this the syntax
> we want? (Making it so will involve resolving another shift/reduce conflict,
> but as Nisse says, this shouldn't dictate the design.) Ideally, it would be
> nice if the brackets could be omitted if the definition only contains one
> clause:
>
>   fst = \ (a , b) -> a
>
> However, I can imagine that this would be hard to achieve the way we currently
> do things -- how does the parser know if "\ true -> 0" should be parsed as a
> traditional lambda with a variable named "true" (as current Agda does) or as
> an incomplete pattern matching lambda (as it then probably should, to be
> consistent with "f : Bool -> Nat ; f true = 0")?

So to elaborate on this, again as a sort of temporary solution for the
sake of conservativity, at the AIM sprint we decided to implement
pattern-matching lambda as completely orthogonal to (and syntactically
distinct from) the existing lambda, rather than as a more general
replacement of the existing lambda.  Clearly it should be a more
general replacement.  However, we did not want to break any existing
code that makes use of some of the special characteristics of the
existing lambda.  Besides "\ true -> 0", the more serious issue is
intensional equality.  Currently, Agda gives special treatment to
lambdas: we have

  (\x -> x) == (\x -> x)

yet for two top-level functions f and g defined by the same clauses

f x = x
g x = x

we do not have f == g.  The implementation strategy for the
pattern-matching lambda was to compile it away to a top-level
definition, and so for example two occurrences of "\(x -> x)" (in
Fredrik's new syntax) will not be definitionally equal, since they
will be treated like f and g above.

My opinion is that conceptually there should be no difference between
top-level definitions, pattern-matching lambdas, and the existing
(non-pattern-matching) lambdas.  Lambdas should always be replaceable
by top-level definitions, without affecting typeability.  But this
seems to leave the following options:

1. Definitional equality becomes more extensional, recursively
comparing the bodies of function definitions (e.g., so that f and g
are equal).  I think this should be decidable by a coinductive
algorithm (i.e., to check f == g, check their bodies are equal under
the assumption that f == g), but I don't know about its
computational/conceptual complexity.

or

2. Definitional equality becomes "more intensional", so that we can't
even assert (\x -> x) == (\x -> x).  Really, this would be raising the
question of whether definitional equality is a useful notion at
functional type.

Noam