coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems

From: Yao Li <liyao AT seas.upenn.edu>
To: John Wiegley <johnw AT newartisans.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems
Date: Fri, 13 Apr 2018 11:07:25 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=liyao AT seas.upenn.edu; spf=Pass smtp.mailfrom=liyao AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mx0b-000c2a01.pphosted.com
Ironport-phdr: 9a23:EsST8R8XSLLrrv9uRHKM819IXTAuvvDOBiVQ1KB30e0cTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsGSmVOQ8hfVy5ODI2zYYUMAeoPI+FWopLhp1sXqBuyGQmsCP/txzJOm3T43bc60+MkEQze3gMvBdUOu2nSotX0KawfVuS1zKjIzDrZaPNbwiz955bSfRA6u/2MQKpwftTXyUkpDQ/KkEifqZH8Mj6Ty+8DvW+b7+96WuKujW4qswdxrSahx8g2kInJmoMVykve+iV/24Y5P8G3SEl+YdOiDZBetDmaOpNrTs4tQGxkojs2x7wItJKhYSQHyJQqywTRZvGGa4SE/xPuWeaLLTtlmn5odqiziwiv/UWh0OHwSNS43VBXpSRfiNbMrGoC1xnL58iHVPR9+kCh1C6K1wHc9u1LOlk4mbbHJ5I93rE8iIAcvVjeEiPsgEX2lK+WdkI/+ui09evof6/qqYObN49xkg3+M6IuldKjAekgLwQDUGuW9f6h2LDi80D1WqhGg/02n6XDvp3XJNwXpqujDA9U1oYj5Qy/DzCj0NkAmXkHLVJEdwiAj4XyIFHBPur3Deylj1SxiDdk2fbGPrv7DprTM3fDja/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2PfLPgjr8HvgHA9lE5VKauu3Z0IQHa1Af18P0SCaHz3xNwGFDFZkBA5SbnbgVrKdT8bM3KzTqs7zio2AZngEJ/OQIbrjbCcinToVqZKb3xLXwjfWUzjcJ+JDrJVMHrLc51R1wccXL3kcLcPkBSntQv00b1id7SG4SARrtT+zNVz4avemQxgrGUoXfTY6HmESiRPpk1NXyU/hf4tukF00RGeyaV+hbpVGcEBv6oUADd/DobVyqlBM/63Wg/FeY3ZGlO2Gt/jWWlpRYg4m4ZIe159HM6+gxyF1C2vUecY

That is a very good argument. Thanks!

Still I wonder what’s the reason that some libraries like mathcomp choose to
use canonical structures? What are the advantages of them comparing with type
classes?

Best,
Yao

> On 12 Apr 2018, at 3:05 PM, John Wiegley
> <johnw AT newartisans.com>
> wrote:
>
>>>>>> "YL" == Yao Li
>>>>>> <liyao AT seas.upenn.edu>
>>>>>> writes:
>
> YL> 2. How do people usually choose among canonical structures, type
> classes,
> YL> and module systems? Do you have some specific use cases that only one of
> YL> them is most suitable? Or do you think people should only use one of
> them
> YL> (and which one would it be)?
>
> I usually choose type classes because: The errors I get from misusing
> canonical structures continue to mystify me, and module functors do not
> extract to Haskell. Type classes are at least familiar, allow for setting
> priorities, and come with Show Typeclasses Debug.
>
> --
> John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems, Yao Li, 04/12/2018
- Re: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems, John Wiegley, 04/12/2018
  - Re: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems, Yao Li, 04/13/2018
    - Re: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems, Andrew Appel, 04/13/2018
    - Re: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems, Matthieu Sozeau, 04/13/2018
    - RE: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems, Soegtrop, Michael, 04/13/2018