coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Yao Li <liyao AT seas.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems
Date: Thu, 12 Apr 2018 11:48:29 -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 mx0a-000c2a01.pphosted.com
Ironport-phdr: 9a23:MQo7QRbJ11OqnwUzs2Tpk3P/LSx+4OfEezUN459isYplN5qZoM25bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57G7YhdF+gqFVrhy/oBJy2JTbbJ2QNPdkfqPRYdEXSGxcVchRTSxBBYa8YpMNAOUbOuZTso/zp1oTpha5AQmsBePuxSVPhnLtxq01zf4uERrc0Aw9B9IBrnLUrNPvOKgMTO+10bDFwDPeZP1VwTfw8JXEfx8irP2WQL59cMTcxVMyGw7Fk1mcs4joMy2N2ugQsmWW7/BsWf+xh2MpsQ19vCajy8M2hoTNmo4YzE3P+z9jz4YvP9K4TVZ2Yd66H5tUsCGXL452Q8w+T25yoSo21qEKtYKncyQU0psr2wPTZ+afc4iQ4hLjU/2RIStmi314Yr6wmxGy8U24xu39UMm7zkpKozJYntTDtX0BzQHf58mJR/dn40us2SuD2xrX5+1aOUw0kLDUK58lwr4+jJoTtkHDEzfymEX3jK6ZbEIk9/Oz6+v5eLrmvYWQN5Jsig7gNKQunNazDvolPQgTR2Sb4/iz1KX//U3lR7VHluE5kq7AsJzDOcsborO5DBRO34Y46xe/Ci+m384CkXkGKlJFYhOHgJLzN1HAOvCrRcu41l+riXJgw+3MFrznGJTEaHbZw5n7erMo2kdbgC4yhYRb5oNdDZkaLfvoHFLpudreSBI1LlrnkK7cFNxh29ZGCiq0CaiDPfaK6A7a1qcUO+CJIbQtlnP4Ivkh6eTpiCZny0QQdLLvwIMabnb+E/h7cRzAPSjcx+wZGGJPhTIQCfTwgQTcAyVebm30Qrox4Dd9BY67X9+aG9KdxYeZ1SL+JaV4I2BLDlfWQSXtZ92NHq9UMCnIK5c41CQcVb+6V4ItkxqpsV2ixg==

Dear All,

This may be an old question, but I haven’t seen many documented discussions. Assia Mahboubi and Enrico Tassi’s Canonical Structures for the working Coq user is great, but it still does not answer some questions I have.

In particular:

Mahboubi and Tassi mentioned that type classes and canonical structures use different search engines: type classes’ search engine is ad hoc, and canonical structures’ is based on unification. But what difference does that make? Is there something you can do with type classes but not with canonical structures, or the other way around?
How do people usually choose among canonical structures, type classes, and module systems? Do you have some specific use cases that only one of them is most suitable? Or do you think people should only use one of them (and which one would it be)?

Best,

Yao

[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