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