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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Ashley Yakeley
> Why isn't there an instance Eq (a -> b) ?
I guess it's because even for those cases where it can be written, it will rarely be what you want to do, so it's better to require the programmer to explicitly request a function-comparison than to risk silently using such a costly operation when the programmer intended no such thing. While we're here, I'd be more interested in a dirty&fast 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. Stefan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Stefan Monnier <[hidden email]> wrote:
> While we're here, I'd be more interested in a dirty&fast 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's "the same object"? Functions and values have no identity in Haskell. The best you can do is to ask, whether the arguments refer to the same thunk in memory (sharing), but as you say the answer isn't portable. It's also not much useful IMO. Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://blog.ertes.de/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Stefan Monnier
On Wed, Apr 14, 2010 at 2:22 PM, Stefan Monnier
<[hidden email]> wrote: > While we're here, I'd be more interested in a dirty&fast 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Ashley Yakeley
On Wed, 14 Apr 2010, Ashley Yakeley wrote:
> On 2010-04-14 03:41, [hidden email] wrote: >> For example (Int -> Bool) is a perfectly fine Compact set that isn't >> finite > > Did you mean "Integer -> Bool"? "Int -> Bool" is finite, but large. Yes, I meant Integer -> Bool. -- 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by John Meacham
On 2010-04-14 11:12, John Meacham wrote:
> 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, They are distinct Haskell functions, but they represent the same moral function. > and should not be determined to be equal by an equality instance. I don't see why not. It doesn't break the expected Eq laws of reflexivity, symmetry, transitivity. Also, it supports this law: if f == g = True, then f x == g x = True ... in exactly the same way that it supports reflexivity, that is, "fast and loose" ignoring bottom. > A compiler will not transform g into f > because said distinction is important and part of the definition of a > function. I'm not seeing this implication as part of the semantics of (==). -- Ashley Yakeley _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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). -- Ashley Yakeley _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Apr 14, 2010, at 1:24 PM, Ashley Yakeley wrote: > Bottoms should not be considered values. They are failures to > calculate values, because your calculation would never terminate (or > similar condition). And yet you are trying to recover the semantics of comparing bottoms. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On 2010-04-14 13:31, Alexander Solla wrote:
> And yet you are trying to recover the semantics of comparing bottoms. No, I don't think so. -- Ashley Yakeley _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Ashley Yakeley
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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On 2010-04-14 13:59, [hidden email] 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? -- Ashley Yakeley _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On 2010-04-14 14:58, Ashley Yakeley wrote:
> On 2010-04-14 13:59, [hidden email] 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? Worse, this rules out values of types that are not Eq. -- Ashley Yakeley _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Ashley Yakeley
On Wed, 2010-04-14 at 12:16 -0700, Ashley Yakeley wrote:
> On 2010-04-14 11:12, John Meacham wrote: > > 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, > > They are distinct Haskell functions, but they represent the same > moral > function. > 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe signature.asc (853 bytes) Download Attachment |
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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Ashley Yakeley
On Wed, 14 Apr 2010, Ashley Yakeley wrote:
> On 2010-04-14 14:58, Ashley Yakeley wrote: >> On 2010-04-14 13:59, [hidden email] 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. Proper functions are functions that are proper values i.e. f == f which is defined to mean that (x == y) ==> f x == f y (even if this isn't a decidable relation). > Worse, this rules out values of types that are not Eq. Hmm, I guess I'm carrying all this over from the world of dependently typed programming where we have setoids and the like that admit equality relations that are not necessarily decidable. In Haskell only the decidable instances of equality manage to have a Eq instance. The other data types one has an (partial) equivalence relation in mind but it goes unwritten. But in my dependently typed world we don't have partial values so there are no bottoms to worry about; maybe these ideas don't carry over perfectly. -- 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Thu, 2010-04-15 at 03:53 -0400, [hidden email] wrote:
> Hmm, I guess I'm carrying all this over from the world of dependently > typed programming where we have setoids and the like that admit equality > relations that are not necessarily decidable. In Haskell only the > decidable instances of equality manage to have a Eq instance. The other > data types one has an (partial) equivalence relation in mind but it goes > unwritten. > > But in my dependently typed world we don't have partial values so there > are no bottoms to worry about; maybe these ideas don't carry over > perfectly. It's an interesting approach, though, since decided equality seems to capture the idea of "full value" fairly well. I'm currently thinking along the lines of a set V of "Platonic" values, while Haskell names are bound to expressions that attempt to calculate these values. At any given time during the calculation, an expression can be modelled as a subset of V. Initially, it's V, as calculation progresses it may become progressively smaller subsets of V. Saying a calculation is bottom is to make a prediction that cannot in general be decided. It's to say that the calculation will always be V. If it ever becomes not V, it's a "partial value". If it ever becomes a singleton, it's a "complete value". On the other hand, this approach may not help with strict vs. non-strict functions. -- Ashley Yakeley _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by roconnor
On 03:53 Thu 15 Apr , [hidden email] wrote:
> On Wed, 14 Apr 2010, Ashley Yakeley wrote: > > > On 2010-04-14 14:58, Ashley Yakeley wrote: > >> On 2010-04-14 13:59, [hidden email] 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by roconnor
On Apr 15, 2010, at 12:53 AM, [hidden email] 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |