# instance Eq (a -> b)

70 messages
1234
Open this post in threaded view
|

## instance Eq (a -> b)

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

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

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

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

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

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

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

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

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

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

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

## Re: 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

## Re: 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 <[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
Open this post in threaded view
|

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 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 -> Intf x = 6g x = 6We can in Haskell compute that these two functions are equal, without solving the halting problem.what about these?f,g :: Bool -> Intf x = 6g x = x `seq` 6As 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
Open this post in threaded view
|

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

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

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

 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