The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi

my biggest problem with typeclasses is the error messages of the unification engine. It is really hard, even for confirmed users, to figure out from the message why some statement can't be coerced to something typable.

Something should be said about typeclasses vs functors/modules but I never came to a clear conclusion about it.

P.

2017-06-19 14:00 GMT+02:00 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