Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition.

In general? No If we had an implementation of the `sin` function, how
can testing a finite number of points along it determine if that implementation is correct for every point? For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set. Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness. Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :) /Joe On Oct 12, 2009, at 1:42 PM, muad wrote: > > Is it possible to prove correctness of a functions by testing it? I > think the > tests would have to be constructed by inspecting the shape of the > function > definition. > >  > View this message in context: http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html > Sent from the Haskell  HaskellCafe mailing list archive at > Nabble.com. > > _______________________________________________ > HaskellCafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskellcafe _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
It is possible for functions with compact domain, not just finite.
2009/10/12 Joe Fredette <[hidden email]>: > In general? No If we had an implementation of the `sin` function, how can > testing a finite number of points along it determine > if that implementation is correct for every point? > > For specific functions (particularly those with finite domain), it is > possible. If you know the 'correct' output of every input, then testing each > input and ensuring correct output will work. Consider the definition of the > `not` function on booleans. The domain only has two elements (True and > False) and the range has only two outputs (True and False), so if I test > every input, and insure it maps appropriately to the specified output, we're > all set. > > Basically, if you can write your function as a big case statement that > covers the whole domain, and that domain is finite, then the function can be > tested to prove it's correctness. > > Now, I should think the Muad'Dib would know that, perhaps you should go back > to studying with the Mentats. :) > > /Joe > > > > On Oct 12, 2009, at 1:42 PM, muad wrote: > >> >> Is it possible to prove correctness of a functions by testing it? I think >> the >> tests would have to be constructed by inspecting the shape of the function >> definition. >> >>  >> View this message in context: >> http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html >> Sent from the Haskell  HaskellCafe mailing list archive at Nabble.com. >> >> _______________________________________________ >> HaskellCafe mailing list >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskellcafe > > _______________________________________________ > HaskellCafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskellcafe >  Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
For example, it is possible to prove correctness of a function
"negatedHead :: [Bool] > Bool" by testing it on "True:undefined" and "False:undefined". 2009/10/12 Eugene Kirpichov <[hidden email]>: > It is possible for functions with compact domain, not just finite. > > 2009/10/12 Joe Fredette <[hidden email]>: >> In general? No If we had an implementation of the `sin` function, how can >> testing a finite number of points along it determine >> if that implementation is correct for every point? >> >> For specific functions (particularly those with finite domain), it is >> possible. If you know the 'correct' output of every input, then testing each >> input and ensuring correct output will work. Consider the definition of the >> `not` function on booleans. The domain only has two elements (True and >> False) and the range has only two outputs (True and False), so if I test >> every input, and insure it maps appropriately to the specified output, we're >> all set. >> >> Basically, if you can write your function as a big case statement that >> covers the whole domain, and that domain is finite, then the function can be >> tested to prove it's correctness. >> >> Now, I should think the Muad'Dib would know that, perhaps you should go back >> to studying with the Mentats. :) >> >> /Joe >> >> >> >> On Oct 12, 2009, at 1:42 PM, muad wrote: >> >>> >>> Is it possible to prove correctness of a functions by testing it? I think >>> the >>> tests would have to be constructed by inspecting the shape of the function >>> definition. >>> >>>  >>> View this message in context: >>> http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html >>> Sent from the Haskell  HaskellCafe mailing list archive at Nabble.com. >>> >>> _______________________________________________ >>> HaskellCafe mailing list >>> [hidden email] >>> http://www.haskell.org/mailman/listinfo/haskellcafe >> >> _______________________________________________ >> HaskellCafe mailing list >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskellcafe >> > > > >  > Eugene Kirpichov > Web IR developer, market.yandex.ru >  Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Eugene Kirpichov
Really? How? That sounds very interesting, I've got a fair knowledge
of basic topology, I'd love to see an application to programming... On Oct 12, 2009, at 1:55 PM, Eugene Kirpichov wrote: > It is possible for functions with compact domain, not just finite. > > 2009/10/12 Joe Fredette <[hidden email]>: >> In general? No If we had an implementation of the `sin` function, >> how can >> testing a finite number of points along it determine >> if that implementation is correct for every point? >> >> For specific functions (particularly those with finite domain), it is >> possible. If you know the 'correct' output of every input, then >> testing each >> input and ensuring correct output will work. Consider the >> definition of the >> `not` function on booleans. The domain only has two elements (True >> and >> False) and the range has only two outputs (True and False), so if I >> test >> every input, and insure it maps appropriately to the specified >> output, we're >> all set. >> >> Basically, if you can write your function as a big case statement >> that >> covers the whole domain, and that domain is finite, then the >> function can be >> tested to prove it's correctness. >> >> Now, I should think the Muad'Dib would know that, perhaps you >> should go back >> to studying with the Mentats. :) >> >> /Joe >> >> >> >> On Oct 12, 2009, at 1:42 PM, muad wrote: >> >>> >>> Is it possible to prove correctness of a functions by testing it? >>> I think >>> the >>> tests would have to be constructed by inspecting the shape of the >>> function >>> definition. >>> >>>  >>> View this message in context: >>> http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html >>> Sent from the Haskell  HaskellCafe mailing list archive at >>> Nabble.com. >>> >>> _______________________________________________ >>> HaskellCafe mailing list >>> [hidden email] >>> http://www.haskell.org/mailman/listinfo/haskellcafe >> >> _______________________________________________ >> HaskellCafe mailing list >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskellcafe >> > > > >  > Eugene Kirpichov > Web IR developer, market.yandex.ru _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Eugene Kirpichov
Also google "seemingly impossible functional programs".
2009/10/12 Eugene Kirpichov <[hidden email]>: > For example, it is possible to prove correctness of a function > "negatedHead :: [Bool] > Bool" by testing it on "True:undefined" and > "False:undefined". > > 2009/10/12 Eugene Kirpichov <[hidden email]>: >> It is possible for functions with compact domain, not just finite. >> >> 2009/10/12 Joe Fredette <[hidden email]>: >>> In general? No If we had an implementation of the `sin` function, how can >>> testing a finite number of points along it determine >>> if that implementation is correct for every point? >>> >>> For specific functions (particularly those with finite domain), it is >>> possible. If you know the 'correct' output of every input, then testing each >>> input and ensuring correct output will work. Consider the definition of the >>> `not` function on booleans. The domain only has two elements (True and >>> False) and the range has only two outputs (True and False), so if I test >>> every input, and insure it maps appropriately to the specified output, we're >>> all set. >>> >>> Basically, if you can write your function as a big case statement that >>> covers the whole domain, and that domain is finite, then the function can be >>> tested to prove it's correctness. >>> >>> Now, I should think the Muad'Dib would know that, perhaps you should go back >>> to studying with the Mentats. :) >>> >>> /Joe >>> >>> >>> >>> On Oct 12, 2009, at 1:42 PM, muad wrote: >>> >>>> >>>> Is it possible to prove correctness of a functions by testing it? I think >>>> the >>>> tests would have to be constructed by inspecting the shape of the function >>>> definition. >>>> >>>>  >>>> View this message in context: >>>> http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html >>>> Sent from the Haskell  HaskellCafe mailing list archive at Nabble.com. >>>> >>>> _______________________________________________ >>>> HaskellCafe mailing list >>>> [hidden email] >>>> http://www.haskell.org/mailman/listinfo/haskellcafe >>> >>> _______________________________________________ >>> HaskellCafe mailing list >>> [hidden email] >>> http://www.haskell.org/mailman/listinfo/haskellcafe >>> >> >> >> >>  >> Eugene Kirpichov >> Web IR developer, market.yandex.ru >> > > > >  > Eugene Kirpichov > Web IR developer, market.yandex.ru >  Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Eugene Kirpichov
Oh thanks for the example, I suppose you can disregard my other
message. I suppose this is a bit like shortcircuiting. No? On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote: > For example, it is possible to prove correctness of a function > "negatedHead :: [Bool] > Bool" by testing it on "True:undefined" and > "False:undefined". > > 2009/10/12 Eugene Kirpichov <[hidden email]>: >> It is possible for functions with compact domain, not just finite. >> >> 2009/10/12 Joe Fredette <[hidden email]>: >>> In general? No If we had an implementation of the `sin` function, >>> how can >>> testing a finite number of points along it determine >>> if that implementation is correct for every point? >>> >>> For specific functions (particularly those with finite domain), it >>> is >>> possible. If you know the 'correct' output of every input, then >>> testing each >>> input and ensuring correct output will work. Consider the >>> definition of the >>> `not` function on booleans. The domain only has two elements (True >>> and >>> False) and the range has only two outputs (True and False), so if >>> I test >>> every input, and insure it maps appropriately to the specified >>> output, we're >>> all set. >>> >>> Basically, if you can write your function as a big case statement >>> that >>> covers the whole domain, and that domain is finite, then the >>> function can be >>> tested to prove it's correctness. >>> >>> Now, I should think the Muad'Dib would know that, perhaps you >>> should go back >>> to studying with the Mentats. :) >>> >>> /Joe >>> >>> >>> >>> On Oct 12, 2009, at 1:42 PM, muad wrote: >>> >>>> >>>> Is it possible to prove correctness of a functions by testing it? >>>> I think >>>> the >>>> tests would have to be constructed by inspecting the shape of the >>>> function >>>> definition. >>>> >>>>  >>>> View this message in context: >>>> http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html >>>> Sent from the Haskell  HaskellCafe mailing list archive at >>>> Nabble.com. >>>> >>>> _______________________________________________ >>>> HaskellCafe mailing list >>>> [hidden email] >>>> http://www.haskell.org/mailman/listinfo/haskellcafe >>> >>> _______________________________________________ >>> HaskellCafe mailing list >>> [hidden email] >>> http://www.haskell.org/mailman/listinfo/haskellcafe >>> >> >> >> >>  >> Eugene Kirpichov >> Web IR developer, market.yandex.ru >> > > > >  > Eugene Kirpichov > Web IR developer, market.yandex.ru _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by muad
On Mon, Oct 12, 2009 at 10:42 AM, muad <[hidden email]> wrote:
> > Is it possible to prove correctness of a functions by testing it? I think the > tests would have to be constructed by inspecting the shape of the function > definition. not True==False not False==True Done. Tested :) Less trivially, consider a function of signature swap :: (a,b) > (b,a) We don't need to test it at all, it can only do one thing, swap its arguments. (Assuming it terminates.) But consider: swap :: (a,a) > (a,a) If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x) for all types a and b. We only need one test. The reason is that we have a free theorem that says that for all functions, f, of type (a,a) > (a,a) this holds: f (g a,g b) == let (x,y) = f (a,b) in (g x',g y') For any x and y define g 1 = x g 2 = y Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') == let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x) In other words, free theorems can turn an infinite amount of testing into a finite test. (Assuming termination.)  Dan _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
I completely forgot about free theorems! Do you have some links to
resources  I tried learning about them a while ago, but couldn't get a grasp on them... Thanks. /Joe On Oct 12, 2009, at 2:00 PM, Dan Piponi wrote: > On Mon, Oct 12, 2009 at 10:42 AM, muad <[hidden email]> > wrote: >> >> Is it possible to prove correctness of a functions by testing it? I >> think the >> tests would have to be constructed by inspecting the shape of the >> function >> definition. > > not True==False > not False==True > > Done. Tested :) > > Less trivially, consider a function of signature > > swap :: (a,b) > (b,a) > > We don't need to test it at all, it can only do one thing, swap its > arguments. (Assuming it terminates.) > > But consider: > swap :: (a,a) > (a,a) > > If I find that swap (1,2) == (2,1) then I know that swap (x,y)==(y,x) > for all types a and b. We only need one test. > The reason is that we have a free theorem that says that for all > functions, f, of type (a,a) > (a,a) this holds: > > f (g a,g b) == let (x,y) = f (a,b) in (g x',g y') > > For any x and y define > > g 1 = x > g 2 = y > > Then f(x,y) == f (g 1,g 2) == let (x',y') == f(1,2) in (g x',g y') == > let (x',y') == (2,1) in (g x',g y') == (g 2,g 1) == (y,x) > > In other words, free theorems can turn an infinite amount of testing > into a finite test. (Assuming termination.) >  > Dan > _______________________________________________ > HaskellCafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskellcafe _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
Joe,
> On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette <[hidden email]> wrote: > I completely forgot about free theorems! Do you have some links to resources >  I tried learning about them a while > ago, but couldn't get a grasp on them... Thanks. There is Wadler's paper but I do find it tricky: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875 You can play with the generator here: http://linux.tcs.inf.tudresden.de/~voigt/ft/ The results can look unreadable at first, but I find that if I copy them onto paper and do all of the remaining substitutions manually (like I had to do with (a,b) > (b,a)) you end up with something readable. If you keep doing this you'll get a good intuition for what the free theorem for a type will look like.  Dan _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by jfredett
What do you mean under shortcircuiting here, and what is the connection?
The property that allows to deduce global correctness from correctness on underdefined inputs is just continuity in the topological sense. 2009/10/12 Joe Fredette <[hidden email]>: > Oh thanks for the example, I suppose you can disregard my other message. > > I suppose this is a bit like shortcircuiting. No? > > > On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote: > >> For example, it is possible to prove correctness of a function >> "negatedHead :: [Bool] > Bool" by testing it on "True:undefined" and >> "False:undefined". >> >> 2009/10/12 Eugene Kirpichov <[hidden email]>: >>> >>> It is possible for functions with compact domain, not just finite. >>> >>> 2009/10/12 Joe Fredette <[hidden email]>: >>>> >>>> In general? No If we had an implementation of the `sin` function, how >>>> can >>>> testing a finite number of points along it determine >>>> if that implementation is correct for every point? >>>> >>>> For specific functions (particularly those with finite domain), it is >>>> possible. If you know the 'correct' output of every input, then testing >>>> each >>>> input and ensuring correct output will work. Consider the definition of >>>> the >>>> `not` function on booleans. The domain only has two elements (True and >>>> False) and the range has only two outputs (True and False), so if I test >>>> every input, and insure it maps appropriately to the specified output, >>>> we're >>>> all set. >>>> >>>> Basically, if you can write your function as a big case statement that >>>> covers the whole domain, and that domain is finite, then the function >>>> can be >>>> tested to prove it's correctness. >>>> >>>> Now, I should think the Muad'Dib would know that, perhaps you should go >>>> back >>>> to studying with the Mentats. :) >>>> >>>> /Joe >>>> >>>> >>>> >>>> On Oct 12, 2009, at 1:42 PM, muad wrote: >>>> >>>>> >>>>> Is it possible to prove correctness of a functions by testing it? I >>>>> think >>>>> the >>>>> tests would have to be constructed by inspecting the shape of the >>>>> function >>>>> definition. >>>>> >>>>>  >>>>> View this message in context: >>>>> >>>>> http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html >>>>> Sent from the Haskell  HaskellCafe mailing list archive at >>>>> Nabble.com. >>>>> >>>>> _______________________________________________ >>>>> HaskellCafe mailing list >>>>> [hidden email] >>>>> http://www.haskell.org/mailman/listinfo/haskellcafe >>>> >>>> _______________________________________________ >>>> HaskellCafe mailing list >>>> [hidden email] >>>> http://www.haskell.org/mailman/listinfo/haskellcafe >>>> >>> >>> >>> >>>  >>> Eugene Kirpichov >>> Web IR developer, market.yandex.ru >>> >> >> >> >>  >> Eugene Kirpichov >> Web IR developer, market.yandex.ru > >  Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Dan Piponi2
I'm making the same mistake repeatedly. In both my mails there are
places where I said (a,b) or (b,a) when I meant (a,a).  Dan On Mon, Oct 12, 2009 at 11:09 AM, Dan Piponi <[hidden email]> wrote: > Joe, > >> On Mon, Oct 12, 2009 at 11:03 AM, Joe Fredette <[hidden email]> wrote: >> I completely forgot about free theorems! Do you have some links to resources >>  I tried learning about them a while >> ago, but couldn't get a grasp on them... Thanks. > > There is Wadler's paper but I do find it tricky: > http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875 > > You can play with the generator here: > http://linux.tcs.inf.tudresden.de/~voigt/ft/ > The results can look unreadable at first, but I find that if I copy > them onto paper and do all of the remaining substitutions manually > (like I had to do with (a,b) > (b,a)) you end up with something > readable. If you keep doing this you'll get a good intuition for what > the free theorem for a type will look like. >  > Dan > HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Eugene Kirpichov
I mean that, like in the definition of ``
True  _ = True False  x = x If you generalize this to `or`ing a list of inputs, eg: foldr () False list_of_bools you can 'shortcircuit' the test as soon as you find a 'True' value. This is actually not the greatest example, since you can't actually test it in finite number of tests, but you can test "half" the function by testing a that lists like [True:undefined] or [False, False, False, ... , True , undefined] return "True". It's "shortcircuiting" in the sense that it (like the `` function) doesn't need to see (necessarily) all of it's arguments to return a correct result. /Joe On Oct 12, 2009, at 2:11 PM, Eugene Kirpichov wrote: > What do you mean under shortcircuiting here, and what is the > connection? > The property that allows to deduce global correctness from correctness > on underdefined inputs is just continuity in the topological sense. > > 2009/10/12 Joe Fredette <[hidden email]>: >> Oh thanks for the example, I suppose you can disregard my other >> message. >> >> I suppose this is a bit like shortcircuiting. No? >> >> >> On Oct 12, 2009, at 1:56 PM, Eugene Kirpichov wrote: >> >>> For example, it is possible to prove correctness of a function >>> "negatedHead :: [Bool] > Bool" by testing it on "True:undefined" >>> and >>> "False:undefined". >>> >>> 2009/10/12 Eugene Kirpichov <[hidden email]>: >>>> >>>> It is possible for functions with compact domain, not just finite. >>>> >>>> 2009/10/12 Joe Fredette <[hidden email]>: >>>>> >>>>> In general? No If we had an implementation of the `sin` >>>>> function, how >>>>> can >>>>> testing a finite number of points along it determine >>>>> if that implementation is correct for every point? >>>>> >>>>> For specific functions (particularly those with finite domain), >>>>> it is >>>>> possible. If you know the 'correct' output of every input, then >>>>> testing >>>>> each >>>>> input and ensuring correct output will work. Consider the >>>>> definition of >>>>> the >>>>> `not` function on booleans. The domain only has two elements >>>>> (True and >>>>> False) and the range has only two outputs (True and False), so >>>>> if I test >>>>> every input, and insure it maps appropriately to the specified >>>>> output, >>>>> we're >>>>> all set. >>>>> >>>>> Basically, if you can write your function as a big case >>>>> statement that >>>>> covers the whole domain, and that domain is finite, then the >>>>> function >>>>> can be >>>>> tested to prove it's correctness. >>>>> >>>>> Now, I should think the Muad'Dib would know that, perhaps you >>>>> should go >>>>> back >>>>> to studying with the Mentats. :) >>>>> >>>>> /Joe >>>>> >>>>> >>>>> >>>>> On Oct 12, 2009, at 1:42 PM, muad wrote: >>>>> >>>>>> >>>>>> Is it possible to prove correctness of a functions by testing >>>>>> it? I >>>>>> think >>>>>> the >>>>>> tests would have to be constructed by inspecting the shape of the >>>>>> function >>>>>> definition. >>>>>> >>>>>>  >>>>>> View this message in context: >>>>>> >>>>>> http://www.nabble.com/isproofbytestingpossibletp25860155p25860155.html >>>>>> Sent from the Haskell  HaskellCafe mailing list archive at >>>>>> Nabble.com. >>>>>> >>>>>> _______________________________________________ >>>>>> HaskellCafe mailing list >>>>>> [hidden email] >>>>>> http://www.haskell.org/mailman/listinfo/haskellcafe >>>>> >>>>> _______________________________________________ >>>>> HaskellCafe mailing list >>>>> [hidden email] >>>>> http://www.haskell.org/mailman/listinfo/haskellcafe >>>>> >>>> >>>> >>>> >>>>  >>>> Eugene Kirpichov >>>> Web IR developer, market.yandex.ru >>>> >>> >>> >>> >>>  >>> Eugene Kirpichov >>> Web IR developer, market.yandex.ru >> >> > > > >  > Eugene Kirpichov > Web IR developer, market.yandex.ru _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Dan Piponi2
Dan Piponi wrote:
> On Mon, Oct 12, 2009 at 10:42 AM, muad <[hidden email]> wrote: > >> Is it possible to prove correctness of a functions by testing it? >> > consider a function of signature > > swap :: (a,b) > (b,a) > > We don't need to test it at all, it can only do one thing, swap its > arguments. (Assuming it terminates.) > Terminates and does not swap its arguments :) What do free theorems say about this, exactly  do they just implicitly exclude this possibility? Neil. _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
Neil Brown wrote:
> Dan Piponi wrote: >> On Mon, Oct 12, 2009 at 10:42 AM, muad <[hidden email]> wrote: >> >>> Is it possible to prove correctness of a functions by testing it? >> consider a function of signature >> >> swap :: (a,b) > (b,a) >> >> We don't need to test it at all, it can only do one thing, swap its >> arguments. (Assuming it terminates.) >> > swap = undefined > > Terminates and does not swap its arguments :) What do free theorems > say about this, exactly  do they just implicitly exclude this > possibility? Normally, one presumes that "undefined" (id est, calling "error") is equivalent to looping, except that calling "error" is pragmatically speaking better: it is nicer to the caller of your function (they/you get to see a somewhat more descriptive error message instead of 100% CPU without any results). Regards, Jochem  Jochem Berndsen  [hidden email]  jochem@牛在田里.com _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Neil Brown7
On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown <[hidden email]> wrote:
> swap = undefined > > Terminates and does not swap its arguments :) What do free theorems say > about this, exactly  do they just implicitly exclude this possibility? I'm terrible at reasoning about functions with bottoms (ie. undefined or nontermination). But I suspect that a property like this holds: if the type signature of a function f is polymorphic in a, and it doesn't produce bottom for one particular value x of type a, for some particular type a, f can never produce bottom for any choice of x in any choice of type a. (Which is not to say it might not fail, but that the failure will be an issue with x, not f.) The intuition behind this is that if a function is polymorphic in a then it never examines the a. So even if a is bottom, the function can never know it. But it could fail because f additionally accepts as argument a polymorphic function that itself accepts a's, and that fails. But then it wouldn't be f's fault, it'd be the fault of the function you passed in. This is very poor of me. There's probably a nice precise formulation of what I've just said :)  Dan _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by jfredett
Joe Fredette wrote:
> Really? How? That sounds very interesting, I've got a fair knowledge > of basic topology, I'd love to see an application > to programming... Compactness is one of the most powerful concepts in mathematics, because on the one hand it makes it possible to reduce many infinite problems to finite ones (inherent in its definition: for every open cover there is a finite subcover), on the other hand it is often easy to prove compactness due to Tychonoff's theorem (any product of compact spaces is compact). The connection to computing science is very nicely explained in http://math.andrej.com/2007/09/28/seeminglyimpossiblefunctionalprograms/ I found this paragraph particularly enlightening: """ > modulus :: (Cantor > Integer) > Natural > modulus f = least(\n > forevery(\a > forevery(\b > eq n a b > (f a == f b)))) This [...] finds the modulus of uniform continuity, defined as the least natural number `n` such that `forall alpha,beta. alpha =_n beta implies f(alpha)=f(beta),` where `alpha =_n beta iff forall i< n. alpha_i = beta_i.` What is going on here is that computable functionals are continuous, which amounts to saying that finite amounts of the output depend only on finite amounts of the input. But the Cantor space is compact, and in analysis and topology there is a theorem that says that continuous functions defined on a compact space are uniformly continuous. In this context, this amounts to the existence of a single `n` such that for all inputs it is enough to look at depth `n` to get the answer (which in this case is always finite, because it is an integer). """ Cheers _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Neil Brown7
Neil Brown <[hidden email]> writes:
>> swap :: (a,b) > (b,a) >> We don't need to test it at all, it can only do one thing, swap its >> arguments. (Assuming it terminates.) > swap = undefined > Terminates and does not swap its arguments :) I think this counts as nontermination, and that for semantic purposes, any bottom value  infinite loops, exceptions, undefined  is treated equally. k  If I haven't seen further, it is by standing in the footprints of giants _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Ben Franksen
That has got to be the single awesomest thing I have ever seen ever...
The first time I tried to read through the "Seemingly Impossible Functional Programs" post, I understood none of it. Now it seems obviously. I Love Math... Thanks for the explanation! /Joe On Oct 12, 2009, at 3:22 PM, Ben Franksen wrote: > Joe Fredette wrote: >> Really? How? That sounds very interesting, I've got a fair knowledge >> of basic topology, I'd love to see an application >> to programming... > > Compactness is one of the most powerful concepts in mathematics, > because on > the one hand it makes it possible to reduce many infinite problems to > finite ones (inherent in its definition: for every open cover there > is a > finite subcover), on the other hand it is often easy to prove > compactness > due to Tychonoff's theorem (any product of compact spaces is > compact). The > connection to computing science is very nicely explained in > > http://math.andrej.com/2007/09/28/seeminglyimpossiblefunctionalprograms/ > > I found this paragraph particularly enlightening: > > """ >> modulus :: (Cantor > Integer) > Natural >> modulus f = least(\n > forevery(\a > forevery(\b > eq n a b > >> (f a == > f b)))) > > This [...] finds the modulus of uniform continuity, defined as the > least > natural number `n` such that > `forall alpha,beta. alpha =_n beta implies f(alpha)=f(beta),` > where > `alpha =_n beta iff forall i< n. alpha_i = beta_i.` > > What is going on here is that computable functionals are continuous, > which > amounts to saying that finite amounts of the output depend only on > finite > amounts of the input. But the Cantor space is compact, and in > analysis and > topology there is a theorem that says that continuous functions > defined on > a compact space are uniformly continuous. In this context, this > amounts to > the existence of a single `n` such that for all inputs it is enough > to look > at depth `n` to get the answer (which in this case is always finite, > because it is an integer). > """ > > Cheers > > _______________________________________________ > HaskellCafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskellcafe _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Dan Piponi2
Could that nice precise formulation simply be Scott continuity, which in
turn preserves compactness through composition and under application? Dan Piponi wrote: > On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown <[hidden email]> wrote: >> swap = undefined >> >> Terminates and does not swap its arguments :) What do free theorems say >> about this, exactly  do they just implicitly exclude this possibility? > > I'm terrible at reasoning about functions with bottoms (ie. undefined > or nontermination). > > But I suspect that a property like this holds: if the type signature > of a function f is polymorphic in a, and it doesn't produce bottom for > one particular value x of type a, for some particular type a, f can > never produce bottom for any choice of x in any choice of type a. > (Which is not to say it might not fail, but that the failure will be > an issue with x, not f.) > > The intuition behind this is that if a function is polymorphic in a > then it never examines the a. So even if a is bottom, the function can > never know it. But it could fail because f additionally accepts as > argument a polymorphic function that itself accepts a's, and that > fails. But then it wouldn't be f's fault, it'd be the fault of the > function you passed in. > > This is very poor of me. There's probably a nice precise formulation > of what I've just said :) >  > Dan > _______________________________________________ > HaskellCafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskellcafe > > _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
Free forum by Nabble  Edit this page 