coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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!Here is an example of the weakness of typeclasses:
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?
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
- 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, John Wiegley, 04/12/2018
Archive powered by MHonArc 2.6.18.