coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Andrew Appel <appel AT CS.Princeton.EDU>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Canonical Structures vs. Type Classes vs. Module Systems
Date: Fri, 13 Apr 2018 11:29:28 -0400 (EDT)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=appel AT CS.Princeton.EDU; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=None smtp.helo=postmaster AT yellowcard.cs.princeton.edu
Ironport-phdr: 9a23:BS5k0hzF7MK4YFvXCy+O+j09IxM/srCxBDY+r6Qd2+gXIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHmiCkJKT03/2PZisJtg61UvBOhqRtjw4PPeo6ZKOZxc7nHcN8GR2dMWNtaWSxbAoO7aosCF/YMPeBFoInnuVQPowa1CBW0BOP31DBIgmL90Kog3OQ5CQHJwgggEskQvXrJttn7Lr0SUeGzzKbU0zrDc/RW2THn5IbHfB4ur+iBULRtesTfzkkvEhnKjlSWqYH9MDOV1/gNs2iG7+V7T+6gl2knqwR3rzOyxckskpHEip8Lxl3H7yl13Zs5KcOiREJmb9OpEYFcuiCbOoduX88vTH1ktDwnxrAFpZK3ZjYGxZQnyhLFdfCKfJWE7gr+WOqPIjp0nm9pdK+hixqo7EStxO/xWtO73VpXqCdOj8PCuWoX1xPJ78iKUvt98Vml2TaIzw3S6v9LIUQwlarcJZ8u3qQ/loAOvkjZAiD2g1/6jLeMdkUl/Oin9/roYqnhpp+aLYN7lBzxMrk2lsy+B+Q3LBQOUnCG9eii17Dv51D1TKhUgvEsj6XUvpHXKd4aq6O4GwNV15ws6xe7DzeoytQYmnwHIUpfdxKfl4jmJVXOLevkAvekmVisiC1rx/HAPrL9HJrNMn/DkLH7cblj9kFc1RI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioynkZYdq2017MWbmq5F7JoORa3e33p1/4HHX0HoUIXVPTnjBXWWCZLanKadJl63is6DomrEYDFAK2BverSj2+AApRKazUeWRi3GnDyetDcAqZeWGepOsZk1wc8e/2kQo4l2wupsVaqmbF8aPLO+ysTuI7k0p546/CBzEhupwwxNNyU1iS2d08xhnkBHm9k95s5mVZ8zFyOza9+xdF0KI4Lvq4bYkIBLZfZitdCJZXyVwbGJIbbWVuiRtK5CjgrQpQ62JkWeUd7ENi+iRaF0ia3UecY

From: "Yao Li" <liyao AT seas.upenn.edu>

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?

Here is an example of the weakness of typeclasses:

https://github.com/coq/coq/issues/7175

That issue report cites a paper,

Gonthier et al., "How to make ad hoc proof automation less ad hoc", JFP 23 (4): 357–401, 2013.

that explains a bit why canonical structures are used in mathcomp.

-- Andrew Appel

[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