
1234

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 runtime representation.
John

John Meacham  ⑆repetae.net⑆john⑈  http://notanumber.net/_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


> 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 functioncomparison 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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/_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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.
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Wed, 14 Apr 2010, Ashley Yakeley wrote:
> On 20100414 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.''
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On 20100414 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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.
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On 20100414 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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.
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Wed, 14 Apr 2010, Ashley Yakeley wrote:
> On 20100414 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.''
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On 20100414 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On 20100414 14:58, Ashley Yakeley wrote:
> On 20100414 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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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.
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Wed, 20100414 at 12:16 0700, Ashley Yakeley wrote:
> On 20100414 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.
>
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
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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.''
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Wed, 14 Apr 2010, Ashley Yakeley wrote:
> On 20100414 14:58, Ashley Yakeley wrote:
>> On 20100414 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.''
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On Thu, 20100415 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. nonstrict
functions.

Ashley Yakeley
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


On 03:53 Thu 15 Apr , [hidden email] wrote:
> On Wed, 14 Apr 2010, Ashley Yakeley wrote:
>
> > On 20100414 14:58, Ashley Yakeley wrote:
> >> On 20100414 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/)
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe


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.
_______________________________________________
HaskellCafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskellcafe

1234
