Any precedent or plan for guaranteed-safe Eq and Ord instances?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
23 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Any precedent or plan for guaranteed-safe Eq and Ord instances?

Ryan Newton
Hello all,

Normally, we don't worry *too* much about incorrect instances of standard classes (Num, Eq, Ord) etc.  They make the user's program wrong, but they don't compromise the type system.

Unfortunately, with the LVish parallel programming library we do have a situation where incorrect instances of Eq and Ord can cause the "types to lie".  In particular, something that claims to be a pure, non-IO type, can actually yield a different result on different runs, including throwing exceptions on some runs but not others.

So what's the best way to lock down "SafeEq" and "SafeOrd" instances, taking control away from the user (at least with -XSafe is turned on)? 

We could derive our own SafeEq and SafeOrd instances based on GHC.Generics.  BUT, that only helps if we can forbid the user from writing their own incorrect Generics instances when Safe Haskell is turned on.  It looks like GHC.Generics is currently marked as "TrustWorthy":


So.... could we get GHC.Generics marked as "Unsafe" and enable some more limited interface that is "Trustworthy"?  (Allowing the user ONLY to do 'deriving Generic').

This would be similar to the new policy in GHC 7.8 of only allowing derived Typeable instances...

  -Ryan


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Ryan Newton

Here are some examples:

---------------------------------------------
data Foo = Bar | Baz

instance Eq Foo where
  _ == _ = True

instance Ord Foo where
  compare Bar Bar = EQ
  compare Bar Baz = LT
  compare _   _   = error "I'm partial!"
---------------------------------------------

These would allow LVish's "runPar" to non-determinstically return Bar or Baz (thinking they're the same based on Eq).  Or it would allow runPar to nondeterministically crash based on different schedulings hitting the compare error or not [1].

FYI here's LVish:

    

   -Ryan

[1] If you're curious why this happens, its because the Ord instance is used by, say, Data.Set and Data.Map for the keys.  If you're inserting elements in an arbitrary order, the final contents ARE deterministic, but the comparisons that are done along the way ARE NOT.



On Tue, Oct 1, 2013 at 4:13 PM, Ryan Newton <[hidden email]> wrote:
Hello all,

Normally, we don't worry *too* much about incorrect instances of standard classes (Num, Eq, Ord) etc.  They make the user's program wrong, but they don't compromise the type system.

Unfortunately, with the LVish parallel programming library we do have a situation where incorrect instances of Eq and Ord can cause the "types to lie".  In particular, something that claims to be a pure, non-IO type, can actually yield a different result on different runs, including throwing exceptions on some runs but not others.

So what's the best way to lock down "SafeEq" and "SafeOrd" instances, taking control away from the user (at least with -XSafe is turned on)? 

We could derive our own SafeEq and SafeOrd instances based on GHC.Generics.  BUT, that only helps if we can forbid the user from writing their own incorrect Generics instances when Safe Haskell is turned on.  It looks like GHC.Generics is currently marked as "TrustWorthy":


So.... could we get GHC.Generics marked as "Unsafe" and enable some more limited interface that is "Trustworthy"?  (Allowing the user ONLY to do 'deriving Generic').

This would be similar to the new policy in GHC 7.8 of only allowing derived Typeable instances...

  -Ryan



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Heinrich Apfelmus
Ryan Newton wrote:

> Here are some examples:
>
> ---------------------------------------------
> data Foo = Bar | Baz
>
> instance Eq Foo where
>   _ == _ = True
>
> instance Ord Foo where
>   compare Bar Bar = EQ
>   compare Bar Baz = LT
>   compare _   _   = error "I'm partial!"
> ---------------------------------------------
>
> These would allow LVish's "runPar" to non-determinstically return Bar or
> Baz (thinking they're the same based on Eq).  Or it would allow runPar to
> nondeterministically crash based on different schedulings hitting the
> compare error or not [1].
>
> [..]
>
> [1] If you're curious why this happens, its because the Ord instance is
> used by, say, Data.Set and Data.Map for the keys.  If you're inserting
> elements in an arbitrary order, the final contents ARE deterministic, but
> the comparisons that are done along the way ARE NOT.

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.

One prominent example would be equality of Data.Map itself: two maps are
"equal" if they contain the same key-value pairs,

     map1 == map2  <=>  toAscList map1 == toAscList map2

but that doesn't mean that their internal representation -- the balanced
tree -- is the same. Virtually all exported operations in Data.Map
preserve this equivalence, but the library is, in principle, still able
to distinguish "equal" maps.

In other words, equality of abstract data types is different from
equality of algebraic data types (constructors). I don't think you'll
ever be able to avoid this proof obligation that the public API of an
abstract data type preserves equivalence, so that LVish will yield
"results that are deterministic up to equivalence".


However, you are mainly focused on equality of keys for a Map. In this
case, it might be possible to move towards pointer equality and use
things like  Hashable  or  StableName .


Best regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Tom Ellis
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.

> One prominent example would be equality of Data.Map itself: two maps
> are "equal" if they contain the same key-value pairs,
>
>     map1 == map2  <=>  toAscList map1 == toAscList map2
>
> but that doesn't mean that their internal representation -- the
> balanced tree -- is the same. Virtually all exported operations in
> Data.Map preserve this equivalence, but the library is, in
> principle, still able to distinguish "equal" maps.

I had a quick skim of

    http://www.haskell.org/ghc/docs/latest/html/libraries/containers/Data-Map-Lazy.html

to find such examples, and the only one that jumped out was "showTree".  Are
there others?

Still, although the library is, in principle, able to distinguish "equal"
maps, isn't this just a leaking implementation detail?  Is it somehow of
benefit to API users?

Tom
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Roman Cheplyaka-2
In reply to this post by Heinrich Apfelmus
* Heinrich Apfelmus <[hidden email]> [2013-10-02 11:24:39+0200]
> In other words, equality of abstract data types is different from
> equality of algebraic data types (constructors). I don't think you'll
> ever be able to avoid this proof obligation that the public API of an
> abstract data type preserves equivalence, so that LVish will yield
> "results that are deterministic up to equivalence".

It still seems to fit nicely into Safe Haskell. If you are the
implementor of an abstract type, you can do whatever you want in the Eq
instance, declare your module as Trustworthy, and thus take the
responsibility for soundness of that instance w.r.t. your public API.

Roman

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Tillmann Rendel-5
Hi,

Roman Cheplyaka wrote:
> It still seems to fit nicely into Safe Haskell. If you are the
> implementor of an abstract type, you can do whatever you want in the Eq
> instance, declare your module as Trustworthy, and thus take the
> responsibility for soundness of that instance w.r.t. your public API.

A possible problem with marking "instance Eq" as an unsafe feature is
that many modules would be only Trustworthy instead of Safe. So if I
don't trust the authors of a module (because I don't know them), I
cannot safely use their code just because they implement their own Eq
instance?

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.


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.

   Tillmann
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Roman Cheplyaka-2
* Tillmann Rendel <[hidden email]> [2013-10-02 13:19:38+0200]

> Hi,
>
> Roman Cheplyaka wrote:
> >It still seems to fit nicely into Safe Haskell. If you are the
> >implementor of an abstract type, you can do whatever you want in the Eq
> >instance, declare your module as Trustworthy, and thus take the
> >responsibility for soundness of that instance w.r.t. your public API.
>
> A possible problem with marking "instance Eq" as an unsafe feature is
> that many modules would be only Trustworthy instead of Safe. So if I
> don't trust the authors of a module (because I don't know them), I
> cannot safely use their code just because they implement their own Eq
> instance?
>
> 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.
>
>
> 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.
Good point!

Roman

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Stijn van Drongelen
In reply to this post by Tillmann Rendel-5
I do think something has to be done to have an Eq and Ord with more strict laws.

* Operators in Eq and Ord diverge iff any of their parameters are bottom.
* The default definitions of (/=), (<), (>) and `compare` are law.
* (==) is reflexive and transitive
* (<=) is antisymmetric ((x <= y && y <= x) `implies` (x == y))
* (<=) is 'total' (x <= y || y <= x)
* (<=) is transitive

Currently, reflexivity of (==) is broken in the Prelude (let x = 0/0 in x == x). I know this is for IEEE 754 compliance, but c'mon, this is Haskell, we can have better ways of dealing with NaNs.

-Stijn

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Niklas Haas
On Wed, 2 Oct 2013 15:46:42 +0200, Stijn van Drongelen <[hidden email]> wrote:

> I do think something has to be done to have an Eq and Ord with more strict
> laws.
>
> * Operators in Eq and Ord diverge iff any of their parameters are bottom.
> * The default definitions of (/=), (<), (>) and `compare` are law.
> * (==) is reflexive and transitive
> * (<=) is antisymmetric ((x <= y && y <= x) `implies` (x == y))
> * (<=) is 'total' (x <= y || y <= x)
> * (<=) is transitive
>
> Currently, reflexivity of (==) is broken in the Prelude (let x = 0/0 in x
> == x). I know this is for IEEE 754 compliance, but c'mon, this is Haskell,
> we can have better ways of dealing with NaNs.

Like making Double not be an instance of Eq?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Colin Adams
In reply to this post by Stijn van Drongelen
Only for meanings of "better" which do not imply as good performance.


On 2 October 2013 14:46, Stijn van Drongelen <[hidden email]> wrote:
I do think something has to be done to have an Eq and Ord with more strict laws.

* Operators in Eq and Ord diverge iff any of their parameters are bottom.
* The default definitions of (/=), (<), (>) and `compare` are law.
* (==) is reflexive and transitive
* (<=) is antisymmetric ((x <= y && y <= x) `implies` (x == y))
* (<=) is 'total' (x <= y || y <= x)
* (<=) is transitive

Currently, reflexivity of (==) is broken in the Prelude (let x = 0/0 in x == x). I know this is for IEEE 754 compliance, but c'mon, this is Haskell, we can have better ways of dealing with NaNs.

-Stijn

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Stijn van Drongelen
In reply to this post by Niklas Haas
On Wed, Oct 2, 2013 at 3:49 PM, Niklas Haas <[hidden email]> wrote:
On Wed, 2 Oct 2013 15:46:42 +0200, Stijn van Drongelen <[hidden email]> wrote:
> I do think something has to be done to have an Eq and Ord with more strict
> laws.
>
> * Operators in Eq and Ord diverge iff any of their parameters are bottom.
> * The default definitions of (/=), (<), (>) and `compare` are law.
> * (==) is reflexive and transitive
> * (<=) is antisymmetric ((x <= y && y <= x) `implies` (x == y))
> * (<=) is 'total' (x <= y || y <= x)
> * (<=) is transitive
>
> Currently, reflexivity of (==) is broken in the Prelude (let x = 0/0 in x
> == x). I know this is for IEEE 754 compliance, but c'mon, this is Haskell,
> we can have better ways of dealing with NaNs.

Like making Double not be an instance of Eq?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Like making IEEE754 Doubles not an instance of Eq. Normal and denormal Doubles should have Eq instances.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Tom Ellis
In reply to this post by Stijn van Drongelen
On Wed, Oct 02, 2013 at 03:46:42PM +0200, Stijn van Drongelen wrote:
> * Operators in Eq and Ord diverge iff any of their parameters are bottom.

What's the benefit of this requirement, as opposed to, for example

   False <= _ = True
   ...

Tom
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Roman Cheplyaka-2
In reply to this post by Stijn van Drongelen
* Stijn van Drongelen <[hidden email]> [2013-10-02 15:46:42+0200]
> I do think something has to be done to have an Eq and Ord with more strict
> laws.
>
> * Operators in Eq and Ord diverge iff any of their parameters are bottom.

This outlaws the Eq instances of lists, trees, and other (co)recursive
types.

Furthermore, in this formulation, even Eq for tuples is illegal, because

  (undefined, something) == somethingElse

is going to diverge.

Roman

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Stijn van Drongelen

On Wed, Oct 2, 2013 at 4:17 PM, Tom Ellis <[hidden email]> wrote:
What's the benefit of this requirement, as opposed to, for example

   False <= _ = True

I was trying to cover for void types, where the only sensible definitions are

    instance Eq Void where
        _ == _ = error "void (==)"

    instance Ord Void where
        _ <= _ = error "void (<=)"

This is because reflexivity must be guaranteed, so undefined == undefined may not yield False, but I doubt error "foo" == (let x = x in x) should yield True either. But perhaps this exception deserves its own rule.

On Wed, Oct 2, 2013 at 5:36 PM, Roman Cheplyaka <[hidden email]> wrote:
* Stijn van Drongelen <[hidden email]> [2013-10-02 15:46:42+0200]
> I do think something has to be done to have an Eq and Ord with more strict
> laws.
>
> * Operators in Eq and Ord diverge iff any of their parameters are bottom.

This outlaws the Eq instances of lists, trees, and other (co)recursive
types.

Furthermore, in this formulation, even Eq for tuples is illegal, because

  (undefined, something) == somethingElse

is going to diverge.

Roman

I knew this was going to bite me in the ass. Let me try again:

* Operators in Eq and Ord may only diverge when any of their parameters are bottom.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Stijn van Drongelen
On Wed, Oct 2, 2013 at 6:57 PM, Stijn van Drongelen <[hidden email]> wrote:

On Wed, Oct 2, 2013 at 5:36 PM, Roman Cheplyaka <[hidden email]> wrote:
* Stijn van Drongelen <[hidden email]> [2013-10-02 15:46:42+0200]
> I do think something has to be done to have an Eq and Ord with more strict
> laws.
>
> * Operators in Eq and Ord diverge iff any of their parameters are bottom.

This outlaws the Eq instances of lists, trees, and other (co)recursive
types.

Furthermore, in this formulation, even Eq for tuples is illegal, because

  (undefined, something) == somethingElse

is going to diverge.

Roman

I knew this was going to bite me in the ass. Let me try again:

* Operators in Eq and Ord may only diverge when any of their parameters are bottom.

What am I thinking. Scratch that.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Mike Meyer
In reply to this post by Tom Ellis
On Wed, Oct 2, 2013 at 5:18 AM, Tom Ellis <[hidden email]> wrote:
> 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.

Yes, and we already handle it properly:

Prelude> let f = (1.0 /)
Prelude> let (z, negz) = (0.0, -0.0)
Prelude> z == negz
True
Prelude> f z /= f negz
True

This is *not* an "IEEE Floats are weird" thing. Application
programmers want 0.0 to equal -0.0, but -Infinity to not be equal to
Infinity.

Of course, given how many "IEEE Floats are weird" things there are,
you can reasonably consider ignoring this example.

   <mike


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Carter Schonwald
So i think we can conclude the following

1) things are not perfect currently. But it requires some huge type class changes to have a better story

2) certain types of data types will need to be newtyped to have instances that play nice with Ryans concurrency work. Thats ok. Theres often good reasons for those "illegal" instances. There is no sound and COMPLETE way to enforce having "good" instances, and thats a good thing, though having more libs work correctly is always a good thing

3) as always, people complain about floats, when the real issue is the current numerical type classes, which are wrong in a number of ways. I hope to experiment with my own ideas in that direction soon. Not worth a boring no ideas worth taking seriously cafe thread


On Wed, Oct 2, 2013 at 2:39 PM, Mike Meyer <[hidden email]> wrote:
On Wed, Oct 2, 2013 at 5:18 AM, Tom Ellis <[hidden email]> wrote:
> 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.

Yes, and we already handle it properly:

Prelude> let f = (1.0 /)
Prelude> let (z, negz) = (0.0, -0.0)
Prelude> z == negz
True
Prelude> f z /= f negz
True

This is *not* an "IEEE Floats are weird" thing. Application
programmers want 0.0 to equal -0.0, but -Infinity to not be equal to
Infinity.

Of course, given how many "IEEE Floats are weird" things there are,
you can reasonably consider ignoring this example.

   <mike


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Heinrich Apfelmus
In reply to this post by Tom Ellis
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Ryan Newton
In reply to this post by Tillmann Rendel-5
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.



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Any precedent or plan for guaranteed-safe Eq and Ord instances?

Tillmann Rendel-5
Hi,

Ryan Newton wrote:
>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.

I guess that lying Generics instances might arise because of software
evolution. Let's say we start with an abstract data type of binary trees.

   module Tree (Tree, node, empty, null, split) where
     data Tree a = Node (Tree a) (Tree a) | Empty
       deriving Generics

     node = Node

     empty = Empty

     null Empty = True
     null _ = False

     split (Node a b) = (a, b)

     size Empty = 0
     size (Node x y) = size x + size y

Note that this data type is not really abstract, because we export the
Generics instance, so clients of this module can learn about the
implementation of Tree. This is not a big deal, because the chosen
implementation happens to correspond to the abstract structure of binary
trees anyway. So I would expect that generic code will work fine. For
example, you could use generic read and show functions to serialize
trees, and get a reasonable data format.

Now, we want to evolve our module by caching the size of trees. We do
something like this:

   module Tree (Tree, node, empty, null, split) where
     data Tree a = Tree !Int (RealTree a)

     data RealTree a = Node (Tree a) (Tree a) | Empty

     tree (Node a b) = Tree (size a + size b) t
     tree Empty = Tree 0 Empty

     node x y = tree (Node x y)

     empty = tree Empty

     null (Tree _ Empty) = True
     null _ = False

     split (Tree _ (Node a b)) = (a, b)

     size (Tree n _) = n

Except for the Generics instance, we provide the exact same interface
and behavior to our clients, we just traded some space for performance.
But what Generics instance should we provide? If we just add "deriving
Generics" to the two datatypes, we leak the change of representation to
our clients. For example, a client that serialized a tree with a generic
show function based on the old Tree cannot hope to deserialize it back
with a generic read function based on the new Tree. The size information
would be missing, and the structure would be different.

If we write a Generics instance by hand, however, I guess we can make it
present the exact same structure as the derived Generics instance for
the old Tree. With this lying instance, the generic read function will
happily deserialize the old data. The size will be computed on the fly,
because our hand-written Generics instance will introduce calls to our
smart constructors.

   Tillmann
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12