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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
> 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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
In reply to this post by Jonas Almström Duregård
On 14 Apr 2010, at 09:12, Jonas Almström Duregård wrote:
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 |
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 |
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. > - 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 |
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 |
Free forum by Nabble | Edit this page |