Typeclasses: considered harmful? Idiomatic?

I just read the typeclasses section of software foundations part 4 (QuickChick). I’m familiar with type classes from Haskell and Scala, but it seems like the Coq ones are very powerful…but the lack of overlap checking seems very dangerous. I’m curious what is considered a best practice in Coq. Limited use in modules only? Are typeclasses exposed as parts of APIs? Are there ways to manage the non-nondeterminism and potential overlap in finding instances? The idea that you could add a library and your typeclasses change underneath you seems…bad. Maybe qualified imports or something? Hint database management? Priorities seems like it would be brittle across libraries (but fine within a library) The section itself does mention issues, and even has discussion from members of the community, as well mentions some papers discussing other methods, which I will def read, but thought I’d ask here. Not sure if things have moved at all. The community discussion they include does not really make me feel better about typeclasses in Coq!

Even in Haskell, which has the strongest restriction (unique), some people believe typeclasses should never be used (though this is considered somewhat extreme, I think). In Scala, where you can’t have conflicts at the same level, it is idiomatic to do a lot to get the typeclass search to work properly and it can be a source of weird bugs (which are quite similar to what is outlined in the community discussion at the end of the section, though if anything the Coq case is even worse than in Scala with the potential for badness).

I appreciate any illumination!


First of all, Coq does not have a single idiomatic style — but “using typeclasses” is one of the main styles used by respected authors.
Using canonical structures is another, used by other respected authors, but with subtle tradeoffs.

Other people are much more qualified than me on this topic, but since you come from the Haskell world, I figured I could sketch a comparison from my experience in Haskell and Coq (I’ve also used Scala).

TLDR: concerns exist, but IME they seem mostly disjoint from what you discuss. It’s also much less clear how typeclasses should behave in a proof assistant, how they behave in Coq, and how exactly the two align.

Coq typeclasses for Haskellers

I haven’t really seen typeclass issues affect correctness, once the code compiles — typically, correctness proofs should catch any problems, since they can guarantee so much more than plain non-dependent typechecking.

Typeclass Search Performance

The main concern is keeping instance search fast enough: when possible, you make typeclass search “syntax directed” by creating instance carefully. If an instance is too generic, you can turn it into a normal lemma and apply it by hand, or write a custom Hint Extern that can use arbitrary Ltac to decide whether it’s safe to apply it. When I make mistakes, I often can fix it as soon as it causes problems.

but the lack of overlap checking seems very dangerous

I’ve never seen that cause problems in practice because of conflicting instances. And if it did, I guess you’d likely notice when your proofs break.

Ecosystem size and structure

Maybe I haven’t seen this because I’ve never combined two independent libraries that use the same typeclasses; at best, I’ve seen libraries use some of the few typeclasses from the Coq stdlib. Probably things are different in the CompCert ecosystem, since many different projects use it?

Actual conflicts between libraries

Combining two libraries absolutely can cause problems in Coq, but mostly for different reasons: you can’t Import together two libraries with conflicting notations (but you can at least load them via Require, and use them in different scopes). And as soon as you load a library via Require, it can change global mutable state in Coq itself (say via flags), which affects code that is processed later. That’s far from elegant, and an actual problem, but I’m afraid it’s pretty baked-in in Coq. As a workaround, you can always try to change again those flags.

Now such global flags can affect how typeclass search proceeds in some cases — they can change which algorithm is used, or whether certain definitions should be expanded or not during search.
In Haskell, instead, definitions are either always expanded (type synonyms, type functions) or never expanded (datatypes, classes themselves).

Instances are imported transitively

As a special case, typeclass instances are made available upon Require, not Import. In other words, the instances in scope are usually all those defined by transitive imports. That’s far from ideal, but also hard to change.
Except ones that somebody removes — that’s possible too, via Remove Hints, whenever you realize somebody else provided a questionable instance — but I can only remember one use of this.

Why orphan instances are fine: No global uniqueness of instances is needed

Let me point out that one concern from Haskell can be avoided (even tho it doesn’t seem you mentioned it): having non-unique instances is safer, so “orphan instances” are much more acceptable (and in fact, they’re often necessary). If you are defining a type of FinSet T that depends on an instance o of Ord T, you can use dependent types to prevent mixing FinSet T that use different orders — the actual type will be @FinSet T o (tho the o itself will likely be kept implicit, so you’ll just write FinSet T) so mixing @FinSet T o1 with @FinSet T o2 will lead to a type error.
Combining multiple instances of Ord T for the same T is still likely to lead to confusion, but that will be caught by the typechecker.

I checked std++ (my go-to typeclass-using library) for examples; while it avoids order-based data structures there, its main general-purpose collections (gset and gmap) are indexed by an encoding function, represented via typeclass Countable.

Why orphans are currently necessary in Coq in practice

Orphans aren’t forbidden or discouraged, and the typeclasses in use are not standardized. So as soon as you combine a typeclass TC from a library A with a definition D from library B, and you need an instance for TC D, it’s likely it appears in neither library — but luckily, you can write it yourself or provide it in a glue library. And yes, forbidding orphans might force people to work around this, tho it’s not clear there’s a good way to do that (even in Haskell).


This was a really excellent discussion. Thank you so much.

It’s clear I need to spend more time with the sort of…glue of Coq. Via software foundations I’ve largely spent time understand proofs, but I really need to understand how like…things are compiled, how dependencies between files work, how imports work, etc.

Very helpful post!

1 Like