Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page