This post engages in plenty of armchair speculation, and is overall horribly vague, or just nonsense ("addOneTwo works on any type that’s provably isomorphic to

This post engages in plenty of armchair speculation, and is overall horribly vague, or just nonsense ("addOneTwo works on any type that’s provably isomorphic to Integer"). It's more like a plea for all things that seem intuitively nice and good, mashed together without any deep consideration for whether they can be realized consistently. Type classes are still an open research topic, especially when combined with dependent types. From the top of my head: Class coherence is the property that any two instances of the same types are equal. It's a strong guarantee that boosts the robustness and usability of type classes significantly. Scala doesn't have it, instead it has a arcane set of rules that determine the resolution of implicits in the face of ambiguity, and it's a huge pain for more complicated use cases. Named instances are incompatible with coherence. We could just put one named instance into a runtime object, and voila, it's indistinguishable from any other instance. We could remedy this by indexing the type of an instance with a label, which isn't better than choosing instances with newtype wrappers. Similarly, local instances and explicit instance application imply incoherence. Also, laws for classes are an already existing feature in Idris, Agda and Coq. The problem is that laws for anything are by far best realized via dependent types, and dependent types have a nontrivial interaction with classes that is an open problem. With dependent types, checking whether two instance heads are different could be just undecidable, depending on what constructs one allows there. It's a possibility to neuter the language fragment that goes into instance heads, so that propositional equality becomes decidable over it - in a way Haskell already does this, by disallowing type families in instances. But in a dependent language it could be rather awkward that a fair amount of useful types cannot be made instances. Alternatively, one could require proofs from the programmer in each instance that the instance head is propositionally different from all other instance heads in scope. But this would also require much thought, and I haven't given it yet. Also, if our classes are actually coherent, we would like to have an internal proof of this property (as opposed to in current Haskell where we just sort of know that this is the case), but I have no idea how to do this best. Maybe the instance resolution procedure could be modeled internally in a strong enough language, and coherence could be given as a theorem, and there could be some syntactic sugar for code with classes. Or we could have both coherent and incoherent classes, each explicitly marked as such. Or we could have coherent classes by proving that a certain class is necessarily coherent, independently from any instance resolution procedure. There are many such classes, but not nearly all that we frequently use, and some classes are coherent but we can't prove it in currently implemented type theories because the proof relies on parametricity (Functor is such a class).