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

[Nils Anders Danielsson]

On 2011-05-07 12:10, Noam Zeilberger wrote:
> 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.

I agree.

> 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.

ΠΣ implements something like this. Having proper α-equality for (more)
definitions seems like a good thing.

> 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.

This doesn't seem appealing to me.

-- 
/NAD