[Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?
Fri Oct 4 12:03:04 UTC 2013
Tom Ellis wrote:
> On Wed, Oct 02, 2013 at 11:24:39AM +0200, Heinrich Apfelmus wrote:
>> I'm not sure whether the Eq instance you mention is actually
>> incorrect. I had always understood that Eq denotes an equivalence
>> relation, not necessarily equality on the constructor level.
> There's a difference between implementors being able to distingush equals,
> and application programmers. Internal implementations are allowed to break
> all sorts of invariants, but, by definition, APIs shouldn't.
> Are there examples where application programmers would like there so be some
> f, a and b such that a == b but f a /= f b (efficiency concerns aside)? I
> can't think of any obvious ones.
I think the trouble here is that the instance
data Foo = Bar | Baz
instance Eq Foo where _ == _ = True
is perfectly fine if the possibility to distinguish between Foo and
Bar is not exported, i.e. if this is precisely an implementation detail.
The LVish library sits between chairs. If you consider all Eq instances
Safe in the sense of SafeHaskell, then LVish must be marked Unsafe -- it
can return different results in a non-deterministic fashion. However, if
only Eq instance that adhere to the "exported functions preserve
equivalence" law are allowed, then LVish can be marked Safe or
Trustworthy, but that assurance is precisely one we lack.
I think the generic form of the problem is this:
module LVish where
-- | 'foo' expects the invariant that the
-- first argument must be 'True'.
foo :: Bool -> String
foo False = unsafeLaunchMissiles
foo True = "safe"
module B where
goo = foo False
What status should SafeHaskell assign to the modules LVish and B,
It looks like the right assignment is:
LVish - Unsafe
B - Trustworthy
If LVish cannot guarantee referential transparency without assumptions
on external input, then it stands on a similar footing as unsafePerformIO .
More information about the Haskell-Cafe