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

[Patrik Jansson]

Coq has something similar called canonical structures which are used
to guide type inference to the "right / canoniclal / simliest" choice
in cases when there are more than one possible answer. See 2.7.15 in
[1] for inspiration.

[1] http://coq.inria.fr/refman/Reference-Manual004.html

/Patrik

PS. I just learnt about this today in a talk by Georges Gonthier so
Iäm not the right person to ask if you want to know more.

2010/9/20 Benja Fallenstein <benja.fallenstein at gmail.com>:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>