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

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

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 _)

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 ren...@informatik.uni-marburg.de 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

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,

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

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-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

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

2013-10-02 Thread Roman Cheplyaka
* Heinrich Apfelmus apfel...@quantentunnel.de [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

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
* Tillmann Rendel ren...@informatik.uni-marburg.de [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

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 = x)

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 rhym...@gmail.com 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`

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 rhym...@gmail.com 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

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 hask...@nand.wakku.to wrote: On Wed, 2 Oct 2013 15:46:42 +0200, Stijn van Drongelen rhym...@gmail.com 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

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 ___

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

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

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 Stijn van Drongelen
On Wed, Oct 2, 2013 at 6:57 PM, Stijn van Drongelen rhym...@gmail.comwrote: On Wed, Oct 2, 2013 at 5:36 PM, Roman Cheplyaka r...@ro-che.info wrote: * Stijn van Drongelen rhym...@gmail.com [2013-10-02 15:46:42+0200] I do think something has to be done to have an Eq and Ord with more strict

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 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

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 would