[Agda] Pie in the sky (was: Again, a question on records)

[Benja Fallenstein]

Hi Samuel,

On Mon, Sep 20, 2010 at 4:48 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> Wow. What a great idea! If Agda were to have this feature, it would
> become my all-time favorite language instead of... well, instead of
> current Agda.
>
> I must insist. I am really enthusiastic about this feature. Like, if
> the Agda developers refuse to put it in, I'll just have to fork and
> attempt to add it in myself.

It's great to see that I'm not the only one who'd really, really like
to see this! :-)

> please don't have an obvious and true reason why something like this
> could never work,

The non-injectivity of type constructors could be a problem from a
certain perspective, but it seems to me that it's acceptable for a
type class system to operate on syntactic normal forms instead of
actual values -- i.e., in

record Show (X : Set) : Set where
    field show : X -> String

I'm not sure we can prove Show is injective, but it seems sensible
that a type class system should be able to treat Show A as different
from Show B.

- Benja