[Haskell-cafe] is proof by testing possible?

[Joe Fredette]

Sadly not enough, I understand the basics, but the whole "proof <=>  
this diagram commutes" thing still seems like
voodoo to me. There is a section coming up in my Topology ISP that  
will be on CT. So I hope that I will be able to
gain some purchase on the subject, at least enough to build up a  
working understanding on my own.

I have a practical understanding of Functors and Natural  
Transformations, so working a bit with these free theorem things
is kind of fun.

Actually, another germane-if-random question, why isn't there a  
natural transformation class? Something like:


     class Functor f, Functor g => NatTrans g f a where
		trans :: f a -> g a

So your flatten function becomes a `trans` a la

     instance NatTrans Tree [] a where
		trans = flatten

In fact, I'm going to attempt to do this now... Maybe I'll figure out  
why before you reply. :)

/Joe


On Oct 12, 2009, at 8:41 PM, Brent Yorgey wrote:

> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe