Haskell's Type Classes: We Can Do Better
degoes.net
degoes.net
More than one alternative module implementation may be provided for a module signature, and the actual implementation to be used is chosen on the implicit modules available in the current context. This results into an error if the implicit module cannot be chosen without ambiguity.
I know the standard arguments for class coherence (Set etc.), but I haven't found any of them convincing. Relying on two values coming from two different places to be the same indicates that the design of the code is wrong. It's like writing a function f x y but you must only ever call it with identical arguments x=y. The right thing to do then is to give f only one argument to begin with.
But aside of that, I'm not all that convinced of the importance of coherence in a dependent setting either! My intuition is that types should encode all the properties that we'd like to be able to use in instances. In other words, even if we don't get coherence, we can use types to constrain the implementation of instances as much as we like.
Highly ambiguous instance resolution (like a bunch of Monoid Int instances lying around) is a bit of a pain though, and there could be some "using instance" feature/syntax that locally throws out all instances except one.
Additionally, as of now there are no large production code bases that use Coq style type classes in a proper dependent language. There are very few sizable applications in dependent languages to begin with. So we don't know a lot about the practical caveats of that design, while there is a lot of experience and know-how about Haskell-style classes, which is one reason why we should at least consider salvaging coherence in future languages.
Generally, I think that type classes are a rather ugly and haphazard construction compared to the succinct elegance of the type theories of core languages; still, eventually type classes worm their way into languages (Agda, Coq) because people really like them and like to use them, so a language designer should consider them. I wish there was an elegant/general formal treatment that captures the essential features, in any case.
Tie the type definition to the point where the data is created. Default to the local definition, but have a way to select the other one if you need some particular interaction between modules. Wouldn't that solve the conflict?
At which point you have basically reinvented "newtype"
My concern is that this PhD-style development suffices for most Haskell users, but is not practical for any non-small project in the real world with more than one developer.
This is not my experience of working with Haskell in the real world on a non-non-small project with (many) more than one developer.
Global coherence and confluence (which GHC attempts to enforce unless told otherwise) is great for refactoring and equational reasoning and (yes) mathematics and programming at large, as Ed Kmett's fantastic "Typeclasses v. the World" talk covers:
https://www.youtube.com/watch?v=hIZxTQP1ifo
Global uniqueness of instances (which GHC does NOT enforce) is bad for modular programming, or programming at large, which is a point some of the commenters here are making.
http://blog.ezyang.com/2014/07/type-classes-confluence-coher...
The submitted HN link here has a terrible title. What the author is proposing is enforcing typeclass laws, which is a great idea (but difficult in practice to implement). Practice and time has shown that lawless classes are the ones that people hate, the ones that don't add any benefit and in fact make it harder to reason about large Haskell programs.
I hope people don't take away from this link that classes in Haskell are bad. Haskell is three things: pure, functional, and typeclasses. They're part of the identity of Haskell; they're the reason we set off on this wonderful journey into the uncharted oceans of functional programming back in 1990. Typeclasses are AWESOME. And they can be improved.
Postscript: Kmett also has a package that persuades the compiler to let you have dynamically generates instances. It has the same user experience as local implicits, which I think a lot of people here are asking for:
http://hackage.haskell.org/package/reflection/src/examples/C...
λ> using (Monoid (+) 0) $ mappend mempty 12
12
Yes, I know the article isn't about dependent types per se but many of the features he wants get pretty close to dependent types since that is pretty much the state of the art when it comes to advanced type systems with lawful abstractions and whatnot.
I'm pretty sure Parent didn't included Haskell.
And anyway, my point was that you can do much much more than type level arithmetic.
Plus someone is seriously working on dependent types in Haskell - so no, I think it's fitting.
I don't think I can be convinced that correct-by-construction methods are wrongheaded. I am convinced that humans aren't very good at wrangling precise and complex and large ideas without failure.
Do not forget that most dependently type languages (and Coq the first) are proof languages. The goal is not (only) to write programs, but to prove things and a rather large number of theorem have been proven that way.
Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ?
Edit: woops, missed the "here" in parent's comment. No, I don't work on compcert. :)
How long will this be the case? Seems like they've been "cutting edge research" for a few decades, and the Curry-Howard correspondence itself is like 80 years old. Surely if there were a real demand for these kinds of programming languages, we would have seen some industry penetration at some point, right?
Some of this is about the penetration of certain ideas. Like, we had to wait for multiple cores on commodity hardware before functional programming started to cross over from the academic community to the professional web programmer.
That shift helps your average programmer to think a bit more mathematically, and then it's basically about whether the programmer starts to appreciate types - and to me that seems to be less about purity of argument than the professional atmosphere the programmer is in. Are you prototyping and moving fast and breaking stuff, or are you caring more about longevity and correctness.
And then once you start getting more into static typing and functional programming, a lot of these other ideas start to become more attractive and intriguing.
It's like a lot of ideas that circulate around for a long time before they really take hold; you're waiting for a certain critical mass of system inputs and momentum, and then things can start to change really fast.
Also, do not forget Haskell's roots were to create a programming language environment where people studying compilers could easily experiment with new features. Hence Haskell's large number of language extensions.
Or, maybe, there just isn't a real industry demand for dependent types. Hell, many engineers still have trouble convincing their employers to write robust tests, let alone full proofs of correctness.
For example, let's say you define a type of list of size n. Great. You can only assign list of the same size and you can only append an element of the type "n" to a type "n-1" or the compiler will complain. Now you can even prove that your program is formally correct. What's not to like?
And then, reality knocks at your door.
How do you instantiate such a type? It needs to be instantiated right away with n elements or your program won't compile. But these elements are coming from the runtime, say, a database. How the hell does this work?
Dependently typed languages that go just a step beyond prototypes quickly realize how crippling this approach is and they will give you all kinds of escape hatches to weaken the type system just so you can use the darn thing. But it's futile, because at the end of the day, a program is a living thing that relies on side effects and external inputs, and sophisticated systems are just not designed to cope with human fuzziness.
The reason why dependently typed systems never became popular is not because the world hasn't realized yet how awesome they are: it's because they just aren't a good fit to solve real problems.
Nobody would ever question the value of a unit-testing framework because it requires you to instantiate objects and doesn't hit the database and the ORM. (Yes, there are testing strategies that cover all of that, but for unit-testing application logic, you generally want to skip all of that.) Dependent types should let you do the same thing that a test would do, except exhaustively: if you add a new email address to an account with N addresses, you can then index N+1 of those addresses, but no more. The N-address account coming from the ORM isn't considered an "escape hatch" that "weakens the test system": it's just how it works.
I want stronger types for exhaustive testing of business logic on individual functions -- the sort of things that a comment would say (e.g. "Returns a subset of this parameter if it is provided, otherwise..."), except machine-checked. I don't need my entire program to have a type that Messrs. Curry and Howard like. In all probability, my entire program is structured as an infinite loop anyway.
I don't know that any systems really let you get here (other than maybe extraction of particular functions into Haskell or ML, but really the people who would voluntarily write their entire app in Haskell or ML are not the right target audience).
I don't follow. If your list is not the right size, your program doesn't compile, period.
If it does, you're not using a dependently typed language.
Am I missing something?
Then, at runtime, you can cast an unsized list to a sized list giving - say - a function List[A] => Option[Sized[List[A], N5]] that will fail if the list is not of size 5. From then on you can go on letting the compiler keep track of lengths.
Of course, this does not work at all if you have no clue what size your input will have
The key insight here is that the check may be performed at compile time or runtime as long as the compiler can see that you've performed the check. It can do this e.g. in pattern match clauses. For example in code like
case inputList of
[a,b,c,d,e] -> branch-A
otherwise -> branch-B
(And if you think about it... if you didn't allow for runtime checks to satisfy such proof obligations there would essentially no way for any dependently programs to depend on any runtime values at all.)
Aside: Another thing which I think has been missed in this entire discussion is that you don't have to actually use List-of-size-N as your type. If you don't actually care about the size of the list in the code you're writing, you're also allowed to just use List-of-any-finite-size as your data type. (Of course this could cause a certain amount of friction if the standard library is all based on List-of-size-N, but it shouldn't be too bad in e.g. Idris.)
Taking your example, I would have written a function f* that takes a list (with an arbitrary type of elements) and produces an integer. Its basic ML type would be:
f : list 'a -> int
f : l:list 'a{length l = 5} -> x:int{p x = True}
Now assume I want to use this function later in my code to deal with some user provided input. Assume I have a function read_int_list:
read_int_list : () -> list int
val process_input =
let inp = read_inst_list ();
let res = if length inp = 5
then f inp
else -1 // error
So interacting with user input and output is absolutely NOT a problem for dependently typed languages and their ilk. In fact, there is a full-blown implementation of the TLS protocol in F.
What is a problem, however, are the two points I hinted at: convincing the compiler that your statements are true. This is done in one of the two ways. First, you can manually give "hints" to the compiler, which is normally very tedious. Second, the compiler can try proving them automatically (F* for example leverages an SMT solver), which is great when it works, but often doesn't work.
So the real problem is that producing proofs is quite time consuming, and thus expensive. The world, as you put it, is not completely wrong: very often, a buggy program is cheaper than a correct one. Heck, people still stick to OpenSSL over the above verified TLS implementation - and for good reasons. The exceptions being programs used in NASA rovers and such - which is where you're starting to see dependent types being used. I certainly won't use them for my projects - at least not until the systems get massively better at producing proofs. It's partly happened with the advent of the SMT solvers, but it's nowhere near enough.
It's easy, since it works as it always did. You check whether the list coming from the database has the correct size n, and then the type system knows that and lets you pass said list to a function that expects a list of size n.
list = GetAListFromTheDatabase()
if(list.size == n){
// type checker knows that the size is n here
foo(list);
}else{
error("Database returned a list of incorrect size.");
} after a certain point the validation overhead of advanced type systems is just not worth it.
Another advantage is that unlike Curry-Howard based verification, program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This tends to yield shorter proofs.
See Microsoft's Daphny [1] or CFML [2] for prototype tool chains implementing program logic based verification. Facebook's infer tool [3], while not allowing full verification, is also based on program logic.
[1] http://research.microsoft.com/en-us/projects/dafny
This is simply not the case. Significant verification projects always plan for verification and do verification in tandem. This is definitely true for all Dafny projects to date as well. Verification is just so much harder than unverified programming that you generally want to do everything you can while programming to make verification easier. This may become less true as proof automation improves but it will always be a tension.
> But what makes you think you need dependent types to do full specification [...] ?
Also, keep in mind that Dafny and similar tools can only express first order logic; this can significantly restricts the expressiveness of your specification language and intermediate lemmas.
> program logic does not have to be constructive, instead you can use classical reasoning with excluded middle.
This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle (only NuPRL is I believe) so you can always assume it as an axiom if you'd like. Most projects don't do this because constructivism is a benefit not a burden in verification: it allows you to make distinctions that aren't possible in classical logic.
I agree that Dafny and similar projects are very exciting though; Dafny's tight integration with Z3 provides an awesome level of automation that will keep getting better and better.
Significant verification projects always plan for verification
and do verification in tandem.
A key problem in contemporary software engineering is that specifications constantly change (aka "customers don't know what they want"). Agile software engineering methodologies have mostly taken over from waterfalls because agile is designed from the start to minimise the cost of change (how successful they are at minimise the cost of change is another matter). If you have to redo not just the code itself and tests but also proofs every time your customer changes the spec, the costs of software development increase rapidly. Look at e.g. Java exception specifications, for a similar but much more benign problem. The program logic approach to verification does not force the full cost of verification on the programmer, because verification can be deferred until the program specification is stable and it's code passes all tests. This enables a hybrid approach to program correctness: in early states of the software engineering process, you use lightweight methods such as Hindley-Milner like typing systems, and testing, and only in later states you go for logic-based approaches. Let me repeat that the program logic approach always allows you to specify and verify from day one, so program logic gives you the best of both worlds.
Dafny and similar tools can only express first order logic
This is a silly point. First off proof assistants like Coq aren't
inconsistent with the law of the excluded middle
The real reason everybody uses dependent types is that they are perfectly matched for the verification of pure functional programs, since proofs are pure functional programs. This is beautiful. But as soon as you want to verify non functional programs, that beautiful coincidence evaporates.
This is another key shortcoming of the dependent types approach: it's unlikely that it can be extended in a beautiful way to low-level programming, stateful programming, timed programming, concurrent programming.
My bet is that the tooling & theory will continue to improve and eventually the overhead will become low enough that a significant portion (~10-20%) of software will be certified.
I recommend reading Adam Chlipala's vision statement for inspiration on what certified programming could enable: http://adam.chlipala.net/summary.html
This subsumes a lot of things like generics, existential types, GADTs, higher kinded types, rank-n polymorphism, etc. You can even use it to do record types, polymorphic variants, modules, refinement types, etc. The dependent function type is a universal lego block for types.
Even more striking, it unifies the type level with the value level. Instead of having a language of types and a language of expressions there is just one language. The type List<T> takes a type T and gives you the type of lists with elements of type T. In dependently typed languages this is just a function List(T) that takes a type and returns a type. Instead of having F<T> at the type level and f(x) at the value level, there's only one kind of function that does both.
I have no doubt that we will eventually be programming in a dependently typed language, the only question is when.
I have no doubt that we will eventually be
programming in a dependently typed language,
the only question is when.
So even if you ultimately want to reason about your programs using an external program logic (which I predict we do not, but we'll see), then for expressiveness you still want your language to have dependent types for the reason I mentioned above:
> Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs.
Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. You can write your program as normal and later prove lemmas about functions in the program. For instance instead of saying
reverse : Vec n a -> Vec n a
reverse : (xs : List a) -> {ys : List a | length xs == length ys}
reverse : List a -> List a
reverse_preserves_length : forall xs. length (reverse xs) == length xs
What's this forall you say? A dependent function type of course!
Idris has ... is that not satisfactory?
It is perfectly possible to program in them like you would in a normal language.
I regularly run into situations where I think "gosh, if I had dependent types
Two, type system researchers promote provably correct programming as the advantage of dependent types.
they generalize a vast swath of different type system features
Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system.
> For a start you have to prove termination, even when you use simple types.
This is not the case. E.g. in Idris you have non-terminating functions. In NuPRL the whole thing is built on potentially non-terminating functions. Of course the functions that you use as proof witnesses have to terminate, but that's true in any system since a non-terminating proof witness means that the proof is bogus ("Theorem: Socrates is a goat. Proof: Socrates is a goat because Socrates is a goat."). The functions in the program that that the specification is saying something about do not have to be proven to terminate.
> (1) you can always do the same with program logic, prove that you don't need a cast, but more imporantly (2) in a lot of large-scale programming projects, you don't have good specifications up-front
I don't want to prove that I didn't need the cast or check, I want to not have the cast or check in the program in the first place. This is about types that are expressive enough to model the actual shape of the data, not about proving that a program is correct relative to some specification. By analogy with lacking generics / parametric polymorphism like old versions of Java: if I write a program that uses a List I need to cast to and from Object. With generics I can use a List<T> and do not need the cast. I don't want to write the program with casts and then prove that I didn't need them, I want to write the program with List<T> without casts. For the same reason that you still want generics even if you use a program logic to reason about your programs, you still want dependent types even if you use a program logic to reason about your programs.
> With program logic you can easily delay verification until the end of the project (but don't have to), with Curry-Howard based verification you can't.
Why? You can write the same program without specification as you would in the program logic system, and then prove lemmas about it.
> the beauty stands in the way of type inference
Type inference is overrated anyway, and with dependent types you don't actually lose type inference. You do lose it for the parts of the programs that use fancy types, but you wouldn't be able to write those at all in a language with full type inference. There is no fundamental reason that a dependently typed language couldn't have the same type inference for non-dependently typed pieces of the program as the language that only supports non-dependent types.
By the way, and I admit this is more of a theoretical curiosity, IIRC full type inference for dependent types is decidable if you do not have implicit parameters. That does make sense: you can either infer types, or values, but not both at the same time. Of course in practice you much rather have implicit parameters than type inference. From the proof assistant side of Curry-Howard type inference is also kind of strange: you infer the theorem (the type) from the proof (the program). So it's like writing down a proof, but having it inferred what the proof is actually proving.
> the Hindley-Milner polymorphic typing system "has hit a sweetspot"
Where sweetspot = local optimum :) Meanwhile, OCaml is getting GADTs ;-)
I don't understand what you mean by encoding tax. Can you give an
example? Certainly lots and lots of work to make an actual
practical and usable system still needs to happen, but I don't
see any fundamental limitations with respect to effects,
including non-termination.
Let me give you a second example. Most programming languages can be encoded into \pi-calculus, and pi-calculus has a good logic called Hennessy–Milner logic (HML). You can use HML to reason about all \pi-calculus behaviour. Since \pi-calculus is a very expressive model of computing, HML is extremely fine-grained. Now assume you want to reason about ML programs. You do this by translating them into \pi-calculus and then using HML. But due to the fine-grainedness of HML this will be very painful. It's much more efficient to develop a logic for ML itself, and avoid paying the "encoding tax".
As I said, I don't know Idris well, but I assume that the proof language does not have state and other effects, so they need to be coded up as pure functions. I expect there to be an "encoding tax" to be paid for this translation of effects into pure functions.
This is not the case. E.g. in Idris you have non-terminating functions.
By analogy with lacking
generics / parametric polymorphism like old versions of Java:
You can write the same program without specification as you
would in the program logic system, and then prove lemmas about
it.
There is no fundamental reason that a dependently typed language
couldn't have the same type inference for non-dependently typed
pieces of the program as the language that only supports
non-dependent types.
By the way, and I admit this is more of a theoretical curiosity,
IIRC full type inference for dependent types is decidable if you
do not have implicit parameters.
OCaml is getting GADTs ;-)
There is general consensus that the best way to handle effects is a pure base language with an effect system on top. Idris takes a good shot at this, but I doubt it's the last word. Eff and Koka and F* seem particularly promising as well.
> This is not a good analogy, because type-inference can handle parametric polymorphism, whereas general type-dependency on values cannot be dealt in that form.
Why did type inference become the #1 criterion for a type system in this discussion? There are far more important criteria than type inference, such as expressiveness. If your type system is not expressive enough you wouldn't be able to write the program that can't be type inferred at all. Why is that a win?
> Yes, but they are not in your proof language. You can always code up anything.
No sound system can have non terminating functions as proof witnesses. You can reason about potentially non terminating functions just fine in dependently typed languages. Look in particular at NuPRL, which is build around the concept.
> If it's so simple, then we should have systems that do this. We don't have such systems, hence it's probably not that simple.
Doing type inference for non HM-typeable parts of programs is theoretically simple. For the parts of the program that do not have type annotations just type infer them with a HM inference algorithm, if it succeeds great if it fails signal a type error. Just like in ML. The reason that it hasn't been done is likely a combination of reasons (1) not publishable (2) a lot of work (3) type inference just isn't that important especially if you're only doing it for the HM-typeable fragment.
> My experiences in Coq and Agda suggest that that's not the case.
Coq and Agda are not the pinnacle of the possibilities of dependent types. As I said, it's ongoing research. My point is that the style of writing a program and then separately proving lemmas about it is perfectly possible in a dependently typed language.
I would also suggest that your experience may not yet have been that extensive if you didn't know about implicit parameters?
> I don't know what you mean by "implicit parameters". Type inference might be decidable for some weak inexpressive dependently typed systems, but MLTT, CoC, nope?
Implicit parameters let you mark function parameters as implicit and they will be inferred at the call site if the compiler can deduce that they must have one particular value in order for the program to type check. It's like the reverse of type inference: instead of inferring the type of an expression, we infer the expression from the type. It's kind of related to type classes, which let the compiler infer type class dictionaries from types.
Look at the Sage work for full inference for refinement types. I think the same strategy could work for full dependent types. Of course it's not really what you want in practice, since in a dependent type system the most precise type you infer for a function simply restates what the function computes. That is, if you have the function (\x -> x+2) then the type will simply say "a function that returns its argument +2". Inferring the most precise HM type gives reasonable results precisely because HM is weak, so you don't get a type that's "too precise" ;-)
> Yep, and that preserves type inference, which is the key factor. So it's Hindley-Milner still.
Type inference for GADTs is undecidable.
There is general consensus that the best way to handle effects is
a pure base language with an effect system on top.
Why did type inference become the #1 criterion for a type system
in this discussion?
There are far more important criteria than type inference, such
as expressiveness.
- Expressiveness.
- Strength of properties guaranteed by typing.
- Speed (including decidability) of type-checking or type-inference.
Unfortunately there are hard trade-offs between them.
Doing type inference for non HM-typeable parts of programs is
theoretically simple.
I would also suggest that your experience may not yet have been
that extensive if you didn't know about implicit parameters?
Look at the Sage work for full inference for refinement types.
Type inference for GADTs is undecidable.
This is precisely what an effect system is, and what the languages that I mentioned do. So it seems that you agree with the the church of lambda on this point?
> We have been talking about large-scale software engineering, and whether Curry-Howard or program logic is a more scalable approach towards program verification. [...] I cannot see how a verification tool that I'm forced to use in prototype phases when there is no stable specification is cost-effective in large-scale software engineering.
I've explained several times that the assumption that you need to do full on verification from the start with a CH style system is incorrect. You can write your prototype without any verification and add lemmas and theorems about it when the spec stabilizes. This is not a fundamental difference between CH style vs program logic style.
> Sheer expressiveness is not interesting. You can produce trivial typing systems where every program is typable.
Well yes, you also need "well typed programs don't go wrong" of course, which dependent type systems do have. I don't think decidability of type checking is desirable, by the way. What you really want is a system that checks statically as much as possible, but can check dynamically that which it can't verify statically. Rather than two possibilities "correct" vs "incorrect" you want three: "definitely correct", "definitely incorrect" and "can't determine statically, so let's check dynamically". In the last case conventional systems just reject the program as incorrect, but I think that is not as helpful.
> Even if some kind of polished Haskell with dependent types can be build, whether that then generalises to state, concurrency, timing etc in a clean way is another open question.
More open than a program logic system that does the same? I don't think the approaches are that different in this regard. With state/concurrency/etc you work with a description of the computation (like in Haskell you work with a description of an IO computation). Those satisfy certain laws which you can use to reason about them. There is of course a huge design space to be explored here, but that design space isn't all that different than the design space of a program logic style system for the same.
> The term is used in with different meanings in different contexts.
I see, yes. They're sometimes called implicit parameters, sometimes implicit arguments, and there's differences in whether only unification is used or also type class / canonical structures / scala style implicit parameters kind of non-canonical inference.
> That's not full type inference. Sage use hybrid type-checking and inserts dynamic checks where type inference fails.
The dynamic checks are for when type checking fails, not type inference. The type inference will always infer the type if the term is typeable. Of course it may sometimes infer a type that the type checker doesn't know statically whether it's valid or not, so you need dynamic checks then. There is no incompleteness defeating magic here, but if the term is typeable then the type inference will infer a type for the term, whether the type checker statically knows that it's valid or not. I did say this was more of a theoretical curiosity.
> Are you sure?
That paper itself says so in the first sentence?
This is precisely what an effect system is, and what the
languages that I mentioned do. So it seems that you agree with
the the church of lambda on this point?
I've explained several times that the assumption that you need
to do full on verification from the start with a CH style
system is incorrect. You can write your prototype without any
verification and add lemmas and theorems about it when the
spec stabilizes.
Well yes, you also need "well typed programs don't go wrong"
of course, which dependent type systems do have.
List.hd [];;
I don't think decidability of type checking is desirable, by
the way. What you really want is a system that checks
statically as much as possible, but can check dynamically that
which it can't verify statically. Rather than two
possibilities "correct" vs "incorrect" you want
three: "definitely correct", "definitely incorrect" and "can't
determine statically, so let's check dynamically". In the last
case conventional systems just reject the program as
incorrect, but I think that is not as helpful.
More open than a program logic system that does the same?
I don't think the approaches are that different in this
regard. With state/concurrency/etc you work with a description
of the computation
The dynamic checks are for when type checking fails, not type
inference. The type inference will always infer the type if the
term is typeable.
That paper itself says so in the first sentence?
I think I've understood your points and made mine, so lets see how it pans out :) Thanks for the discussion!
My two cents is that this is just like every other static vs. dynamic typing debate, and it's a deep tradeoff. I've been pretty pleased with typeclasses as an easy-to-use sweet spot between complexity/mental overhead and safety. But I'm certainly willing to believe we can do better, of course.
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).
> Named instances are incompatible with coherence. We could > just put one named instance into a runtime object
Could you give an example of what you mean in, e.g., Haskell (assuming some fictional facility for named instances existed)?
> With dependent types, checking whether two instance heads > are different
What are instance heads?
Instance heads are the types in the instance declaration that the compiler dispatches on, for example in `instance Show Int` the head is `Int`.
> named instances
You can see an example for named instances in Idris (very Haskell-like syntax) here (http://idris.readthedocs.org/en/latest/tutorial/classes.html...). We could put named instances into runtime objects (example in Haskell: `data ShowInstance a = Show a => Instance` which does exactly this), thereby forgetting the name, which could cause ambiguities down the line. But even without instances in runtime boxes, different instances for the same type necessitate that there are some rules for instance resolution that a programmer has to consider. For example, if we have two monoid instances for `Int`, one with addition and one with multiplication, we somehow need to make sure that the monoid operations mean what we want them to mean, so that we don't get unexpectedly addition instead of multiplication.
If there was a compiler which would enforce these rules.
You can find the gist here. https://gist.github.com/joost-de-vries/949fbea6345fec1ac4ef