The Coq mailing list

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

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