[Haskell-cafe] is proof by testing possible?

[wren ng thornton]

Joe Fredette wrote:
> 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

A few problems there:

(1) The |a| should be natural, i.e. universally qualified in the class 
methods, not an argument of the typeclass.

(2) Just because there's a natural transformation from F to G does not 
mean there's a "related" natural transformation back. The law you want is,

     forall (X :: *) (Y :: *) (f :: X -> Y).
         eta_Y . fmap_F f == fmap_G f . eta_X

(3) There can be more than one natural transformation between two 
functors. Which means a type class is the wrong way to go about things 
since there can only be one for the set of type parameters. Consider for 
instance:

     type F a = [a]
     type G a = [a]

     identity :: F a -> G a
     identity []     = []
     identity (x:xs) = (x:xs)

     reverse :: F a -> G a
     reverse = go []
         where
         go ys []     = ys
         go ys (x:xs) = go (x:ys) xs

     nil :: F a -> G a
     nil = const []

     ...

-- 
Live well,
~wren