Re: [Haskell-cafe] Equality of functions
[EMAIL PROTECTED] wrote: That is too pessimistic, I'm afraid. There is also an intensional equality. Granted, it can be sound but never, in general, complete (although it can be total). That is, if the comparison function returns True, then the arguments truly denote the same, identically the same function. If the answer is False, well, we don't know. The arguments may still denote the same function. That means it is a four valued modal logic... it should really return AllTrue or SomeFalse... (I think, assuming that the false meant at least one false answer). Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Equality of functions
Hi All, After some weeks of experimenting and digging around, I understand that functions cannot be compared for equality. Thanks to Bjorn Lisper for pointing this out. I basically understand (?) the underlying mathematical issue, which is that functions in general may have infinite domains and ranges. For example, a function f, which gives the successor of an integer, x + 1, could not be compared to a function g, which gives the predecessor of an integer which has 2 added, (x + 2) - 1, even though these two functions give exactly the same result on all arguments, because we would have to compare them on all possible values for x. Question -- is this all there is to the issue, or is there something more? Apologies in advance for not understanding the math better here. Question -- though Haskell, as a lazy language, does not otherwise have problems with infinite lists, why does it here? Question -- is there some way around this problem? It is very handy to be able to have a variable over functions and then compare the value to a designated function. This would let me say things like: when variableFunctionX == functionA then otherwise etc... One possible (dirty?) solution I thought up is to use the record types of Hugs to correlate the function with a name of type String: type FunctionNameFunction = Rec (functionName :: String, functionFunction :: WhateverFunction) Then, whenever one needs to use the function, one uses the value of functionFunction, but whenever one needs to evaluate for identity, one uses the value of functionName, using just string identity. Of course, this makes lots of things less 'pretty' (to apply a function to an argument, one has to first 'pull out' the function from the record), but it addresses a general problem. One would also have to keep careful track of which functionNames correlate with with functionFunctions. Other suggestions? Cheers, Adam ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality of functions
Adam Zachary Wyner wrote: Question -- is this all there is to the issue, or is there something more? Apologies in advance for not understanding the math better here. You can compare functions in a pointwise fashion, which does not work (other than approximatively) for infinite domains. This is the black box approach. You can also compare functions in a proof-theoretic fashion. Try to proof a derivation that f can be transformed into g. This is the white-box approach. This requires reasoning at the level of program text. Question -- though Haskell, as a lazy language, does not otherwise have problems with infinite lists, why does it here? Because lazyness only helps in cases where we don't want to see the full infinite data structure. Equality is a universal property; we would need to iterate over all elements of the domain. Question -- is there some way around this problem? It is very handy to be able to have a variable over functions and then compare the value to a designated function. This would let me say things like: when variableFunctionX == functionA then otherwise etc... Don't understand. One possible (dirty?) solution I thought up is to use the record types of Hugs to correlate the function with a name of type String: type FunctionNameFunction = Rec (functionName :: String, functionFunction :: WhateverFunction) Then, whenever one needs to use the function, one uses the value of functionFunction, but whenever one needs to evaluate for identity, one uses the value of functionName, using just string identity. Of course, this makes lots of things less 'pretty' (to apply a function to an argument, one has to first 'pull out' the function from the record), but it addresses a general problem. One would also have to keep careful track of which functionNames correlate with with functionFunctions. Yes, one can represent functions by type codes. These type codes would be interpreted by an Apply class (as in the HList library). Type codes could be compared for equality (again demonstrated in the HList paper). Modulo some extra tweaking, we can compute type equality for such *fixed* functions. In fact, one can build a little functional language in the type system this way. Expressions in this language would distinguished terms. One could even implement the abovementioned white-box approach in the type system. (For any given system of proof/transformation rules.) I am sure this is too complicated and too restricted than to be truly useful. Cheers, Ralf ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality of functions
On 30 Nov 2004, at 13:22, Adam Zachary Wyner wrote: Question -- is this all there is to the issue, or is there something more? Apologies in advance for not understanding the math better here. From the point of view of a programmer, that's all there is to it: there is no way of proving two functions are the same except by exhaustively checking every input. Question -- though Haskell, as a lazy language, does not otherwise have problems with infinite lists, why does it here? Try [1..]==[1..] You'll find it runs forever. (Aside: [1..]==[2..] returns False straightaway, though) In the same sense, you could try (map f [1..]) == (map g [1..]) and it will return False quickly if they are different, but it will run forever if they are the same. Question -- is there some way around this problem? It is very handy to be able to have a variable over functions and then compare the value to a designated function. This would let me say things like: You don't need records to pair functions with strings, but yes, one way to do this is to make your functions more structured types and compare them some other way. If you happen to know all your functions are 2nd order polynomials, then it suffices to check them at three points (or, check f, f', and f'' at 0, say): you could implement equality checks this way. In other function domains there may be other effective equality tests. The general situation is: there is no effective way to check the equality of functions on infinite domains. However, for most particular classes of functions you would actually want to compare, there are specific effective procedures. Jules ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality of functions
On Tue, 2004-11-30 at 13:52 +, Jules Bean wrote: In the same sense, you could try (map f [1..]) == (map g [1..]) and it will return False quickly if they are different, but it will run forever if they are the same. For some very generous definition of quickly :) Bernie. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality of functions
On 1 Dec 2004, at 01:06, Bernard Pope wrote: On Tue, 2004-11-30 at 13:52 +, Jules Bean wrote: In the same sense, you could try (map f [1..]) == (map g [1..]) and it will return False quickly if they are different, but it will run forever if they are the same. For some very generous definition of quickly :) With respect to the fact that we do not know how fast f or g run, the only way to define quickly in this sense is relative to how fast f and g run. We can return False from (map f [1..]) == (map g [1..]) with a constant time slow down from returning False from (f 1) == (g 1). I'd call constant time reasonably 'quickly'. Bob -- What is the internet? It's the largest equivalence class in the reflexive transitive symmetric closure of the relationship can be reached by an IP packet from. -- Seth Breidbart ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality of functions
Woops... scratch my stupitity... we could of course discover the test to be false on an extremely large integer. Bob -- God is real... Unless you define it as an integer. On 1 Dec 2004, at 01:19, Thomas Davie wrote: On 1 Dec 2004, at 01:06, Bernard Pope wrote: On Tue, 2004-11-30 at 13:52 +, Jules Bean wrote: In the same sense, you could try (map f [1..]) == (map g [1..]) and it will return False quickly if they are different, but it will run forever if they are the same. For some very generous definition of quickly :) With respect to the fact that we do not know how fast f or g run, the only way to define quickly in this sense is relative to how fast f and g run. We can return False from (map f [1..]) == (map g [1..]) with a constant time slow down from returning False from (f 1) == (g 1). I'd call constant time reasonably 'quickly'. Bob -- What is the internet? It's the largest equivalence class in the reflexive transitive symmetric closure of the relationship can be reached by an IP packet from. -- Seth Breidbart ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality of functions
Adam Zachary Wyner wrote: Hi All, After some weeks of experimenting and digging around, I understand that functions cannot be compared for equality. Thanks to Bjorn Lisper for pointing this out. I basically understand (?) the underlying mathematical issue, which is that functions in general may have infinite domains... Other suggestions? You can define equality for functions with finite domains. See the enclosed Haskell module. Loading package base ... linking ... done. Compiling Finite ( Finite.hs, interpreted ) Ok, modules loaded: Finite. *Finite not == not True *Finite () == () True *Finite () == (||) False -- Thomas H module Finite where instance (Finite a, Eq b) = Eq (a-b) where f == g = and [ f x == g x | x - allValues ] -- A class for finite types class Finite a where allValues :: [a] instance Finite () where allValues = [()] instance Finite Bool where allValues = [False,True] --instance Finite Ordering where ... --instance Finite Char where ... --instance Finite Int where ... instance (Finite a,Finite b) = Finite (a,b) where allValues = [ (x,y) | x-allValues, y-allValues] instance Finite a = Finite (Maybe a) where allValues = Nothing:[Just x|x-allValues] instance (Finite a,Finite b) = Finite (Either a b) where allValues = [Left x|x-allValues]++[Right y|y-allValues] -- ... ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality of functions
Jules Bean wrote: From the point of view of a programmer, that's all there is to it: there is no way of proving two functions are the same except by exhaustively checking every input. That is too pessimistic, I'm afraid. There is also an intensional equality. Granted, it can be sound but never, in general, complete (although it can be total). That is, if the comparison function returns True, then the arguments truly denote the same, identically the same function. If the answer is False, well, we don't know. The arguments may still denote the same function. Here's one example of intensional comparison: import Foreign comp a b = do pa - newStablePtr a pb - newStablePtr b let res = pa == pb freeStablePtr pa freeStablePtr pb return res *FD comp id id = print True *FD comp undefined id = print False *FD comp undefined undefined = print True This function lives in the IO monad, where it should stay because it destroys free theorems. It is quite equivalent to Scheme's eq? predicate. For some -- wide -- classes of functions, it is possible to define a pure functional intensional comparison. For example, a recent message http://www.haskell.org/pipermail/haskell/2004-November/014939.html demonstrated the reconstruction of (even compiled) numerical functions. So, one can define intensional equality of two numeric functions as structural equality of their reconstructed representations. Alas, this comparison function can't be total: bottom is beyond comparison. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
