The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Do let me know if you dig up the examples you had in mind — I’d love to be able to show people a simple comparison of the three approaches (and I’d love to understand it myself!)…

   - B

On Jun 19, 2017, at 11:23 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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.