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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to