instance Eq (a -> b)

classic Classic list List threaded Threaded
70 messages Options
1234
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

John Meacham
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Stefan Monnier
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ertugrul Söylemez
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Casey McCann
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

roconnor
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Alexander Solla-2

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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Alexander Solla-2

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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

roconnor
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Alexander Solla-2

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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Maciej Piechotka
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.
>
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

roconnor
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

roconnor
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
Reply | Threaded
Open this post in threaded view
|

Re: instance Eq (a -> b)

Ashley Yakeley
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Nick Bowler-3
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: instance Eq (a -> b)

Alexander Solla-2
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
1234