Proposal: GHC.Generics marked UNSAFE for SafeHaskell

[Ganesh Sittampalam]

Hi,

The Safe Haskell safety properties are currently defined at
http://www.haskell.org/ghc/docs/latest/html/users_guide/safe-haskell.html#safe-language:

 - Referential transparency: e.g. no unsafePerformIO

 - Module boundary control: no abstraction violation like Template
Haskell and GeneralizedNewtypeDeriving

 - Semantic consistency: importing a safe module can't change existing
code, so no OverlappingInstances and the like

Is this change necessary to preserve the existing properties, or are you
hoping to add a new one?

I also understand that you want to require 'standard' Generic instances
on types - will that mean that module authors are forced to expose
internals to use your library?

Cheers,

Ganesh

On 06/10/2013 22:32, Ryan Newton wrote:
> 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-Generics.html
> 
> 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 LVish
> <http://www.cs.indiana.edu/~rrnewton/papers/2013_07_LVish_quasiDet_working_draft.pdf>
> library has one big hole in it because of this Eq/Ord limitation; the
> problem is documented here
> <http://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 <rrnewton at gmail.com
> <mailto:rrnewton at gmail.com>> wrote:
> 
>     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.
> 
> 
> 
> 
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>