Proposal: GHC.Generics marked UNSAFE for SafeHaskell

Sun Oct 6 22:12:15 UTC 2013

one thing i'm confused by, and this wasn't properly addressed in the prior
threads,
is

for a type like

data Annotated t ann =  MkAnn t ann

would you consider the following unsafe?

instance Eq t => Eq ( Annotated t ann)
   (==) (MkAnn t1 _) (MkAnn t2 _ ) =  t1 == t2

instance Ord t => Ord (Annotated t ann)
  compare (MkAnn t1 _) (MkAnn t2 _) = compare t1 t2

by the rubric you've proposed these might be *BAD*, right? But theres many
cases where you're doing computation on data, and you wish to track origin,
time, etc, but these annotations are *irrelevant* for the actual values
computed... It sounds like the proposal you want would rule out such
instances!

am i not understanding your proposal?

cheers
-Carter

On Sun, Oct 6, 2013 at 5:46 PM, Johan Tibell <johan.tibell at gmail.com> wrote:

> What would break if we changed it to Unsafe?
>
> On Sun, Oct 6, 2013 at 2:32 PM, Ryan Newton <rrnewton at gmail.com> 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 library has one big
> hole
> > in it because of this Eq/Ord limitation; the problem is documented here.
> >    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> 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
> >
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131006/7cfe632f/attachment.html>