Re: [Haskell-cafe] Re: instance Eq (a - b)
Because it is the most utilitarian way to get a bunch of strict ByteStrings out of a lazy one. Yes it exposes an implementation detail, but the alternatives involve an unnatural amount of copying. -Edward Kmett On Sat, Apr 17, 2010 at 6:37 PM, Ashley Yakeley ash...@semantic.org wrote: Ketil Malde wrote: Do we also want to modify equality for lazy bytestrings, where equality is currently independent of chunk segmentation? (I.e. toChunks s1 == toChunks s2 == s1 == s2 but not vice versa.) Why is toChunks exposed? -- Ashley Yakeley ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
Ashley Yakeley ash...@semantic.org writes: There's an impedance mismatch between the IEEE notion of equality (under which -0.0 == 0.0), and the Haskell notion of equality (where we'd want x == y to imply f x == f y). Do we also want to modify equality for lazy bytestrings, where equality is currently independent of chunk segmentation? (I.e. toChunks s1 == toChunks s2 == s1 == s2 but not vice versa.) My preference would be to keep Eq as it is, a rough approximation of an intuitive notion of equality. -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Thu, 15 Apr 2010, Maciej Piechotka wrote: Are f 0 = 1 f n = f (n - 1) + f (n - 2) and g 0 = 1 g n | n 0 = g (n - 1) + g (n - 2) | n 0 = g (n + 2) - g (n + 1) The same (morally) function? Are: f x = 2*x and f x = undefined The same function Try using the (x == y) == (f x = g y) test yourself. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On 03:53 Thu 15 Apr , rocon...@theorem.ca wrote: On Wed, 14 Apr 2010, Ashley Yakeley wrote: On 2010-04-14 14:58, Ashley Yakeley wrote: On 2010-04-14 13:59, rocon...@theorem.ca wrote: There is some notion of value, let's call it proper value, such that bottom is not one. In other words bottom is not a proper value. Define a proper value to be a value x such that x == x. So neither undefined nor (0.0/0.0) are proper values In fact proper values are not just subsets of values but are also quotients. thus (-0.0) and 0.0 denote the same proper value even though they are represented by different Haskell values. The trouble is, there are functions that can distinguish -0.0 and 0.0. Do we call them bad functions, or are the Eq instances for Float and Double broken? I'd call them disrespectful functions, or maybe nowadays I might call them improper functions. The good functions are respectful functions or proper functions. snip from other post Try using the (x == y) == (f x = g y) test yourself. Your definitions seem very strange, because according to this, the functions f :: Double - Double f x = 1/x and g :: Double - Double g x = 1/x are not equal, since (-0.0 == 0.0) yet f (-0.0) /= g (0.0). -- Nick Bowler, Elliptic Technologies (http://www.elliptictech.com/) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Apr 15, 2010, at 12:53 AM, rocon...@theorem.ca wrote: I'd call them disrespectful functions, or maybe nowadays I might call them improper functions. The good functions are respectful functions or proper functions. There's no need to put these into a different class. The IEEE defined this behavior in 1985, in order to help with rounding error. Floats and doubles are NOT a field, let alone an ordered field. 0.0 =/= -0.0 by design, for floats and doubles. 0.0 == -0.0 for integers, exact computable reals, etc. The problem isn't the functions, or the Eq instance. It's the semantics of the underlying data type -- or equivalently, expecting that floats and doubles form an ordered field. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
Your instances of Finite are not quite right: bottom :: a bottom = doSomethingToLoopInfinitely. instance Finite () where allValues = [(), bottom] instance Finite Nothing where allValues = [bottom] Though at a guess an allValuesExculdingBottom function is also useful, perhaps the class should be class Finite a where allValuesExcludingBottom :: [a] allValues :: Finite a = [a] allValues = (bottom:) . allValuesExcludingBottom Bob On 14 Apr 2010, at 08:01, Ashley Yakeley wrote: Joe Fredette wrote: this is bounded, enumerable, but infinite. The question is whether there are types like this. If so, we would need a new class: class Finite a where allValues :: [a] instance (Finite a,Eq b) = Eq (a - b) where p == q = fmap p allValues == fmap q allValues instance (Finite a,Eq a) = Traversable (a - b) where sequenceA afb = fmap lookup (sequenceA (fmap (\a - fmap (b - (a,b)) (afb a)) allValues)) where lookup :: [(a,b)] - a - b lookup (a,b):_ a' | a == a' = b lookup _:r a' = lookup r a' lookup [] _ = undefined instance Finite () where allValues = [()] data Nothing instance Finite Nothing where allValues = [] -- Ashley Yakeley ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, 2010-04-14 at 08:13 +0100, Thomas Davie wrote: Your instances of Finite are not quite right: bottom :: a bottom = doSomethingToLoopInfinitely. instance Finite () where allValues = [(), bottom] Bottom is not a value, it's failure to evaluate to a value. But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error ABC) vs. (error PQR). Obviously this is not finite. -- Ashley Yakeley ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error ABC) vs. (error PQR). Obviously this is not finite. Nor is it computable, since it must distinguish terminating programs from nonterminating ones (i.e. the halting problem). On a side note, since instance (Finite a, Finite b) = Finite (a - b) should be possible, one can even compare some higher order functions with this approach ;). On 14 April 2010 09:29, Ashley Yakeley ash...@semantic.org wrote: On Wed, 2010-04-14 at 08:13 +0100, Thomas Davie wrote: Your instances of Finite are not quite right: bottom :: a bottom = doSomethingToLoopInfinitely. instance Finite () where allValues = [(), bottom] Bottom is not a value, it's failure to evaluate to a value. But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error ABC) vs. (error PQR). Obviously this is not finite. -- Ashley Yakeley ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On 14 Apr 2010, at 08:29, Ashley Yakeley wrote: On Wed, 2010-04-14 at 08:13 +0100, Thomas Davie wrote: Your instances of Finite are not quite right: bottom :: a bottom = doSomethingToLoopInfinitely. instance Finite () where allValues = [(), bottom] Bottom is not a value, it's failure to evaluate to a value. But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error ABC) vs. (error PQR). Obviously this is not finite. Certainly bottom is a value, and it's a value in *all* Haskell types. Of note, bottom is very important to this question – two functions are not equal unless their behaviour when handed bottom is equal. We also don't need to distinguish different bottoms, there is only one bottom value, the runtime has different side effects when it occurs at different times though. Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On 14 Apr 2010, at 09:01, Jonas Almström Duregård wrote: But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error ABC) vs. (error PQR). Obviously this is not finite. Nor is it computable, since it must distinguish terminating programs from nonterminating ones (i.e. the halting problem). On a side note, since instance (Finite a, Finite b) = Finite (a - b) should be possible, one can even compare some higher order functions with this approach ;). f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. Of course, this is the nature of generally undecidable problems. They are decidable in some cases, but not in general. /Jonas 2010/4/14 Thomas Davie tom.da...@gmail.com: On 14 Apr 2010, at 09:01, Jonas Almström Duregård wrote: But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error ABC) vs. (error PQR). Obviously this is not finite. Nor is it computable, since it must distinguish terminating programs from nonterminating ones (i.e. the halting problem). On a side note, since instance (Finite a, Finite b) = Finite (a - b) should be possible, one can even compare some higher order functions with this approach ;). f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. what about these? f,g :: Bool - Int f x = 6 g x = x `seq` 6 /Jonas 2010/4/14 Thomas Davie tom.da...@gmail.com: On 14 Apr 2010, at 09:01, Jonas Almström Duregård wrote: But if one did start considering bottom to be a value, one would have to distinguish different ones. For instance, (error ABC) vs. (error PQR). Obviously this is not finite. Nor is it computable, since it must distinguish terminating programs from nonterminating ones (i.e. the halting problem). On a side note, since instance (Finite a, Finite b) = Finite (a - b) should be possible, one can even compare some higher order functions with this approach ;). f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On 14 Apr 2010, at 09:08, Jonas Almström Duregård wrote: f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. Of course, this is the nature of generally undecidable problems. They are decidable in some cases, but not in general. Well yes, but we already knew that this was true of function equality – we can't tell in general. Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On 14 Apr 2010, at 09:12, Jonas Almström Duregård wrote: f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. what about these? f,g :: Bool - Int f x = 6 g x = x `seq` 6 As pointed out on #haskell by roconnor, we apparently don't care, this is a shame... We only care that x == y = f x == g y, and x == y can't tell if _|_ == _|_. It's a shame that we can't use this to tell if two functions are equally lazy (something I would consider part of the semantics of the function). Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
what about these? f,g :: Bool - Int f x = 6 g x = x `seq` 6 As pointed out on #haskell by roconnor, we apparently don't care, this is a shame... We only care that x == y = f x == g y, and x == y can't tell if _|_ == _|_. So the facts that (1) f == g (2) f undefined = 6 (3) g undefined = undefined is not a problem? /Jonas 2010/4/14 Thomas Davie tom.da...@gmail.com: On 14 Apr 2010, at 09:12, Jonas Almström Duregård wrote: f,g :: Bool - Int f x = 6 g x = 6 We can in Haskell compute that these two functions are equal, without solving the halting problem. what about these? f,g :: Bool - Int f x = 6 g x = x `seq` 6 As pointed out on #haskell by roconnor, we apparently don't care, this is a shame... We only care that x == y = f x == g y, and x == y can't tell if _|_ == _|_. It's a shame that we can't use this to tell if two functions are equally lazy (something I would consider part of the semantics of the function). Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On 14 Apr 2010, at 09:35, Jonas Almström Duregård wrote: what about these? f,g :: Bool - Int f x = 6 g x = x `seq` 6 As pointed out on #haskell by roconnor, we apparently don't care, this is a shame... We only care that x == y = f x == g y, and x == y can't tell if _|_ == _|_. So the facts that (1) f == g (2) f undefined = 6 (3) g undefined = undefined is not a problem? Yeh :( Shame, isn't it. Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
Ashley Yakeley schrieb: Joe Fredette wrote: this is bounded, enumerable, but infinite. The question is whether there are types like this. If so, we would need a new class: I assume that comparing functions is more oftenly a mistake then actually wanted. Say I have compared f x == f y and later I add a parameter to 'f'. Then the above expression becomes a function comparison. The compiler could not spot this bug but will silently compare functions. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, 14 Apr 2010, Ashley Yakeley wrote: Joe Fredette wrote: this is bounded, enumerable, but infinite. The question is whether there are types like this. If so, we would need a new class: class Finite a where allValues :: [a] instance (Finite a,Eq b) = Eq (a - b) where p == q = fmap p allValues == fmap q allValues As ski noted on #haskell we probably want to extend this to work on Compact types and not just Finite types instance (Compact a, Eq b) = Eq (a - b) where ... For example (Int - Bool) is a perfectly fine Compact set that isn't finite and (Int - Bool) - Int has a decidable equality in Haskell (which Oleg claims that everyone knows ;). I don't know off the top of my head what the class member for Compact should be. I'd guess it should have a member search :: (a - Bool) - a with the specificaiton that p (search p) = True iff p is True from some a. But I'm not sure if this is correct or not. Maybe someone know knows more than I do can claify what the member of the Compact class should be. http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, Apr 14, 2010 at 4:41 AM, rocon...@theorem.ca wrote: As ski noted on #haskell we probably want to extend this to work on Compact types and not just Finite types instance (Compact a, Eq b) = Eq (a - b) where ... For example (Int - Bool) is a perfectly fine Compact set that isn't finite and (Int - Bool) - Int has a decidable equality in Haskell (which Oleg claims that everyone knows ;). I don't know off the top of my head what the class member for Compact should be. I'd guess it should have a member search :: (a - Bool) - a with the specificaiton that p (search p) = True iff p is True from some a. But I'm not sure if this is correct or not. Maybe someone know knows more than I do can claify what the member of the Compact class should be. http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ Here is a summary of my prelude for topology-extras, which never got cool enough to publish. -- The sierpinski space. Two values: T and _|_ (top and bottom); aka. halting and not-halting. -- With a reliable unamb we could implement this as data Sigma = Sigma. -- Note that negation is not a computable function, so we for example split up equality and -- inequality below. data Sigma (\/) :: Sigma - Sigma - Sigma -- unamb (/\) :: Sigma - Sigma - Sigma -- seq class Discrete a where -- equality is observable (===) :: a - a - Sigma class Hausdorff a where -- inequality is observable (=/=) :: a - a - Sigma class Compact a where -- universal quantifiers are computable forevery :: (a - Sigma) - Sigma class Overt a where -- existential quantifiers are computable forsome :: (a - Sigma) - Sigma instance (Compact a, Discrete b) = Discrete (a - b) where f === g = forevery $ \x - f x === g x instance (Overt a, Hausdorff b) = Hausdorff (a - b) where f =/= g = forsome $ \x - f x =/= g x By Tychonoff's theorem we should have: instance (Compact b) = Compact (a - b) where forevert p = ??? But I am not sure whether this is computable, whether (-) counts as a product topology, how it generalizes to ASD-land [1] (in which I am still a noob -- not that I am not a topology noob), etc. Luke [1] Abstract Stone Duality -- a formalization of computable topology. http://www.paultaylor.eu/ASD/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, Apr 14, 2010 at 5:13 AM, Luke Palmer lrpal...@gmail.com wrote: On Wed, Apr 14, 2010 at 4:41 AM, rocon...@theorem.ca wrote: As ski noted on #haskell we probably want to extend this to work on Compact types and not just Finite types instance (Compact a, Eq b) = Eq (a - b) where ... For example (Int - Bool) is a perfectly fine Compact set that isn't finite and (Int - Bool) - Int has a decidable equality in Haskell (which Oleg claims that everyone knows ;). I don't know off the top of my head what the class member for Compact should be. I'd guess it should have a member search :: (a - Bool) - a with the specificaiton that p (search p) = True iff p is True from some a. But I'm not sure if this is correct or not. Maybe someone know knows more than I do can claify what the member of the Compact class should be. http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ Here is a summary of my prelude for topology-extras, which never got cool enough to publish. -- The sierpinski space. Two values: T and _|_ (top and bottom); aka. halting and not-halting. -- With a reliable unamb we could implement this as data Sigma = Sigma. -- Note that negation is not a computable function, so we for example split up equality and -- inequality below. data Sigma (\/) :: Sigma - Sigma - Sigma -- unamb (/\) :: Sigma - Sigma - Sigma -- seq class Discrete a where -- equality is observable (===) :: a - a - Sigma class Hausdorff a where -- inequality is observable (=/=) :: a - a - Sigma class Compact a where -- universal quantifiers are computable forevery :: (a - Sigma) - Sigma class Overt a where -- existential quantifiers are computable forsome :: (a - Sigma) - Sigma instance (Compact a, Discrete b) = Discrete (a - b) where f === g = forevery $ \x - f x === g x instance (Overt a, Hausdorff b) = Hausdorff (a - b) where f =/= g = forsome $ \x - f x =/= g x Elaborating a little, for Eq we need Discrete and Hausdorff, together with some new primitive: -- Takes x and y such that x \/ y = T and x /\ y = _|_, and returns False if x = T and True if y = T. decide :: Sigma - Sigma - Bool Escardo's searchable monad[1][2] from an Abstract Stone Duality perspective actually encodes compact *and* overt. (a - Bool) - a seems a good basis, even though it has a weird spec (it gives you an a for which the predicate returns true, but it's allowed to lie if there is no such a). (a - Bool) - Maybe a seems more appropriate, but it does not compose well. I am not sure how I feel about adding an instance of Eq (a - b). All this topology stuff gets a lot more interesting and enlightening when you talk about Sigma instead of Bool, so I think any sort of Compact constraint on Eq would be a bit ad-hoc. The issues with bottom are subtle and wishywashy enough that, if I were writing the prelude, I would be wary of providing any general mechanism for comparing functions, leaving those decisions to be tailored to the specific problem at hand. On the other hand, with a good unamb (pleez?) and Sigma, I think all these definitions make perfect sense. I think the reason I feel that way is that in Sigma's very essence lies the concept of bottom, whereas with Bool sometimes we like to pretend there is no bottom and sometimes we don't. [1] On hackage: http://hackage.haskell.org/package/infinite-search [2] Article: http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/ By Tychonoff's theorem we should have: instance (Compact b) = Compact (a - b) where forevert p = ??? But I am not sure whether this is computable, whether (-) counts as a product topology, how it generalizes to ASD-land [1] (in which I am still a noob -- not that I am not a topology noob), etc. Luke [1] Abstract Stone Duality -- a formalization of computable topology. http://www.paultaylor.eu/ASD/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, Apr 14, 2010 at 02:07:52AM -0700, Ashley Yakeley wrote: So the facts that (1) f == g (2) f undefined = 6 (3) g undefined = undefined is not a problem? This is not a problem. f and g represent the same moral function, they are just implemented differently. f is smart enough to know that its argument doesn't matter, so it doesn't need to evaluate it. g waits forever trying to evaluate its function, not knowing it doesn't need it. Hence they are distinct functions, and should not be determined to be equal by an equality instance. A compiler will not transform g into f because said distinction is important and part of the definition of a function. Not considering 'bottom' a normal value leads to all sorts of issues when trying to prove properties of a program. Just because they don't occur at run time, you can't pretend they don't exist when reasoning about the meaning of a program, any more than you can reasonably reason about haskell without taking types into account simply because types don't occur in the run-time representation. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, Apr 14, 2010 at 2:22 PM, Stefan Monnier monn...@iro.umontreal.ca wrote: While we're here, I'd be more interested in a dirtyfast comparison operation which could look like: eq :: a - a - IO Bool where the semantics is if (eq x y) returns True, then x and y are the same object, else they may be different. Placing it in IO is not great since its behavior really depends on the compiler rather than on the external world, but at least it would be available. What about something like System.Mem.StableName? Various pointer types from the FFI have Eq instances as well and could potentially be (mis)used to that end. - C. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Apr 14, 2010, at 12:16 PM, Ashley Yakeley wrote: They are distinct Haskell functions, but they represent the same moral function. If you're willing to accept that distinct functions can represent the same moral function, you should be willing to accept that different bottoms represent the same moral value. You're quantifying over equivalence classes either way. And one of them is much simpler conceptually. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Wed, 14 Apr 2010, Ashley Yakeley wrote: On 2010-04-14 13:03, Alexander Solla wrote: If you're willing to accept that distinct functions can represent the same moral function, you should be willing to accept that different bottoms represent the same moral value. Bottoms should not be considered values. They are failures to calculate values, because your calculation would never terminate (or similar condition). Let's not get muddled too much in semantics here. There is some notion of value, let's call it proper value, such that bottom is not one. In other words bottom is not a proper value. Define a proper value to be a value x such that x == x. So neither undefined nor (0.0/0.0) are proper values In fact proper values are not just subsets of values but are also quotients. thus (-0.0) and 0.0 denote the same proper value even though they are represented by different Haskell values. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: instance Eq (a - b)
On Apr 14, 2010, at 5:10 PM, Ashley Yakeley wrote: Worse, this rules out values of types that are not Eq. In principle, every type is an instance of Eq, because every type satisfies the identity function. Unfortunately, you can't DERIVE instances in general. As you are finding out... On the other hand, if you're not comparing things by equality, it hardly matters that you haven't defined the function (==) :: (Eq a) = a - a - Bool for whatever your a is. Put it another way: the existence of the identity function defines -- conceptually, not in code -- instances for Eq. In particular, note that the extension of the identify function is a set of the form (value, value) for EVERY value in the type. A proof that (id x) is x is a proof that x = x. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
