The Coq mailing list

[Sergey Goncharov <sergey.goncharov AT fau.de>]

Dear Xuanrui,

On 18/01/2020 08:08, Xuanrui Qi wrote:
> > In Agda one can reuse names of fields in records, while in Coq that
> > yields an error
>
> I'm not sure this is always desirable. Shadowing of field names can be
> confusing at times so I'd not always call this a "usability
> improvement".

Maybe I do misunderstand something, but for example with

--------------------------------
open import Data.Nat

record man (A : Set) : Set where
  field
    height : A

record woman (A : Set) : Set where
  field
    height : A

joe : man ℕ
joe = record { height = 180 }

jodie : woman ℕ
jodie = record { height = 175 }
--------------------------------

(man.height joe) and (women.height jodie) work as expected and 
completely satisfactory to me.

-- Sergey


> Meanwhile, I do have my opinion on how Agda is better than Coq, but IMO
> it's not due to the design of the theorem provers, but rather the fact
> that Agda has more edit-time utilities and tool support. I'd like to
> share my Coq Workshop 2019 slides (& accompanying abstract) where I
> elaborate on the ergonomics of Coq programming:
>
> https://www.xuanruiqi.com/assets/coqws2019_long.pdf
> https://www.xuanruiqi.com/assets/coqws2019_slides.pdf
>
> -Xuanrui
>
>
> On Fri, 2020-01-17 at 20:33 +0100, Sergey Goncharov wrote:
> > On 17/01/2020 20:06, Agda Guru wrote:
> > > Agda is better
> >
> > This looks like a start of a new amusing thread. I am willing to
> > believe
> > that Agda is better, but I would be happy if someone helps me to
> > rationalize this subtle feeling, in particular by going beyond this
> > list
> > https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq
> >
> > Let me start. Foundational issues aside, Agda seems to be better
> > designed, as a programming language, in particular, as a recently
> > learned:
> >
> > 1. In Agda one can reuse names of fields in records, while in Coq
> > that
> > yields an error:
> >
> > Parameter X : Set.
> >
> > Record some_record : Set :=
> > {
> >     field_name : X
> > }.
> >
> > Record some_other_record : Set :=
> > {
> >     field_name : X
> > }.
> >
> > ----> "Error: field_name already exists."
> >
> >
> > Cheers,

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature