Hi all,
We had a discussion on haskell-cafe, which only confirmed the unreliability
of "Eq" and "Ord". Fine. But if I instead want to define a SafeEq class
and instances based on GHC.Generics, then I can't have users writing
Generic instances that lie about the structure of their types.
But as you can see this module is currently marked "Trustworthy":
http://www.haskell.org/ghc/docs/7.4.1/html/libraries/ghc-prim-0.2.0.0/GHC-Ge...
I simply propose that this is changed to "Unsafe"! [1]
*Context:*
The bottom line is that I believe in the Safe-Haskell mission here, and I
want to be able to deliver practical libraries that give a strong guarantee
that types can't be broken. Currently, the
LVishhttp://www.cs.indiana.edu/~rrnewton/papers/2013_07_LVish_quasiDet_working_dr...library
has one big hole in it because of this Eq/Ord limitation; the
problem is documented
herehttp://www.cs.indiana.edu/~rrnewton/haddock/lvish/Control-LVish.html#g:1
.
If we can provide incontrovertible Safe-Haskel guarantees, this is a
huge, qualitative difference compared to what's possible in the C++, Java's
and MLs of the world. There are plenty of libraries that provide
guarantees like "deterministic parallelism" IFF the user does everything
right and breaks no rules (CnC, Pochoir, etc). But we can do better!
Best,
-Ryan
[1] Small detail... some of these bindings, like the class name "Generic"
itself, will still need to be accessible from a Trustworthy library. I
propose GHC.Generics.Safe for that, following existing precedent.
On Sun, Oct 6, 2013 at 5:18 PM, Ryan Newton
Thanks for the responses all.
I'm afraid the point about GHC.Generics got lost here. I'll respond and then rename this as a specific library proposal.
I don't want to fix the world's Eq instances, but I am ok with requiring that people "derive Generic" for any data they want to put in an LVar container. (From which I can give them a SafeEq instance.)
It's not just LVish that is in this boat.... any library that tries to provide deterministic parallelism outside of the IO monad has some very fine lines to walk. Take a look at Accelerate. It is deterministic (as long as you run only with the CUDA backend and only on one specific GPU... otherwise fold topologies may look different and non-associative folds may leak). Besides, "runAcc" does a huge amount of implicit IO (writing to disk, calling nvcc, etc)! At the very least this could fail if the disk if full. But then again, regular "pure" computations fail when memory runs out... so I'm ok grouping these in the same bucket for now. "Determinism modulo available resources."
A possible problem with marking "instance Eq" as an unsafe feature is that
many modules would be only Trustworthy instead of Safe.
My proposal is actually more narrow than that. My proposal is to mark GHC.Generics as Unsafe.
That way I can define my own SafeEq, and know that someone can't break it by making a Generic instance that lies. It is very hard for me to see why people should be able to make their own Generic instances (that might lie about the structure of the type), in Safe-Haskell.
That would go against my "every purely functional module is automatically safe because the compiler checks that it cannot launch the missiles" understanding of Safe Haskell.
Heh, that may already be violated by the fact that you can't use other extensions like OverlappingInstances, or provide your own Typeable instances.
Actually, Eq instances are not unsafe per se, but only if I also use some other module that assumes certain properties about all Eq instances in scope. So in order to check safety, two independent modules (the provider and the consumer of the Eq instance) would have to cooperate.
I've found, that this is a very common problem that we have when trying to make our libraries Safe-Haskell compliant -- often we want to permit and deny combinations of modules. I don't have a solution I'm afraid.