I fiddled with my previous idea -- the NatTrans class -- a bit, the
results
are here[1], I don't know enough really to know if I got the NT law
right, or
even if the class defn is right.
Any thoughts? Am I doing this right/wrong/inbetween? Is there any use
for a class
like this? I listed a couple ideas of use-cases in the paste, but I
have no idea of
the applicability of either of them.
/Joe
http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10679#a10679
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 <[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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
