[Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

[Heinrich Apfelmus]

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, 
respectively?

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 .


Best regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com