Hello David,
On Thu, Oct 18, 2012 at 6:21 AM, David Mazieres expires 2013-01-15 PST
What's interesting is that these examples doesn't violate the goals of Safe Haskell--i.e., they don't violate type safety, encapsulation, or semantic consistency as we defined it--but they are worrisome.
I think that my example violates encapsulation in a similar way to how GND violates encapsulation in the MinList example from the Safe Haskell paper. IIUC, the problem is that all instances are assumed to be coherent (that's why it's an error to have two Monoid Int instances in the same module), but this assumption isn't actually enforced across module boundaries, even though it is reflected in the type system. GHC does print a warning after having encountered orphan instances, but that's all.
This is essentially the same thing as my Monoid example. You've got two different dictionaries for the same type, and can pass either one around depending on what module you imported.
Are "dictionaries" something that is a part of Haskell semantics or an artefact of the implementation?
It's not hard to cook up a contrived example where some sort of security monitor hands over the keys to the kingdom if ever it encounters duplicate items in a set. Auditing the code, that might seem fine unless you understand the implementation of Set, which makes reasoning about security a lot harder.
Agreed.
What we really want is for the dictionary to be associated with the data structure at the time of creation, not passed in as an argument for each operation. But that's not even implementable without the existential types extension, and also would require re-writing all the containers, which is absolutely not what we want.
This is what Scala does. Unfortunately, this can make some operations (e.g. set union) asymptotically less efficient (as it's now impossible to rely on the fact that both sets use the same associated dictionary).
Failing that, I guess we could disallow overlapping instances even when they don't overlap in a single module. This is a whole-program check similar to what type families requires, so could possibly be implemented in a similar way.
I'm really interested in the link-time check that is performed for type families. Is it described somewhere?
However, as with type families, making it work with dynamic loading is going to be kind of hard. Essentially there would have to be some run-time inspectable information about all instances defined.
I think that's why Rust chose to just disallow orphan instances :-) Even without dynamic loading, supporting all GHC extensions (e.g. FlexibleInstances) will probably be non-trivial. -- () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments