[Haskell-cafe] Safe Haskell and instance coherence

[Mikhail Glushenkov]

Hello David,

On Thu, Oct 18, 2012 at 6:21 AM, David Mazieres expires 2013-01-15 PST
<mazieres-f97tx4hr7aw7n8sqs9kpcvuwd2 at temporary-address.scs.stanford.edu>
wrote:
>
> 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