The Coq mailing list

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

Thank you — that’s super-useful!

If I can take a few more seconds of your time, it would be super-helpful to have a very quick list of the typeclasses that you see as best integrated into the standard libraries or most useful for common Coq developments…  :-)

   - B

On Jun 19, 2017, at 10:39 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi,

The fact that typeclass resolution resorts to unrestricted proof search is a blessing and a curse for sure. Errors tell you only that proof search failed and the initial problem while in general you need to look at the trace of resolution steps to figure out what's missing or, in the worst case, making search diverge. If you are writing obviously recursive instances, not mixing computation with the search (e.g. Unfolding happening in the indices necessary for instances to match), and not creating dependent subgoals then you're basically writing Haskell 98-style instances and should get the same "simplicity". I think for more elaborate use cases (terms in indices, dependencies and computation), when encountering unexpected failure the debug output (Set Typeclasses Debug) is necessary. Testing the logic program, using Checks for example is a good way to explore the proof search results. One can also debug interactively by switching to the tactic mode and looking at the [typeclasses eauto] behavior. We're facing the same issues as logic programming and I don't know of a silver bullet to debug these programs. For common issues a newcomer is likely to get, there are missing instances which can be prevented/tested using some coverage tests, divergence which can be understood by looking at the trace (usually it's because of a dangerous instance like transitivity or symmetry which has to be restricted or removed, and sometimes because of a conversion which makes an instance always applicable), and ambiguity when the user does not get the instance he expected (due to overlapping mainly, priorities can help here).

One advantage of modules is that everything is explicit but the abstraction cost a bit higher as you usually have to functorize whole modules instead of individual functions, and often write down signatures separate from the implementations. One rule of thumb is that if there are potentially multiple instances of the same interface for the same type/index then a module is preferable, but adding more indexes to distinguish the instances is also possible.

My 2 cents,
-- Matthieu

Le lun. 19 juin 2017 à 14:45, Pierre Courtieu <pierre.courtieu AT gmail.com> a écrit :

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