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 <[email protected]> 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 >> [email protected] >> http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ > 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
