[Haskell-cafe] is proof by testing possible?
wren ng thornton
wren at freegeek.org
Thu Oct 15 03:06:33 EDT 2009
Joe Fredette wrote:
> I fiddled with my previous idea -- the NatTrans class -- a bit, the results
> are here, 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.
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
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 
go ys  = ys
go ys (x:xs) = go (x:ys) xs
nil :: F a -> G a
nil = const 
More information about the Haskell-Cafe