instance Eq (a -> b)

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

instance Eq (a -> b)

Ashley Yakeley
Why isn't there an instance Eq (a -> b) ?

   allValues :: (Bounded a,Enum a) => [a]
   allValues = enumFrom minBound

   instance (Bounded a,Enum a,Eq b) => Eq (a -> b) where
     p == q = fmap p allValues == fmap q allValues

Of course, it's not perfect, since empty types are finite but not
Bounded. One can nevertheless make them instances of Bounded with
undefined bounds, and have enumFrom and friends always return the empty
list.

It seems one should also be able to write

   instance (Bounded a,Enum a) => Traversable (a -> b) where ???

But this turns out to be curiously hard.

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

Ivan Lazar Miljenovic
On 14 April 2010 16:03, Ashley Yakeley <[hidden email]> wrote:
> Why isn't there an instance Eq (a -> b) ?

How do you prove that f = (2*) and g x = x + x are equal?
Mathematically, you can; but the only way you can "prove" it in
Haskell is by comparing the values for the entire domain  (which gets
computationally expensive)...

Or, how about higher order functions like map?

--
Ivan Lazar Miljenovic
[hidden email]
IvanMiljenovic.wordpress.com
_______________________________________________
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)

jfredett
In reply to this post by Ashley Yakeley
Consider the set of all rationals with 1 as a numerator, and positive  
denominator, eg:

        S = {1/n, n : Nat}

this is bounded, enumerable, but infinite. Which makes the whole  
checking every value bit somewhat, shall we say, difficult. :)

So for instance, we want to show

        f : S -> S
        f(1/n) = 1/2n

and

        g : S -> S
        g(1/n) = 1/2 * 1/n

would be impossible. Since we would have to check infinitely many  
values of `n`

This, of course, presumes I have understood everything, which seems to  
be less likely every day.


On Apr 14, 2010, at 2:03 AM, Ashley Yakeley wrote:

> Why isn't there an instance Eq (a -> b) ?
>
>  allValues :: (Bounded a,Enum a) => [a]
>  allValues = enumFrom minBound
>
>  instance (Bounded a,Enum a,Eq b) => Eq (a -> b) where
>    p == q = fmap p allValues == fmap q allValues
>
> Of course, it's not perfect, since empty types are finite but not  
> Bounded. One can nevertheless make them instances of Bounded with  
> undefined bounds, and have enumFrom and friends always return the  
> empty list.
>
> It seems one should also be able to write
>
>  instance (Bounded a,Enum a) => Traversable (a -> b) where ???
>
> But this turns out to be curiously hard.
>
> --
> Ashley Yakeley
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
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 Ivan Lazar Miljenovic
On Wed, 2010-04-14 at 16:11 +1000, Ivan Miljenovic wrote:
> but the only way you can "prove" it in
> Haskell is by comparing the values for the entire domain  (which gets
> computationally expensive)...

It's not expensive if the domain is, for instance, Bool.

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

Jonas Almström Duregård
I guess nontermination is a problem (e.g. if one or both functions
fail to terminate for some values, equality will be undecidable).

/Jonas

On 14 April 2010 08:42, Ashley Yakeley <[hidden email]> wrote:

> On Wed, 2010-04-14 at 16:11 +1000, Ivan Miljenovic wrote:
>> but the only way you can "prove" it in
>> Haskell is by comparing the values for the entire domain  (which gets
>> computationally expensive)...
>
> It's not expensive if the domain is, for instance, Bool.
>
> --
> Ashley Yakeley
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
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 jfredett
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Thomas Davie
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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

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

Ashley Yakeley
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Jonas Almström Duregård
> 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
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)

Ketil Malde-5
In reply to this post by jfredett

Joe Fredette <[hidden email]> writes:

> Consider the set of all rationals with 1 as a numerator, and positive
> denominator, eg:
>
> S = {1/n, n : Nat}

> this is bounded, enumerable, but infinite.

Isn't making this an instance of Enum something of an abuse?

How would you use enumFromThenTo (or equivalently, [x0,x1..xn]) for
these fractions?  I think the intuition is that you can use 'enumFromTo
minBound maxBound' to exhaustively list the values in a type.
E.g. Ashley's own:

>>   allValues :: (Bounded a,Enum a) => [a]
>>   allValues = enumFrom minBound

But this doesn't work for Double (or rational), either, so it's abuse
with some precedent.

Another practical consideration is that checking a function taking a
simple Int parameter for equality would mean 2^65 function evaluations.
I think function equality would be too much of a black hole to be
worth it.

-k
--
If I haven't seen further, it is by standing in the footprints of giants
_______________________________________________
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)

Thomas Davie
In reply to this post by Ashley Yakeley

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Thomas Davie
In reply to this post by Jonas Almström Duregård

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
[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 Ketil Malde-5
Ketil Malde wrote:
> Another practical consideration is that checking a function taking a
> simple Int parameter for equality would mean 2^65 function evaluations.
> I think function equality would be too much of a black hole to be
> worth it.

Oh FFS, _don't do that_.

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

Jonas Almström Duregård
In reply to this post by Thomas Davie
> 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 <[hidden email]>:

>
> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Jonas Almström Duregård
In reply to this post by Thomas Davie
> 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 <[hidden email]>:

>
> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Thomas Davie
In reply to this post by Jonas Almström Duregård

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Thomas Davie
In reply to this post by Jonas Almström Duregård

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
[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 Thomas Davie
Thomas Davie wrote:
> Certainly bottom is a value, and it's a value in *all* Haskell types.

This is a matter of interpretation. If you consider bottom to be a
value, then all the laws fail. For instance, (==) is supposed to be
reflexive, but "undefined == undefined" is not True for almost any type.

For this reason I recommend "fast and loose reasoning":
http://www.cs.nott.ac.uk/~nad/publications/danielsson-et-al-popl2006.html

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

Maciej Piechotka
In reply to this post by Ashley Yakeley
On Tue, 2010-04-13 at 23:03 -0700, Ashley Yakeley wrote:

> Why isn't there an instance Eq (a -> b) ?
>
>    allValues :: (Bounded a,Enum a) => [a]
>    allValues = enumFrom minBound
>
>    instance (Bounded a,Enum a,Eq b) => Eq (a -> b) where
>      p == q = fmap p allValues == fmap q allValues
>
> Of course, it's not perfect, since empty types are finite but not
> Bounded. One can nevertheless make them instances of Bounded with
> undefined bounds, and have enumFrom and friends always return the empty
> list.
>
I guess that the fact that:
- It is costly. On modern machine comparing Int -> a functions would
take 18446744073709551615 steps. Using optimistic assumption (3 GHz, 1
clock per check) it would take 185948 years. Ok - it can be parallelised
but  it would make it better by factor of 16 (which would be
monumentally offset by the fact you likely have this 16 clock cycles
spent on computation/memory access etc.).
- It is rarely needed. I had much often errors about missing Eq (a -> b)
instances when I had error then I needed it.

> It seems one should also be able to write
>
>    instance (Bounded a,Enum a) => Traversable (a -> b) where ???
>
> But this turns out to be curiously hard.
>

To begin with {_|_} -> R - LHS is finite (so bound and enumerable) but
there is uncountable number of such functions.

Q⋂[0,1] -> Q⋂[0,1] -Is not countable (enumerable) as well.
Q⋂[0,1] -> {0,1} - Also uncountable (due to diagonalisation argument)
IIRC

Regards


_______________________________________________
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: instance Eq (a -> b)

Thomas Davie
In reply to this post by Ashley Yakeley

On 14 Apr 2010, at 09:17, Ashley Yakeley wrote:

> Thomas Davie wrote:
>> Certainly bottom is a value, and it's a value in *all* Haskell types.
>
> This is a matter of interpretation. If you consider bottom to be a value, then all the laws fail. For instance, (==) is supposed to be reflexive, but "undefined == undefined" is not True for almost any type.
>
> For this reason I recommend "fast and loose reasoning":
> http://www.cs.nott.ac.uk/~nad/publications/danielsson-et-al-popl2006.html

It might be nice to have a definition of whether we consider bottom to be a value in Haskell then, because the definition of second and fmap on tuples are different because of this consideration:

fmap f (x,y) = (x,f y)
second f ~(x,y) = (x,f y)

Because we consider that the Functor laws must hold for all values in the type (including bottom).

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