Re: [Haskell-cafe] is proof by testing possible?

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe