Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-06 Thread Ryan Newton
Tillmann, Thanks, that is in interesting use case for handwritten Generics. I'm not fully dissuaded though, simply because: (1) it can't be too common! Especially when you intersect the people who have done or will do this with the people who care about SafeHaskell. (Again, if they don't, they

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-06 Thread adam vogt
On Sun, Oct 6, 2013 at 6:54 PM, Tillmann Rendel wrote: > 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 instanc

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-06 Thread Carter Schonwald
(replicating what i said on the ghc-devs thread) 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 _) (MkAn

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-06 Thread Tillmann Rendel
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 abs

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-06 Thread 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 co

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-04 Thread Heinrich Apfelmus
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 differen

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread 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 reaso

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Mike Meyer
On Wed, Oct 2, 2013 at 5:18 AM, Tom Ellis < tom-lists-haskell-cafe-2...@jaguarpaw.co.uk> 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

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Stijn van Drongelen
On Wed, Oct 2, 2013 at 6:57 PM, Stijn van Drongelen wrote: > > On Wed, Oct 2, 2013 at 5:36 PM, Roman Cheplyaka wrote: > >> * Stijn van Drongelen [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 an

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Stijn van Drongelen
On Wed, Oct 2, 2013 at 4:17 PM, Tom Ellis < tom-lists-haskell-cafe-2...@jaguarpaw.co.uk> 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

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Roman Cheplyaka
* Stijn van Drongelen [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. Furth

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Tom Ellis
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 ___ Hask

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Stijn van Drongelen
On Wed, Oct 2, 2013 at 3:49 PM, Niklas Haas wrote: > On Wed, 2 Oct 2013 15:46:42 +0200, Stijn van Drongelen > 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. > > *

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Colin Adams
Only for meanings of "better" which do not imply as good performance. On 2 October 2013 14:46, Stijn van Drongelen 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 de

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Niklas Haas
On Wed, 2 Oct 2013 15:46:42 +0200, Stijn van Drongelen 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. >

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Stijn van Drongelen
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 <=

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Roman Cheplyaka
* Tillmann Rendel [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 > >responsi

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Tillmann Rendel
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.

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread Roman Cheplyaka
* Heinrich Apfelmus [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 equivale

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread 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 impl

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-02 Thread 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!"

Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?

2013-10-01 Thread 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 woul