[Haskell-cafe] is proof by testing possible?

[Brent Yorgey]

Do you know any category theory?  What helped me finally grok free
theorems is that in the simplest cases, the free theorem for a
polymorphic function is just a naturality condition.  For example, the
free theorem for

  flatten :: Tree a -> [a]

is precisely the statement that flatten is a natural transformation
from the Tree functor to the list functor:

  fmap_[] g . flatten == flatten . fmap_Tree g

It gets more complicated than this, of course, but that's the basic idea.

-Brent

On Mon, Oct 12, 2009 at 02:03:11PM -0400, Joe Fredette 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.
>
> /Joe
>
>
>
> On Oct 12, 2009, at 2:00 PM, Dan Piponi wrote:
>
>> On Mon, Oct 12, 2009 at 10:42 AM, muad <muad.dib.space at gmail.com> 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
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe