The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Benjamin,

 

for pointing out the differences and similarities between type classes, modules and canonical instances to beginners with various backgrounds, order relations might be good choice. It is a topic everybody basically understands, but on which one can show some interesting effects.

An example I sometimes use for explaining this is a red black tree example from Andrew Appel extended to arbitrary types with an order relation. To handle comparison of keys in tree boundary cases, I extend the type and its order relation to a type with a bottom and top element. This can be done with modules, type classes and canonical instances. I think one can the see the advantages and disadvantages of the various techniques best when one has a few levels of abstraction – in the above cases basic order relations – the order relations extended with bot/top and the red black tree using the order relations.

 

What I had most problems with initially is that some type classes have implicit parameters. This works quite well when the nesting level of these parameters is small, but when the nesting of parameters gets deeper one can have the issue that unification takes long, that error messages are hard to understand and that later in a proof one might require certain relations between different parameters of a type class which are not explicit when the initial resolution was done and that an instance is chosen which is not compatible with these requirements, although there is one which would be compatible. The solution is typically to explicitly specify some of the implicit parameters, especially their relation to each other. Another advantage of stating certain things explicitly is that it is easier to understand what actually happens. Let me see if I can find a few examples.

 

Best regards,

 

Michel

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Benjamin C. Pierce
Sent: Monday, June 19, 2017 2:01 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] "Core" Coq typeclasses

 

In preparation for the upcoming DeepSpec summer school, I’m working on putting together an “even gentler tutorial” on typeclasses in Coq.  I’d be grateful for the community’s advice on what are the most important / most used typeclasses in the standard libraries (or in widely used contributed libraries).  I plan to use a couple of these as running examples and make a list of the rest so that people know they are there.

 

More generally, I’d love to hear opinions on pragmatic aspects of typeclasses and how to get newcomers up to speed… E.g.:

• What are the most puzzling gotchas that people new to coq’s typeclasses tend to get stuck on, and what are some good strategies for getting un-puzzled?
• What advice should be given to new typeclass users to avoid getting themselves in trouble?  What are the tradeoffs between typeclasses and other modularity mechanisms in Coq.

Thanks!

 

    - Benjamin

 

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928