[Agda] no-eta-equality

[Ulf Norell]

On Thu, Sep 29, 2016 at 4:47 PM, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:

> On Wed, Sep 28, 2016 at 03:16:56PM +0200, Nils Anders Danielsson wrote:
> > On 2016-09-28 15:07, Andrea Vezzosi wrote:
> > >However you should also consider the following version, so that
> > >(suc'Rd (rd a n)) does not reduce by itself, but only when projections
> > >are applied to it.
> > >
> > > [...]
> >
> > I think sucRd is more readable than suc'Rd, and I don't think we should
> > encourage people to obfuscate their code in order to make it faster. A
> > better alternative might be to devise some way to instruct Adga to do
> > this kind of rewrite behind the scenes.
>
> Strongly agreed!
>

Unless you're using lots of nested sigmas (in which case you're on your
own),
I don't think the main problems are coming from the kind of examples where
you'd rather use a constructor, but from the big algebraic structure kind
of examples
where copatterns are nicer anyway.

But of course, feel free to suggest some concrete ideas for what could be
done
behind the scenes and what it would look like in the code. I'm slightly
worried that
people would get surprised by examples like

{-# MAGIC_REWRITE_INTO_COPATTERNS Σ #-}

foo : (x , y) ≡ (x , y)
foo = refl   -- error since the two pairs got rewritten into two different
copattern definitions

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160929/7bdaffbf/attachment.html